RecognitionA5.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

45 declarations, 0 contain sorry, 0 declared as axioms

Recognition of `A₅` inside `PGL₂(𝔽̄_p)`

This file proves Dickson.recognition_A5-style results: a finite subgroup of PGLOf (K p) = PGL₂(𝔽̄_p) of order 60 satisfying the constraints arising in the wild case of Dickson's classification is isomorphic to the alternating group A₅.

The proof is the classical Sylow-theoretic argument that a group of order 60 with no normal Sylow subgroups is simple, hence isomorphic to A₅ (via the action on the five Sylow 2-subgroups / cosets argument), combined with the dichotomy Dickson.element_dichotomy for elements of a finite subgroup of PGLOf (K p): every element either has order p or has order coprime to p.

Imports (4)

Imported by 2 files

instance Dickson.instFintypeOfGroupOfFinite A finite group is a Fintype line 51 source
Source documentation
A finite group is a Fintype. The [Group G] hypothesis restricts this instance to firing on groups, rather than acting as a general Finite → Fintype instance.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Finite, Fintype
Proof uses: Fintype.ofFinite
```
noncomputable instance instFintypeOfGroupOfFinite {G : Type*} [Group G] [Finite G] :
    Fintype G := Fintype.ofFinite _
```
lemma Dickson.factorization_60_2 line 54 source
lemma Dickson.factorization_60_3 line 57 source
lemma Dickson.factorization_60_5 line 60 source
lemma Dickson.factorization_30_3 line 63 source
lemma Dickson.factorization_30_5 line 66 source
lemma Dickson.factorization_15_5 line 69 source
lemma Dickson.factorization_15_3 line 72 source
lemma Dickson.commute_preserves_fixedPoint line 79 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, Dickson.PGLOf, Dickson.K, ZMod, Dickson.ProjectiveLine, Eq, HMul.hMul, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Matrix, Subgroup.center, HSMul.hSMul
Proof uses: Eq.mpr, id, congrArg, Eq.symm, SemigroupAction.mul_smul, Eq.refl
47 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Dickson.order_p_one_fixed_point line 84 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Dickson.PGLOf, Dickson.K, ZMod, Eq, orderOf, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Set.ncard, Dickson.ProjectiveLine, Dickson.fixedPoints
Proof uses: Iff.mpr, And.left, Iff, Nat.Coprime, Dickson.fixedPoints_dichotomy, Nat.Prime.ne_one, Fact.out, Eq.trans, Eq.symm, congrArg, orderOf_one, Iff.mp, LT.lt, IsOfFinOrder, orderOf_pos_iff, Eq.rec, Nat.Prime.pos
37 instances, coercions and auxiliary constants left out.
lemma Dickson.coprime_order_two_fixed_points line 90 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Dickson.PGLOf, Dickson.K, ZMod, Ne, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, IsOfFinOrder, Nat.Coprime, orderOf, Eq, Set.ncard, Dickson.ProjectiveLine, Dickson.fixedPoints
Proof uses: Iff.mpr, And.right, Iff, Dickson.fixedPoints_dichotomy, Nat.Coprime.symm
42 instances, coercions and auxiliary constants left out.
lemma Dickson.two_fixed_points_contradicts_order_p line 95 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Dickson.PGLOf, Dickson.K, ZMod, Dickson.ProjectiveLine, Eq, orderOf, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Ne, HSMul.hSMul, False
Proof uses: Exists, Set, Dickson.fixedPoints, Singleton.singleton, Iff.mp, Set.ncard, Set.ncard_eq_one, Dickson.order_p_one_fixed_point, Eq.trans, And.right, Membership.mem, And, Set.eq_singleton_iff_unique_mem, Eq.symm
39 instances, coercions and auxiliary constants left out.
lemma Dickson.swap_contradicts_odd_order line 103 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Dickson.PGLOf, Dickson.K, ZMod, Dickson.ProjectiveLine, Eq, orderOf, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Ne, HSMul.hSMul, False
Proof uses: Dickson.two_fixed_points_contradicts_order_p, HPow.hPow, Eq.mpr, HDiv.hDiv, Nat.gcd, id, congrArg, orderOf_pow', ne_of_gt, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Nat.ble, Nat.gcd_comm, HMod.hMod, Nat.gcd_rec, Or.resolve_left, Nat.Prime.eq_two_or_odd, Fact.out and 5 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Dickson.no_commute_p_coprime line 116 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Dickson.PGLOf, Dickson.K, ZMod, Ne, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Eq, orderOf, IsOfFinOrder, Nat.Coprime, HMul.hMul, False
Proof uses: Dickson.ProjectiveLine, Exists, And, Set, Dickson.fixedPoints, Insert.insert, Singleton.singleton, Iff.mp, Set.ncard, Set.ncard_eq_two, Dickson.coprime_order_two_fixed_points, Iff, HSMul.hSMul, Or, Iff.trans, Membership.mem, Set.ext_iff, of_eq_true, Eq.trans, True and 13 more
64 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
theorem Dickson.element_dichotomy line 131 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, Or, Eq, orderOf, Nat.Coprime
Proof uses: Ne, LT.lt.ne', IsOfFinOrder.orderOf_pos, Iff.mpr, IsOfFinOrder, Exists, And, LT.lt, HPow.hPow, isOfFinOrder_iff_pow_eq_one, Exists.intro, And.intro, orderOf_pos, Eq.mpr, id, congrArg, Eq.symm, Subgroup.coe_pow, pow_orderOf_eq_one, Subgroup.coe_one and 73 more
99 instances, coercions and auxiliary constants left out.

Tactic trace: 51 steps
Open to load the checked before-and-after goal states.
theorem Dickson.element_partition_count line 179 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, Eq, HSub.hSub, Nat.card, HAdd.hAdd and 5 more
Proof uses: Disjoint, Set, Eq.mpr, Not, id, False, Nat.Prime.ne_one, Fact.out, Eq.trans, Nat.gcd, Eq.symm, Nat.gcd_self, Eq.mp, congrArg, Equiv, Sum, Equiv.sumCompl, HMul.hMul, Unique, Unique.mk and 18 more
84 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Dickson.order_3_centralizes_order_5 line 202 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Finite, Subgroup, Eq, Nat, Nat.card, Subtype, Membership.mem, OfNat.ofNat, orderOf, Subgroup.Normal, HMul.hMul
Proof uses: dite, Eq.mpr, id, congrArg, mul_one, one_mul, Eq.refl, Not, Dvd.dvd, Eq.rec, Subgroup.zpowers, Subgroup.card_dvd_of_le, Iff.mpr, LE.le, Subgroup.zpowers_le, Eq.symm, Nat.card_zpowers, Or, Iff.mp, Nat.dvd_prime and 102 more
113 instances, coercions and auxiliary constants left out.

Tactic trace: 71 steps
Open to load the checked before-and-after goal states.
lemma Dickson.sylow_card_dvd_index line 274 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Finite, Nat, Fact, Nat.Prime, Eq, Nat.card, HMul.hMul, HPow.hPow, Finsupp, Nat.factorization, Dvd.dvd, Fintype.card, Sylow, Dickson.instFintypeSylow
Proof uses: Classical.arbitrary, Subgroup.index, Subtype, Membership.mem, Subgroup, Subgroup.index_mul_card, Nat.eq_of_mul_eq_mul_right, pow_pos, Nat.Prime.pos, Fact.out, Eq.mp, congrArg, Eq.trans, Sylow.card_eq_multiplicity, Eq.mpr, id, Eq.refl, Eq.symm, Nat.card_eq_fintype_card, Subgroup.normalizer and 3 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Dickson.sylow_5_options line 288 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Finite, Eq, Nat, Nat.card, OfNat.ofNat, Or, Fintype.card, Sylow, Dickson.instFintypeSylow
Proof uses: Dvd.dvd, Classical.arbitrary, Subgroup.index, HMul.hMul, Subtype, Membership.mem, Subgroup, Subgroup.index_mul_card, Nat.eq_of_mul_eq_mul_right, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Eq.mp, congrArg, Eq.trans, HPow.hPow, Finsupp, Nat.factorization and 47 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma Dickson.sylow_5_not_one line 306 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, Eq, Nat.card, Fintype.card, Sylow and 2 more
Proof uses: Mathlib.Tactic.Contrapose.contrapose₃, id, Not, And, Subgroup.Normal, Exists, Iff.mp, Fintype.card_eq_one_iff, Exists.intro, And.intro, Eq.mpr, HPow.hPow, Finsupp, Nat.factorization, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, congrArg and 48 more
83 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
lemma Dickson.normal_contains_all_sylow line 341 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Finite, Nat, Fact, Nat.Prime, Subgroup, Subgroup.Normal, Sylow, LE.le
Proof uses: Membership.mem, Eq, HSMul.hSMul, Exists, MulAction.exists_smul_eq, Dickson.instFintypeSylow, And, Set, MonoidHom, MulAut, Monoid.End, MulDistribMulAction.toMonoidEnd, MulAut.conj, Subgroup.Normal.conj_mem
32 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Dickson.order_15_unique_sylow_5 line 352 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Finite, Eq, Nat, Nat.card, OfNat.ofNat, Fintype.card, Sylow, Dickson.instFintypeSylow
Proof uses: Dvd.dvd, Classical.arbitrary, Subgroup.index, HMul.hMul, Subtype, Membership.mem, Subgroup, Subgroup.index_mul_card, Nat.eq_of_mul_eq_mul_right, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Eq.mp, congrArg, Eq.trans, HPow.hPow, Finsupp, Nat.factorization and 35 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
lemma Dickson.sylow_normal_of_unique_in_normal line 371 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Finite, Nat, Fact, Nat.Prime, Subgroup, Subgroup.Normal, Eq, Fintype.card, Sylow, Subtype, Membership.mem, Dickson.instFintypeSylow, OfNat.ofNat, Exists, Subgroup.map, Subgroup.subtype
Proof uses: Iff.mp, Fintype.card_eq_one_iff, Subgroup.Normal.mk, Eq.rec, HSMul.hSMul, HMul.hMul, Inv.inv, Subgroup.mem_map_of_mem, MonoidHom, MulAut, Monoid.End, MulDistribMulAction.toMonoidEnd, MulAut.conj, Subgroup.Characteristic, Sylow.characteristic_of_normal, Exists.intro
39 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Dickson.too_many_elements_of_prime_order line 382 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Finite, Nat, Fact, Nat.Prime, Eq, Nat.card, HMul.hMul, Fintype.card, Sylow, Dickson.instFintypeSylow, Ne, GE.ge, OfNat.ofNat, False
Proof uses: LT.lt, Or, lt_trichotomy, HMod.hMod, card_sylow_modEq_one, Eq.mp, congrArg, Nat.mod_eq_of_lt, Nat.Prime.one_lt, Fact.out, Nat.card_eq_fintype_card, rfl
19 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Dickson.order_30_n3_ne_10_of_n5_eq_6 line 398 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Finite, Eq, Nat, Nat.card, OfNat.ofNat, Fintype.card, Sylow, Dickson.instFintypeSylow, Ne
Proof uses: Eq.trans, Eq.symm, Nat.card_eq_fintype_card, Subtype, Membership.mem, Subgroup, Eq.mpr, HPow.hPow, Finsupp, Nat.factorization, id, congrArg, Sylow.card_eq_multiplicity, Dickson.instFactPrimeOfNatNat_fLT_2, pow_one, Eq.refl, Dickson.instFactPrimeOfNatNat_fLT_1, Finset, Finset.filter, And and 77 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 104 steps
Open to load the checked before-and-after goal states.
lemma Dickson.card_sup_of_coprime_normal line 500 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Finite, Subtype, Membership.mem, Subgroup.Normal, Nat.Coprime, Nat.card, Eq, Nat, Max.max, HMul.hMul
Proof uses: Eq.mpr, Prod, id, congrArg, Eq.symm, Nat.card_prod, Nat.card_congr, Equiv.ofBijective, Subtype.mk, Prod.fst, Prod.snd, Subgroup.mul_mem_sup, Subtype.property, And.intro, Function.Injective, Function.Surjective, Prod.mk, Iff.mp, Subtype.ext_iff, Inv.inv and 48 more
76 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
lemma Dickson.order_30_unique_sylow_5 line 535 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Finite, Eq, Nat, Nat.card, OfNat.ofNat, Fintype.card, Sylow, Dickson.instFintypeSylow
Proof uses: Decidable.byContradiction, Not, Or, Dvd.dvd, Classical.arbitrary, Subgroup.index, HMul.hMul, Subtype, Membership.mem, Subgroup, Subgroup.index_mul_card, Nat.eq_of_mul_eq_mul_right, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Eq.mp, congrArg, Eq.trans and 114 more
92 instances, coercions and auxiliary constants left out.

Tactic trace: 76 steps
Open to load the checked before-and-after goal states.
lemma Dickson.order_15_unique_sylow_3 line 602 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Finite, Eq, Nat, Nat.card, OfNat.ofNat, Fintype.card, Sylow, Dickson.instFintypeSylow
Proof uses: Dvd.dvd, Dickson.sylow_card_dvd_index, Dickson.instFactPrimeOfNatNat_fLT_1, rfl, HAdd.hAdd, HMul.hMul, Exists, Exists.intro, HDiv.hDiv, HMod.hMod, Eq.mpr, id, congrArg, Eq.symm, Nat.card_eq_fintype_card, card_sylow_modEq_one, Decidable.byContradiction, Not, LE.le, Nat.le_of_dvd and 27 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma Dickson.order_30_unique_sylow_3 line 614 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Finite, Eq, Nat, Nat.card, OfNat.ofNat, Fintype.card, Sylow, Dickson.instFintypeSylow
Proof uses: Dickson.order_30_unique_sylow_5, Subgroup, And, Subgroup.Normal, Subtype, Membership.mem, Exists, Iff.mp, Fintype.card_eq_one_iff, Exists.intro, And.intro, Subgroup.Normal.mk, Eq.rec, HSMul.hSMul, HMul.hMul, Inv.inv, Subgroup.mem_map_of_mem, MonoidHom, MulAut, Monoid.End and 83 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
lemma Dickson.no_normal_30_with_all_sylow3 line 654 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Finite, Eq, Nat, Nat.card, OfNat.ofNat, Subgroup, Subgroup.Normal, Subtype, Membership.mem, Fintype.card, Sylow, Dickson.instFintypeSylow, LE.le, False
Proof uses: Exists, Iff.mp, Fintype.card_eq_one_iff, Dickson.order_30_unique_sylow_3, Subgroup.map, Subgroup.subtype, Subgroup.subgroupOf, Eq.trans, Nat.card_congr, Equiv.mk, Subtype.mk, Subtype.property, rfl, HPow.hPow, Finsupp, Nat.factorization, Sylow.card_eq_multiplicity, Dickson.instFactPrimeOfNatNat_fLT_1, Eq.mpr, id and 23 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Dickson.no_normal_30_with_all_sylow5 line 678 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Finite, Eq, Nat, Nat.card, OfNat.ofNat, Subgroup, Subgroup.Normal, Subtype, Membership.mem, Fintype.card, Sylow, Dickson.instFintypeSylow, LE.le, False
Proof uses: Exists, Iff.mp, Fintype.card_eq_one_iff, Dickson.order_30_unique_sylow_5, Subgroup.map, Subgroup.subtype, Subgroup.subgroupOf, Eq.trans, Nat.card_congr, Equiv.mk, Subtype.mk, Subtype.property, rfl, HPow.hPow, Finsupp, Nat.factorization, Sylow.card_eq_multiplicity, Dickson.instFactPrimeOfNatNat_fLT_2, Eq.mpr, id and 23 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Dickson.normal_with_element_contains_all_sylow line 703 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Finite, Nat, Fact, Nat.Prime, Subgroup, Subgroup.Normal, Sylow, Eq, Nat.card, Subtype, Membership.mem, orderOf, LE.le
Proof uses: Subgroup.zpowers, Exists, IsPGroup.exists_le_sylow, IsPGroup.of_card, OfNat.ofNat, Eq.trans, HPow.hPow, Nat.card_zpowers, Eq.symm, pow_one, Subgroup.mem_zpowers, Set.ncard, Eq.le, Nat.card_coe_set_eq, Dickson.normal_contains_all_sylow, Eq.rec, Iff.mpr, Subgroup.zpowers_le, SetLike.ext', Set.eq_of_subset_of_ncard_le and 2 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Dickson.cauchy_element_in_subgroup line 723 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Finite, Nat, Fact, Nat.Prime, Subgroup, Dvd.dvd, Nat.card, Subtype, Membership.mem, Exists, And, Eq, orderOf
Proof uses: exists_prime_orderOf_dvd_card', Subtype.mk, Exists.intro, And.intro, Eq.trans, Subgroup.orderOf_coe
17 instances, coercions and auxiliary constants left out.
lemma Dickson.sylow_prime_pairwise_disjoint line 730 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Finite, Nat, Fact, Nat.Prime, Sylow, Eq, Nat.card, Subtype, Membership.mem, Subgroup, Ne, Min.min, Bot.bot
Proof uses: Dvd.dvd, Eq.rec, Subgroup.card_dvd_of_le, inf_le_left, OfNat.ofNat, Or, Iff.mp, Nat.dvd_prime, Fact.out, Subgroup.card_eq_one, SetLike.ext', Set.eq_of_subset_of_ncard_le, Set, Submonoid, Subgroup.toSubmonoid, Eq.le, Set.ncard, Eq.trans, Eq.symm, Nat.card_coe_set_eq and 5 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Dickson.card_ge_of_contains_all_sylow line 749 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Finite, Nat, Fact, Nat.Prime, Subgroup, Sylow, Eq, Nat.card, Subtype, Membership.mem, LE.le, Fintype.card, Dickson.instFintypeSylow, GE.ge, HAdd.hAdd, HMul.hMul, HSub.hSub, OfNat.ofNat
Proof uses: Finset, SDiff.sdiff, Set.toFinset, Set, Singleton.singleton, Set.PairwiseDisjoint, Finset.univ, Ne, Iff.mpr, Disjoint, Not, Finset.disjoint_left, And.right, Iff.mp, And, Finset.mem_sdiff, Finset.mem_singleton, Bot.bot, Subgroup.mem_bot, Eq.rec and 40 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma Dickson.normal_divides_4_eq_bot line 786 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Finite, Eq, Nat, Nat.card, OfNat.ofNat, Fintype.card, Sylow, Dickson.instFintypeSylow, Subgroup, Subgroup.Normal, Dvd.dvd, Subtype, Membership.mem, Ne, Bot.bot, False
Proof uses: Or, HasQuotient.Quotient, HMul.hMul, Eq.mpr, id, congrArg, Eq.symm, Subgroup.card_eq_card_quotient_mul_card_subgroup, Eq.refl, LE.le, Nat.le_of_dvd, Nat.zero_lt_succ, Nat.pos_of_ne_zero, Nat.succ_ne_zero, eq_zero_of_zero_dvd, Nat.succ, Eq.rec, dite, Or.inl, Nat.eq_of_mul_eq_mul_right and 75 more
76 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
lemma Dickson.sylow3_in_normal_forces_large line 823 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Finite, Eq, Nat, Fintype.card, Sylow, OfNat.ofNat, Dickson.instFintypeSylow, Nat.card, Subtype, Membership.mem, Subgroup, LE.le, Dvd.dvd, Ne
Proof uses: HMul.hMul, HAdd.hAdd, HSub.hSub, LE.le.trans, Nat.mul_le_mul_right, Dickson.card_ge_of_contains_all_sylow, Dickson.instFactPrimeOfNatNat_fLT_1, le_of_eq, Eq.symm, Decidable.byContradiction, Not, dite, le_antisymm, Nat.rawCast, Mathlib.Tactic.IntervalCases.of_le_right, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Nat.ge_of_not_lt, Nat.zero_le
34 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Dickson.sylow5_in_normal_forces_large line 837 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Finite, Eq, Nat, Fintype.card, Sylow, OfNat.ofNat, Dickson.instFintypeSylow, Nat.card, Subtype, Membership.mem, Subgroup, LE.le, Dvd.dvd, Ne
Proof uses: HMul.hMul, HAdd.hAdd, HSub.hSub, LE.le.trans, Nat.mul_le_mul_right, Dickson.card_ge_of_contains_all_sylow, Dickson.instFactPrimeOfNatNat_fLT_2, le_of_eq, Eq.symm, Decidable.byContradiction, Not, dite, le_antisymm, Nat.rawCast, Mathlib.Tactic.IntervalCases.of_le_right, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Nat.ge_of_not_lt, Nat.zero_le
34 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Dickson.is_simple_60_aux line 852 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Finite, Nontrivial, Eq, Nat, Nat.card, OfNat.ofNat, Fintype.card, Sylow, Dickson.instFintypeSylow, Subgroup, Subgroup.Normal, Or, Bot.bot, Top.top
Proof uses: Subtype, Membership.mem, Eq.trans, HPow.hPow, Finsupp, Nat.factorization, Sylow.card_eq_multiplicity, Dickson.instFactPrimeOfNatNat_fLT_1, Eq.mpr, id, congrArg, pow_one, Eq.refl, Dickson.instFactPrimeOfNatNat_fLT_2, dite, Or.inr, Subgroup.index, Eq.symm, propext, Subgroup.index_eq_one and 37 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
theorem Dickson.is_simple_60 line 885 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, Eq, Nat.card, Fintype.card, Sylow and 2 more
Proof uses: IsSimpleGroup.mk, Iff.mp, LT.lt, Nontrivial, Finite.one_lt_card_iff_nontrivial, Eq.rec, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Eq.symm, Subgroup.Normal, Dickson.is_simple_60_aux, Or.resolve_left, Dickson.sylow_5_options, Dickson.sylow_5_not_one
40 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Dickson.simple_group_faithful_action_on_sylow line 893 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Finite, IsSimpleGroup, Nat, Fact, Nat.Prime, Ne, Fintype.card, Sylow, Dickson.instFintypeSylow, OfNat.ofNat, Function.Injective, Equiv.Perm, MonoidHom, MulAction.toPermHom
Proof uses: Eq, Subgroup, MonoidHom.ker, Bot.bot, Top.top, Or, Subgroup.Normal.eq_bot_or_eq_top, Iff.mp, MonoidHom.ker_eq_bot_iff, absurd, Iff.mpr, Exists, Fintype.card_eq_one_iff, Exists.intro, Classical.arbitrary, HSMul.hSMul, MulAction.exists_smul_eq, Eq.rec, Eq.symm, DFunLike.congr_fun and 3 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Dickson.simple_60_n2_ne_15 line 905 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Finite, Eq, Nat, Nat.card, OfNat.ofNat, IsSimpleGroup, Ne, Fintype.card, Sylow, Dickson.instFintypeSylow
Proof uses: Classical.arbitrary, Subtype, Membership.mem, Subgroup, Eq.trans, HPow.hPow, Finsupp, Nat.factorization, Sylow.card_eq_multiplicity, Dickson.instFactPrimeOfNatNat_fLT, Eq.mpr, id, congrArg, Eq.refl, LE.le, Subgroup.normalizer, Subgroup.centralizer, Subgroup.index, Eq.symm, Sylow.card_eq_index_normalizer and 38 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
lemma Dickson.simple_60_n2_eq_5 line 934 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Finite, Eq, Nat, Nat.card, OfNat.ofNat, IsSimpleGroup, Fintype.card, Sylow, Dickson.instFintypeSylow
Proof uses: Dvd.dvd, Dickson.sylow_card_dvd_index, Dickson.instFactPrimeOfNatNat_fLT, rfl, Or, HAdd.hAdd, HMul.hMul, Exists, Exists.intro, HDiv.hDiv, HMod.hMod, Eq.mpr, id, congrArg, Eq.symm, Nat.card_eq_fintype_card, card_sylow_modEq_one, Decidable.byContradiction, Not, LE.le and 69 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 42 steps
Open to load the checked before-and-after goal states.
theorem Dickson.simple_60_is_A5 line 961 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Finite, Eq, Nat, Nat.card, OfNat.ofNat, IsSimpleGroup, Nonempty, MulEquiv, Subtype, Equiv.Perm, Fin, Membership.mem, Subgroup, alternatingGroup
Proof uses: MonoidHom, Sylow, MulAction.toPermHom, MonoidHom.range, MulEquiv.ofBijective, MonoidHom.rangeRestrict, And.intro, Function.Injective, Function.Surjective, Dickson.simple_group_faithful_action_on_sylow, Dickson.instFactPrimeOfNatNat_fLT, Eq.mpr, Ne, Fintype.card, Dickson.instFintypeSylow, id, congrArg, Dickson.simple_60_n2_eq_5, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat and 29 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
theorem Dickson.recognition_A5_proof line 978 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fact, Nat.Prime, GT.gt, OfNat.ofNat, Subgroup, Dickson.PGLOf, Dickson.K, ZMod, Matrix.GeneralLinearGroup, Fin, Matrix, Subgroup.center, Finite, Subtype, Membership.mem, Eq, Nat.card, Fintype.card, Sylow and 5 more
Proof uses: Dickson.simple_60_is_A5, Dickson.is_simple_60
36 instances, coercions and auxiliary constants left out.

FLT/Slop/PGL2/FiniteSubgroups/RecognitionA5.lean

Recognition of A₅ inside PGL₂(𝔽̄_p)

`FLT/Slop/PGL2/FiniteSubgroups/RecognitionA5.lean`

Recognition of `A₅` inside `PGL₂(𝔽̄_p)`