CyclicPartition.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

38 declarations, 0 contain sorry, 0 declared as axioms

Recognition theorems for groups with a partition into cyclic subgroups

This file defines Dickson.HasCyclicPartition G configs: the finite group G is covered by a list of cyclic subgroups Hᵢ of order dᵢ (each appearing with fᵢ conjugates, intersecting pairwise trivially) matching the list configs of Dickson.CyclicPartitionConfig data.

The main results recognise a finite group from the combinatorics of such a partition:

Dickson.isCyclic_of_hasCyclicPartition: one part of full order forces G cyclic;
Dickson.dihedral_of_hasCyclicPartition_odd and Dickson.dihedral_of_hasCyclicPartition_even: partitions of type {n, 2, …, 2} force G ≃* DihedralGroup n;
Dickson.iso_A4_of_hasCyclicPartition, Dickson.iso_S4_of_hasCyclicPartition and Dickson.iso_A5_of_hasCyclicPartition: the partitions corresponding to the exceptional groups of orders 12, 24 and 60 force G ≃* A₄, S₄, A₅ respectively.

These are used in the tame case of Dickson's classification of finite subgroups of PGL₂(𝔽̄_p).

Imports (7)

Imported by 2 files

structure Dickson.CyclicPartitionConfig Combinatorial data for one class in a cyclic partition: f conjugate cyclic subgroups, each of order d line 60 source
Source documentation
Combinatorial data for one class in a cyclic partition: f conjugate cyclic subgroups, each of order d.

no axioms what this means
```
structure CyclicPartitionConfig where
…
```
def Dickson.HasCyclicPartition HasCyclicPartition G configs states that the finite group G is covered by cyclic subgroups (intersecting pairwise trivially) whose orders and conjugate counts match configs line 69 source
Source documentation
HasCyclicPartition G configs states that the finite group G is covered by cyclic subgroups (intersecting pairwise trivially) whose orders and conjugate counts match configs.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, List, Dickson.CyclicPartitionConfig
Proof uses: Exists, Subgroup, And, Eq, Nat, List.length, Fin, Option, GetElem?.getElem?, LT.lt, Option.some, List.get, IsCyclic, Subtype, Membership.mem, Nat.card, Dickson.CyclicPartitionConfig.d, Subgroup.normalizer, HMul.hMul, Dickson.CyclicPartitionConfig.f and 11 more
25 instances, coercions and auxiliary constants left out.
```
def HasCyclicPartition (G : Type*) [Group G] [Fintype G]
    (configs : List CyclicPartitionConfig) : Prop :=
…
```
Mentions: Dickson.CyclicPartitionConfig
theorem Dickson.isCyclic_of_hasCyclicPartition line 87 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Nat, Eq, Nat.card, Dickson.HasCyclicPartition, List.cons, Dickson.CyclicPartitionConfig, Dickson.CyclicPartitionConfig.mk, OfNat.ofNat, List.nil, IsCyclic
Proof uses: List, Subgroup, And, List.length, Fin, Exists, Option, GetElem?.getElem?, LT.lt, Option.some, List.get, Subtype, Membership.mem, Dickson.CyclicPartitionConfig.d, Subgroup.normalizer, HMul.hMul, Dickson.CyclicPartitionConfig.f, Set, Set.ofPred, Subgroup.map and 27 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem Dickson.dihedralRecognition line 98 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Nat, GE.ge, OfNat.ofNat, Subgroup, Subgroup.Normal, IsCyclic, Subtype, Membership.mem, Eq, Nat.card, Subgroup.index, Not, orderOf, Nonempty, MulEquiv, DihedralGroup
Proof uses: NeZero, NeZero.mk, Nat.ne_of_gt, LT.lt.trans_le, Nat.succ, Nat.zero_lt_succ, Exists, Decidable.byContradiction, Top.top, Subgroup.ext, iff_of_true, Eq.mp, Eq.trans, binderNameHint, forall_congr, trivial, absurd, False, congrArg, Subgroup.index_top and 139 more
154 instances, coercions and auxiliary constants left out.

Tactic trace: 186 steps
Open to load the checked before-and-after goal states.
lemma Dickson.extractDihedralStructure line 312 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Nat, Eq, Nat.card, HMul.hMul, OfNat.ofNat, GE.ge, Subgroup, Subtype, Membership.mem, Subgroup.normalizer, Not, Ne, orderOf, And, Subgroup.Normal, Subgroup.index
Proof uses: And.intro, Iff.mp, Top.top, Subgroup.normalizer_eq_top_iff, Subgroup.eq_top_of_card_eq, Eq.trans, Eq.symm, Nat.eq_of_mul_eq_mul_right, LT.lt.trans_le, zero_lt_two, Eq.mpr, id, congrArg, Subgroup.index_mul_card, Eq.rec, Subgroup.one_mem
48 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Dickson.dihedral_of_hasCyclicPartition_odd line 325 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Nat, GE.ge, OfNat.ofNat, Eq, Nat.card, HMul.hMul, Dickson.HasCyclicPartition, List.cons, Dickson.CyclicPartitionConfig, Dickson.CyclicPartitionConfig.mk, List.nil, Nonempty, MulEquiv, DihedralGroup
Proof uses: List, Subgroup, And, List.length, Fin, Exists, Option, GetElem?.getElem?, LT.lt, Option.some, List.get, IsCyclic, Subtype, Membership.mem, Dickson.CyclicPartitionConfig.d, Subgroup.normalizer, Dickson.CyclicPartitionConfig.f, Set, Set.ofPred, Subgroup.map and 59 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
theorem Dickson.dihedral_of_hasCyclicPartition_even line 374 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Nat, GE.ge, OfNat.ofNat, Eq, Nat.card, HMul.hMul, Dickson.HasCyclicPartition, List.cons, Dickson.CyclicPartitionConfig, Dickson.CyclicPartitionConfig.mk, List.nil, Nonempty, MulEquiv, DihedralGroup
Proof uses: List, Subgroup, And, List.length, Fin, Exists, Option, GetElem?.getElem?, LT.lt, Option.some, List.get, IsCyclic, Subtype, Membership.mem, Dickson.CyclicPartitionConfig.d, Subgroup.normalizer, Dickson.CyclicPartitionConfig.f, Set, Set.ofPred, Subgroup.map and 60 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
lemma Dickson.subgroup_S4_order12_eq_A4 line 427 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Subgroup, Equiv.Perm, Fin, OfNat.ofNat, Nat, Eq, Nat.card, Subtype, Membership.mem, alternatingGroup
Proof uses: Equiv.Perm.eq_alternatingGroup_of_index_eq_two, HMul.hMul, Subgroup.index, Subgroup.index_mul_card, id, Nat.factorial, Decidable.byContradiction, Not, Eq.mp, Fintype.card, congrArg, Fintype.card_fin, Fintype.card_perm, Nat.card_eq_fintype_card
17 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem Dickson.sylow_inf_eq_bot_of_prime_card line 435 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Nat, Fact, Nat.Prime, Sylow, Ne, Eq, Nat.card, Subtype, Membership.mem, Subgroup, Min.min, Bot.bot
Proof uses: OfNat.ofNat, Or, Iff.mp, Dvd.dvd, Nat.dvd_prime, Fact.out, Eq.rec, Subgroup.card_dvd_of_le, inf_le_left, Or.inl, Subgroup.card_eq_one, Or.inr, False.elim, Set, SetLike.coe_set_eq, Set.eq_of_subset_of_ncard_le, And.left, id, LE.le, Set.ncard and 11 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
theorem Dickson.sylow3_toPermHom_ker_eq_bot_of_card_12 line 457 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Eq, Nat, Nat.card, OfNat.ofNat, Sylow, Subgroup, MonoidHom.ker, Equiv.Perm, MulAction.toPermHom, Bot.bot
Proof uses: Subtype, Membership.mem, Subgroup.normalizer, HMul.hMul, Subgroup.index, Subgroup.index_mul_card, Decidable.byContradiction, Not, Eq.mp, congrArg, Eq.symm, Sylow.card_eq_index_normalizer, Dickson.instFactPrimeOfNatNat_fLT_1, Dickson.instFintypeSylow, Dvd.dvd, Subgroup.card_dvd_of_le, LE.le, Subgroup.le_normalizer, Or, Iff.mp and 49 more
71 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
lemma Dickson.iso_A4_of_card_12_sylow3_4 line 510 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Eq, Nat, Nat.card, OfNat.ofNat, Sylow, Nonempty, MulEquiv, Subtype, Equiv.Perm, Fin, Membership.mem, Subgroup, alternatingGroup
Proof uses: Function.Injective, MonoidHom, MulAction.toPermHom, Iff.mp, MonoidHom.ker, Bot.bot, MonoidHom.ker_eq_bot_iff, Dickson.sylow3_toPermHom_ker_eq_bot_of_card_12, Fintype.card, Dickson.instFintypeSylow, Eq.mpr, id, congrArg, Fintype.card_fin, Eq.symm, Nat.card_eq_fintype_card, Eq.refl, Equiv, Equiv.permCongr, Fintype.equivOfCardEq and 30 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Dickson.card_sylow3_of_non_normal_order3 line 535 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Eq, Nat, Nat.card, OfNat.ofNat, Subgroup, Subtype, Membership.mem, Not, Subgroup.Normal, Sylow
Proof uses: Nat.ModEq, card_sylow_modEq_one, Dickson.instFactPrimeOfNatNat_fLT_1, Dickson.instFintypeSylow, Dvd.dvd, Eq.rec, Subgroup.index, Subgroup.normalizer, Classical.arbitrary, Subgroup.index_dvd_card, Eq.symm, Sylow.card_eq_index_normalizer, Or, LE.le, Nat.le_of_dvd, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false and 111 more
125 instances, coercions and auxiliary constants left out.

Tactic trace: 42 steps
Open to load the checked before-and-after goal states.
theorem Dickson.iso_A4_of_hasCyclicPartition line 588 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Eq, Nat, Nat.card, OfNat.ofNat, Dickson.HasCyclicPartition, List.cons, Dickson.CyclicPartitionConfig, Dickson.CyclicPartitionConfig.mk, List.nil, Nonempty, MulEquiv, Subtype, Equiv.Perm, Fin, Membership.mem, Subgroup, alternatingGroup
Proof uses: List, And, List.length, Exists, Option, GetElem?.getElem?, LT.lt, Option.some, List.get, IsCyclic, Dickson.CyclicPartitionConfig.d, Subgroup.normalizer, HMul.hMul, Dickson.CyclicPartitionConfig.f, Set, Set.ofPred, Subgroup.map, MulEquiv.toMonoidHom, MonoidHom, MulAut and 18 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Dickson.card_sylow3_of_hasCyclicPartition_S4 line 600 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Eq, Nat, Nat.card, OfNat.ofNat, Dickson.HasCyclicPartition, List.cons, Dickson.CyclicPartitionConfig, Dickson.CyclicPartitionConfig.mk, List.nil, Sylow
Proof uses: List, Subgroup, And, List.length, Fin, Exists, Option, GetElem?.getElem?, LT.lt, Option.some, List.get, IsCyclic, Subtype, Membership.mem, Dickson.CyclicPartitionConfig.d, Subgroup.normalizer, HMul.hMul, Dickson.CyclicPartitionConfig.f, Set, Set.ofPred and 61 more
73 instances, coercions and auxiliary constants left out.

Tactic trace: 42 steps
Open to load the checked before-and-after goal states.
lemma Dickson.center_eq_bot_of_hasCyclicPartition line 649 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Nat, Eq, Nat.card, List, Dickson.CyclicPartitionConfig, Membership.mem, LT.lt, HMul.hMul, Dickson.CyclicPartitionConfig.f, Dickson.CyclicPartitionConfig.d, Dickson.HasCyclicPartition, Subgroup, Subgroup.center, Bot.bot
Proof uses: And, List.length, Fin, Exists, Option, GetElem?.getElem?, Option.some, List.get, IsCyclic, Subtype, Subgroup.normalizer, Set, Set.ofPred, Subgroup.map, MulEquiv.toMonoidHom, MonoidHom, MulAut, MulAut.conj, Ne, Min.min and 59 more
89 instances, coercions and auxiliary constants left out.

Tactic trace: 51 steps
Open to load the checked before-and-after goal states.
lemma Dickson.normal_order2_le_center line 714 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Subgroup, Subgroup.Normal, Eq, Nat, Nat.card, Subtype, Membership.mem, OfNat.ofNat, LE.le, Subgroup.center
Proof uses: Subgroup.zpowers, Exists, IsCyclic.exists_generator, isCyclic_of_prime_card, Dickson.instFactPrimeOfNatNat_fLT, Subgroup.ext, Iff.intro, Int, HPow.hPow, Subtype.mk, Iff.mp, Subgroup.mem_zpowers_iff, congrArg, Eq.symm, Iff.mpr, Exists.intro, Eq.mp, Subgroup.coe_zpow, Eq.rec, Subgroup.zpow_mem and 42 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 50 steps
Open to load the checked before-and-after goal states.
lemma Dickson.card_sylow_eq_one_of_normal line 772 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Nat, Fact, Nat.Prime, Subgroup, Subgroup.Normal, IsPGroup, Subtype, Membership.mem, Eq, Nat.card, HPow.hPow, Finsupp, Nat.factorization, Sylow, OfNat.ofNat
Proof uses: LE.le, Exists, IsPGroup.exists_le_sylow, SetLike.ext', Set.eq_of_subset_of_ncard_le, Eq.ge, Eq.trans, Eq.symm, Sylow.card_eq_multiplicity, Set.toFinite, Set, Eq.mpr, Fintype.card, Dickson.instFintypeSylow, id, congrArg, Nat.card_eq_fintype_card, propext, Fintype.card_eq_one_iff, Exists.intro and 8 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Dickson.not_normal_order6_of_card_sylow3_4 line 787 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Eq, Nat, Nat.card, OfNat.ofNat, Sylow, Subgroup, Subgroup.Normal, Subtype, Membership.mem, False
Proof uses: Exists, Iff.mp, Fintype.card, Dickson.instFintypeSylow, Fintype.card_eq_one_iff, Dvd.dvd, Eq.mpr, HasQuotient.Quotient, Subgroup.normalizer, Classical.arbitrary, id, congrArg, Nat.card_congr, Sylow.equivQuotientNormalizer, Dickson.instFactPrimeOfNatNat_fLT_1, Eq.symm, Subgroup.card_quotient_dvd_card, HMod.hMod, card_sylow_modEq_one, Nat.card_eq_fintype_card and 51 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
lemma Dickson.toPermHom_injective_of_card_24 line 832 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Eq, Nat, Nat.card, OfNat.ofNat, Sylow, Subgroup, Subgroup.center, Bot.bot, Function.Injective, Equiv.Perm, MonoidHom, MulAction.toPermHom
Proof uses: MonoidHom.ker, Classical.arbitrary, Dvd.dvd, Subtype, Membership.mem, Eq.rec, Subgroup.normalizer, Subgroup.card_dvd_of_le, Iff.mp, HSMul.hSMul, Sylow.smul_eq_iff_mem_normalizer, Equiv.Perm.ext_iff, MonoidHom.mem_ker, HMul.hMul, Decidable.byContradiction, Not, Eq.mpr, id, congrArg, Eq.symm and 57 more
74 instances, coercions and auxiliary constants left out.

Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
theorem Dickson.iso_S4_of_hasCyclicPartition line 877 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Eq, Nat, Nat.card, OfNat.ofNat, Dickson.HasCyclicPartition, List.cons, Dickson.CyclicPartitionConfig, Dickson.CyclicPartitionConfig.mk, List.nil, Nonempty, MulEquiv, Equiv.Perm, Fin
Proof uses: Sylow, Dickson.card_sylow3_of_hasCyclicPartition_S4, Subgroup, Subgroup.center, Bot.bot, Dickson.center_eq_bot_of_hasCyclicPartition, Membership.mem, List, Or, False, LT.lt, HMul.hMul, Dickson.CyclicPartitionConfig.f, Dickson.CyclicPartitionConfig.d, Eq.mp, Eq.trans, congrArg, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_mul, Eq.refl and 32 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma Dickson.orderOf_mem_of_hasCyclicPartition_A5 line 905 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Dickson.HasCyclicPartition, List.cons, Dickson.CyclicPartitionConfig, Dickson.CyclicPartitionConfig.mk, OfNat.ofNat, Nat, List.nil, Ne, Membership.mem, Finset, Insert.insert, Singleton.singleton, orderOf
Proof uses: List, Subgroup, And, Eq, List.length, Fin, Exists, Option, GetElem?.getElem?, LT.lt, Option.some, List.get, IsCyclic, Subtype, Nat.card, Dickson.CyclicPartitionConfig.d, Subgroup.normalizer, HMul.hMul, Dickson.CyclicPartitionConfig.f, Set and 49 more
64 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
lemma Dickson.card_sylow5_of_hasCyclicPartition_A5 line 934 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Eq, Nat, Nat.card, OfNat.ofNat, Dickson.HasCyclicPartition, List.cons, Dickson.CyclicPartitionConfig, Dickson.CyclicPartitionConfig.mk, List.nil, Sylow
Proof uses: List, Subgroup, And, List.length, Fin, Exists, Option, GetElem?.getElem?, LT.lt, Option.some, List.get, IsCyclic, Subtype, Membership.mem, Dickson.CyclicPartitionConfig.d, Subgroup.normalizer, HMul.hMul, Dickson.CyclicPartitionConfig.f, Set, Set.ofPred and 53 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma Dickson.card_sylow3_of_hasCyclicPartition_A5 line 954 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Eq, Nat, Nat.card, OfNat.ofNat, Dickson.HasCyclicPartition, List.cons, Dickson.CyclicPartitionConfig, Dickson.CyclicPartitionConfig.mk, List.nil, Sylow
Proof uses: List, Subgroup, And, List.length, Fin, Exists, Option, GetElem?.getElem?, LT.lt, Option.some, List.get, IsCyclic, Subtype, Membership.mem, Dickson.CyclicPartitionConfig.d, Subgroup.normalizer, HMul.hMul, Dickson.CyclicPartitionConfig.f, Set, Set.ofPred and 55 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma Dickson.sylow_le_normal_of_coprime_index line 974 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Nat, Fact, Nat.Prime, Subgroup, Subgroup.Normal, Nat.Coprime, Subgroup.index, Sylow, LE.le
Proof uses: Eq, Nat.card, Subtype, HasQuotient.Quotient, Membership.mem, Subgroup.map, QuotientGroup.mk', HPow.hPow, Exists, Iff.mp, IsPGroup, IsPGroup.iff_card, IsPGroup.map, Sylow.isPGroup', Nat.casesAuxOn, OfNat.ofNat, Subsingleton, Nonempty, And, Nat.card_eq_one_iff_unique and 28 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Dickson.card_elements_orderOf_prime line 991 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Nat, Fact, Nat.Prime, Eq, Finsupp, Nat.factorization, Nat.card, OfNat.ofNat, Fintype.card, Set.ofPred, orderOf, Membership.mem, Set, HMul.hMul, Sylow, HSub.hSub
Proof uses: Subtype, Subgroup, Eq.mpr, HPow.hPow, id, congrArg, Sylow.card_eq_multiplicity, pow_one, Eq.refl, Sigma, And, Ne, Subtype.mk, Dvd.dvd, Subgroup.zpowers, Subgroup.card_dvd_of_le, Iff.mpr, LE.le, Subgroup.zpowers_le, Or and 58 more
88 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
lemma Dickson.mem_of_orderOf_prime_sylow_le line 1040 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Nat, Fact, Nat.Prime, Subgroup, Sylow, LE.le, Eq, orderOf, Membership.mem
Proof uses: IsPGroup, Subtype, Subgroup.zpowers, Iff.mpr, Exists, Nat.card, HPow.hPow, IsPGroup.iff_card, Exists.intro, OfNat.ofNat, Eq.mpr, Fintype.card, id, congrArg, Nat.card_eq_fintype_card, Fintype.card_zpowers, pow_one, Eq.refl, IsPGroup.exists_le_sylow, Subgroup.mem_zpowers
27 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Dickson.exists_orderOf_15_of_card_15 line 1051 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Eq, Nat, Nat.card, OfNat.ofNat, Exists, orderOf
Proof uses: Sylow, Classical.arbitrary, Dvd.dvd, Eq.rec, HasQuotient.Quotient, Subgroup, Subgroup.normalizer, Subgroup.card_quotient_dvd_card, Eq.symm, Nat.card_congr, Sylow.equivQuotientNormalizer, Dickson.instFactPrimeOfNatNat_fLT_1, Dickson.instFintypeSylow, HMod.hMod, card_sylow_modEq_one, Unit, rfl, of_eq_true, Eq.trans, True and 98 more
95 instances, coercions and auxiliary constants left out.

Tactic trace: 63 steps
Open to load the checked before-and-after goal states.
lemma Dickson.card_ge_45_of_orders_3_and_5 line 1136 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Eq, Nat, Nat.card, OfNat.ofNat, Sylow, Subgroup, orderOf, Membership.mem, LE.le, Subtype
Proof uses: Set.ncard, Set.ofPred, Eq.mpr, id, congrArg, Eq.symm, Nat.card_coe_set_eq, Fintype.card, Set, Nat.card_eq_fintype_card, HMul.hMul, HSub.hSub, Dickson.card_elements_orderOf_prime, Dickson.instFactPrimeOfNatNat_fLT_1, Finsupp, Nat.factorization, Dickson.Nat.factorization_eq_one, rfl, Nat.prime_three, Mathlib.Meta.NormNum.isNat_dvd_false and 36 more
56 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma Dickson.not_normal_of_card_lt line 1167 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Nat, Fact, Nat.Prime, Eq, Finsupp, Nat.factorization, Nat.card, OfNat.ofNat, Subgroup, Subgroup.Normal, Nat.Coprime, Subgroup.index, GT.gt, HAdd.hAdd, HMul.hMul, Sylow, HSub.hSub, Subtype and 2 more
Proof uses: LE.le, Set, Union.union, Set.ofPred, orderOf, Singleton.singleton, Set.union_subset, Dickson.mem_of_orderOf_prime_sylow_le, Dickson.sylow_le_normal_of_coprime_index, Iff.mpr, Set.singleton_subset_iff, Subgroup.one_mem, Set.ncard, Set.ncard_le_ncard, Set.toFinite, id, False.elim, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp and 71 more
119 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Dickson.isSimple_of_hasCyclicPartition_A5 line 1188 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Eq, Nat, Nat.card, OfNat.ofNat, Dickson.HasCyclicPartition, List.cons, Dickson.CyclicPartitionConfig, Dickson.CyclicPartitionConfig.mk, List.nil, IsSimpleGroup
Proof uses: Sylow, Dickson.card_sylow5_of_hasCyclicPartition_A5, Dickson.card_sylow3_of_hasCyclicPartition_A5, Nontrivial, Eq.mpr, LT.lt, Fintype.card, id, congrArg, Eq.symm, propext, Fintype.one_lt_card_iff_nontrivial, Nat.card_eq_fintype_card, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, IsSimpleGroup.mk, Subgroup and 91 more
94 instances, coercions and auxiliary constants left out.

Tactic trace: 188 steps
Open to load the checked before-and-after goal states.
lemma Dickson.exists_normal_complement_of_sylow2_15 line 1352 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Eq, Nat, Nat.card, OfNat.ofNat, Sylow, Exists, Subgroup, And, Subgroup.Normal, Subtype, Membership.mem
Proof uses: Nonempty, LE.le, Subgroup.normalizer, Subgroup.centralizer, Set, Eq.symm, HMul.hMul, Subtype.mk, Subgroup.le_normalizer, Iff.mp, Subtype.ext_iff, Std.Commutative.comm, IsPGroup.isMulCommutative_of_card_eq_prime_sq, Dickson.instFactPrimeOfNatNat_fLT, HPow.hPow, HasQuotient.Quotient, Subgroup.card_eq_card_quotient_mul_card_subgroup, Decidable.byContradiction, Not, Eq.mp and 21 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Dickson.card_sylow2_ne_one_of_simple_60 line 1375 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Eq, Nat, Nat.card, OfNat.ofNat, IsSimpleGroup, Ne, Sylow
Proof uses: Exists, False, Iff.mp, Nat.card_eq_one_iff_exists, Subgroup.Normal, Subgroup.Normal.mk, Membership.mem, Subgroup, Eq.rec, HSMul.hSMul, HMul.hMul, Inv.inv, Iff.mpr, Set, MulAut, Set.smulSet, MonoidHom, MulAut.conj, And, Set.mem_smul_set and 40 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma Dickson.card_sylow2_ne_three_of_simple_60 line 1399 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Eq, Nat, Nat.card, OfNat.ofNat, IsSimpleGroup, Ne, Sylow
Proof uses: MonoidHom, Equiv.Perm, MulAction.toPermHom, Subgroup, MonoidHom.ker, Bot.bot, Top.top, Or, False, Subgroup.Normal.eq_bot_or_eq_top, absurd, LE.le, Nat.card_le_card_of_injective, Dickson.instFintypeSylow, Eq.mp, Function.Injective, congrArg, propext, MonoidHom.ker_eq_bot_iff, Eq.mpr and 24 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma Dickson.card_sylow2_eq_five_of_simple_60 line 1417 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Eq, Nat, Nat.card, OfNat.ofNat, IsSimpleGroup, Sylow
Proof uses: Exists, Exists.intro, rfl, Dvd.dvd, Eq.mpr, id, congrArg, Eq.symm, Subgroup.index, Subgroup.normalizer, Classical.arbitrary, Sylow.card_eq_index_normalizer, Dickson.instFactPrimeOfNatNat_fLT, Dickson.instFintypeSylow, Subgroup.card_quotient_dvd_card, HMod.hMod, Eq.rec, card_sylow_modEq_one, LE.le, Nat.le_of_dvd and 67 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
lemma Dickson.toPermHom_injective_of_simple_60 line 1450 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Eq, Nat, Nat.card, OfNat.ofNat, IsSimpleGroup, Function.Injective, Equiv.Perm, Sylow, MonoidHom, MulAction.toPermHom
Proof uses: Subgroup, MonoidHom.ker, Bot.bot, Top.top, Or, Subgroup.Normal.eq_bot_or_eq_top, Eq.mp, congrArg, propext, MonoidHom.ker_eq_bot_iff, False.elim, Dickson.card_sylow2_eq_five_of_simple_60, Iff.mpr, And, Subsingleton, Nonempty, Nat.card_eq_one_iff_unique, And.intro, Subsingleton.intro, HSMul.hSMul and 10 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma Dickson.subgroup_S5_order60_eq_A5 line 1468 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Subgroup, Equiv.Perm, Fin, OfNat.ofNat, Nat, Eq, Nat.card, Subtype, Membership.mem, alternatingGroup
Proof uses: Equiv.Perm.eq_alternatingGroup_of_index_eq_two, HMul.hMul, Subgroup.index, Subgroup.index_mul_card, Decidable.byContradiction, Not, Eq.mp, Nat.factorial, congrArg, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_factorial, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Fintype.card, Fintype.card_fin, Fintype.card_perm, Nat.card_eq_fintype_card
18 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Dickson.iso_A5_of_simple_60 line 1477 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Eq, Nat, Nat.card, OfNat.ofNat, IsSimpleGroup, Nonempty, MulEquiv, Subtype, Equiv.Perm, Fin, Membership.mem, Subgroup, alternatingGroup
Proof uses: Equiv, Sylow, Fintype.equivOfCardEq, Dickson.instFintypeSylow, Fintype.card, Eq.mpr, id, congrArg, Eq.symm, Nat.card_eq_fintype_card, Dickson.card_sylow2_eq_five_of_simple_60, Eq.refl, MonoidHom, MonoidHom.comp, MonoidHom.mk', Equiv.permCongr, Equiv.Perm.ext, HMul.hMul, Fin.ext, of_eq_true and 33 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
theorem Dickson.iso_A5_of_hasCyclicPartition line 1502 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Fintype, Eq, Nat, Nat.card, OfNat.ofNat, Dickson.HasCyclicPartition, List.cons, Dickson.CyclicPartitionConfig, Dickson.CyclicPartitionConfig.mk, List.nil, Nonempty, MulEquiv, Subtype, Equiv.Perm, Fin, Membership.mem, Subgroup, alternatingGroup
Proof uses: Dickson.iso_A5_of_simple_60, Dickson.isSimple_of_hasCyclicPartition_A5
13 instances, coercions and auxiliary constants left out.