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

47 declarations, 0 contain sorry, 0 declared as axioms

Random assortments of results on group theory.

Imports (3)

Imported by 6 files

abbrev MaximalPQuotient The maximal p-quotient of a group line 22 source
Source documentation
The maximal p-quotient of a group.
Note that the torsion free parts of G will not get quotiented out. So G / MaximalPQuotient is a p-group only when G is torsion free.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Nat
Proof uses: HasQuotient.Quotient, Subgroup, iInf, Subgroup.Normal, IsPGroup
3 instances, coercions and auxiliary constants left out.
```
abbrev MaximalPQuotient (G : Type*) [Group G] (p : ℕ) :=
…
```
instance (instance at line 25) line 25 source
abbrev MaximalPQuotient.mk Quotient map into the maximal p-quotient of a group line 31 source
Source documentation
Quotient map into the maximal p-quotient of a group.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Nat, MonoidHom, MaximalPQuotient, iInf, Subgroup, Subgroup.Normal, IsPGroup, HasQuotient.Quotient
Proof uses: QuotientGroup.mk'
12 instances, coercions and auxiliary constants left out.
```
abbrev MaximalPQuotient.mk (G : Type*) [Group G] (p : ℕ) : G →* MaximalPQuotient G p :=
…
```
Mentions: MaximalPQuotient
lemma MaximalPQuotient.mk_surjective line 34 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Nat, Function.Surjective, MaximalPQuotient, MonoidHom, iInf, Subgroup, Subgroup.Normal, IsPGroup, HasQuotient.Quotient, MaximalPQuotient.mk
Proof uses: QuotientGroup.mk'_surjective
14 instances, coercions and auxiliary constants left out.
lemma MaximalPQuotient.mk_eq_zero_of_pow_eq_zero line 37 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Nat, Eq, HPow.hPow, OfNat.ofNat, Nat.Coprime, MaximalPQuotient, MonoidHom, iInf, Subgroup, Subgroup.Normal, IsPGroup, HasQuotient.Quotient, MaximalPQuotient.mk
Proof uses: Eq.mpr, Membership.mem, id, Eq.trans, forall_congr, Eq.mp, orderOf, Nat.Coprime.of_dvd_right, orderOf_dvd_of_pow_eq_one, of_eq_true, True, congrFun', congrArg, eq_self, IsPGroup.orderOf_coprime
46 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Nat.exists_coprime_and_dvd_pow Also see IsPrincipalIdealRing.exists_isCoprime_and_dvd_pow line 45 source
Source comment
Also see `IsPrincipalIdealRing.exists_isCoprime_and_dvd_pow`

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Ne, OfNat.ofNat, Exists, And, Eq, HMul.hMul, Nat.Coprime, Dvd.dvd, HPow.hPow
Proof uses: UniqueFactorizationMonoid.induction_on_prime, False, rfl, Eq.refl, IsUnit, Exists.intro, of_eq_true, Eq.trans, True, congr, congrArg, one_mul, eq_self, Nat.coprime_one_left_eq_true, pow_zero, eq_true, IsUnit.dvd, and_self, Prime, dite and 28 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma Nat.exists_coprime_and_dvd_pow (a b : ℕ) (ha : a ≠ 0) :
    ∃ x y N, a = x * y ∧ x.Coprime b ∧ y ∣ b ^ N := by
…
```
lemma MaximalPQuotient.isPGroup_of_isMulTorsion The "maximal p-quotient" of (ℤ, +) is ℤ/⋂ₙ pⁿℤ = ℤ, not a p-group line 59 source
Source documentation
The "maximal p-quotient" of (ℤ, +) is ℤ/⋂ₙ pⁿℤ = ℤ, not a p-group.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Nat, IsMulTorsion, IsPGroup, MaximalPQuotient, iInf, Subgroup, Subgroup.Normal, HasQuotient.Quotient
Proof uses: Eq, MonoidHom, MaximalPQuotient.mk, Exists, HPow.hPow, OfNat.ofNat, MaximalPQuotient.mk_surjective, And, orderOf, HMul.hMul, Nat.Coprime, Dvd.dvd, Nat.exists_coprime_and_dvd_pow, LT.lt.ne', IsOfFinOrder.orderOf_pos, Exists.intro, Eq.mpr, id, congrArg, pow_mul and 8 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma MaximalPQuotient.isPGroup_of_isMulTorsion
    (G : Type*) [Group G] (p : ℕ) (hG : IsMulTorsion G) :
    IsPGroup p (MaximalPQuotient G p) := by
…
```
Mentions: MaximalPQuotient
lemma Subgroup.IsFiniteRelIndex.of_finite line 72 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Set.Finite, Subgroup.IsFiniteRelIndex
Proof uses: Finite, Subtype, Membership.mem, Iff.mpr, Subgroup.FiniteIndex, Subgroup.subgroupOf, Subgroup.isFiniteRelIndex_iff_finiteIndex, inferInstance
7 instances, coercions and auxiliary constants left out.
lemma Subgroup.finiteIndex_bot_iff line 78 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Iff, Subgroup.FiniteIndex, Bot.bot, Subgroup, Finite
Proof uses: Iff.trans, HasQuotient.Quotient, Subgroup.finiteIndex_iff_finite_quotient, Equiv.finite_iff, QuotientGroup.quotientEquivSelf
3 instances, coercions and auxiliary constants left out.
lemma Subgroup.isFiniteRelIndex_bot_iff line 83 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Iff, Subgroup.IsFiniteRelIndex, Bot.bot, Set.Finite
Proof uses: Iff.trans, Subgroup.FiniteIndex, Subtype, Membership.mem, Subgroup.subgroupOf, Subgroup.isFiniteRelIndex_iff_finiteIndex, Eq.mpr, Finite, id, Eq, congrFun', congrArg, Eq.trans, Subgroup.bot_subgroupOf, Iff.rfl
9 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma QuotientGroup.range_lift line 88 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Subgroup.Normal, MonoidHom, LE.le, MonoidHom.ker, Eq, MonoidHom.range, HasQuotient.Quotient, QuotientGroup.lift
Proof uses: Subgroup.ext, of_eq_true, Iff, Membership.mem, Eq.trans, Exists, True, congr, congrArg, propext, Function.Surjective.exists, QuotientGroup.mk_surjective, iff_self
24 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Subgroup.finite_map_of_isFiniteRelIndex line 93 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, MonoidHom, Subgroup, Subgroup.IsFiniteRelIndex, MonoidHom.ker, Set.Finite, Subgroup.map
Proof uses: HasQuotient.Quotient, Subtype, Membership.mem, Subgroup.subgroupOf, QuotientGroup.lift, MonoidHom.comp, Subgroup.subtype, of_eq_true, Eq.trans, Eq, OfNat.ofNat, True, congrFun', congrArg, id, Eq.mp, eq_self, Eq.mpr, Set.range, eq_of_heq and 11 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def Subgroup.quotientKerEquivMap First isomorphism theorem restricted to a subgroup line 102 source
Source documentation
First isomorphism theorem restricted to a subgroup.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, MonoidHom, Subgroup, MulEquiv, HasQuotient.Quotient, Subtype, Membership.mem, Subgroup.subgroupOf, MonoidHom.ker, Subgroup.map
Proof uses: QuotientGroup.liftEquiv, MonoidHom.codRestrict, MonoidHom.comp, Subgroup.subtype
26 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
noncomputable def Subgroup.quotientKerEquivMap {G G' : Type*} [Group G] [Group G']
    (φ : G →* G') (H : Subgroup G) :
    H ⧸ φ.ker.subgroupOf H ≃* H.map φ :=
…
```
lemma Subgroup.card_map_eq_relIndex_ker line 108 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, MonoidHom, Subgroup, Eq, Nat, Nat.card, Subtype, Membership.mem, Subgroup.map, Subgroup.relIndex, MonoidHom.ker
Proof uses: Nat.card_congr, HasQuotient.Quotient, Subgroup.subgroupOf, MulEquiv, MulEquiv.symm, Subgroup.quotientKerEquivMap
21 instances, coercions and auxiliary constants left out.
lemma orderOf_dvd_ncard line 113 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Set.Finite, Membership.mem, Dvd.dvd, Nat, orderOf, Set.ncard
Proof uses: Fintype, Nonempty, Eq, Set.Finite.nonempty_fintype, Nonempty.intro, Eq.mp, Subtype, Subtype.mk, Fintype.card, Nat.card, congr, congrArg, Subgroup.orderOf_mk, orderOf_dvd_card, Eq.refl
16 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Subgroup.prodToSupOfRight If K is contained in the centralizer of H, then H ⊔ K is given by HK and the map H × K → HK is a group homomorphism line 124 source
Source documentation
If K is contained in the centralizer of H, then H ⊔ K is given by HK and the map H × K → HK is a group homomorphism.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, LE.le, Subgroup.centralizer, MonoidHom, Prod, Subtype, Membership.mem, Max.max
Proof uses: MonoidHom.mk, OneHom.mk, Subtype.mk, HMul.hMul, Prod.fst, Prod.snd
44 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def Subgroup.prodToSupOfRight {G : Type*} [Group G] (H K : Subgroup G) (hK : K ≤ .centralizer H) :
    H × K →* ↑(H ⊔ K) where
…
```
lemma Subgroup.prodToSupOfRight_surjective line 130 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, LE.le, Subgroup.centralizer, Function.Surjective, Prod, Subtype, Membership.mem, Max.max, MonoidHom, Subgroup.prodToSupOfRight
Proof uses: Eq.mpr, Eq, MonoidHom.range, Top.top, id, congrArg, Eq.symm, propext, MonoidHom.range_eq_top, Subgroup.map, Subgroup.subtype, Function.Injective.eq_iff, Subgroup.map_injective, Subgroup.subtype_injective, MonoidHom.range_eq_map, LE.le.antisymm, Subgroup.map_le_range, And, MonoidHom.comp, Eq.trans and 17 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
def QuotientGroup.kerLift' The induced map from the quotient by the kernel to the codomain line 149 source
Source documentation
The induced map from the quotient by the kernel to the codomain.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Monoid, MonoidHom, HasQuotient.Quotient, Subgroup, MonoidHom.ker
Proof uses: QuotientGroup.lift
13 instances, coercions and auxiliary constants left out.
```
def QuotientGroup.kerLift' : G ⧸ ker φ →* H :=
…
```
theorem QuotientGroup.kerLift'_mk line 153 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Monoid, MonoidHom, Eq, HasQuotient.Quotient, Subgroup, MonoidHom.ker, QuotientGroup.kerLift'
Proof uses: rfl
20 instances, coercions and auxiliary constants left out.
theorem QuotientGroup.kerLift'_injective line 157 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Monoid, MonoidHom, Function.Injective, HasQuotient.Quotient, Subgroup, MonoidHom.ker, QuotientGroup.kerLift'
Proof uses: Quotient.inductionOn₂', QuotientGroup.leftRel, Eq, Quotient.sound', Eq.mpr, Membership.mem, HMul.hMul, Inv.inv, id, congrArg, propext, QuotientGroup.leftRel_apply, OfNat.ofNat, MonoidHom.mem_ker, MonoidHom.map_mul, Eq.symm, map_mul, inv_mul_cancel, map_one, Eq.refl
33 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Subgroup.le_ker_of_le_ker_of_coprime_relIndex line 164 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, CommMonoid, MonoidHom, Nat, Eq, HPow.hPow, OfNat.ofNat, Subgroup, Nat.Coprime, Subgroup.relIndex, LE.le, MonoidHom.ker
Proof uses: Classical.byCases, Bot.bot, dite, Classical.propDecidable, of_eq_true, Eq.trans, Top.top, True, congrArg, MonoidHom.ker_one, Not, Subgroup.IsFiniteRelIndex, Subgroup.IsFiniteRelIndex.mk, False.elim, False, Eq.mp, congrFun', id, Nat.card, Subtype and 31 more
57 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
def MonoidHom.liftOfRightInverseAux' Auxiliary definition used to define liftOfRightInverse line 192 source
Source documentation
Auxiliary definition used to define liftOfRightInverse

standard axioms: Quot.sound, propext what this means
Statement uses: Group, Monoid, MonoidHom, Function.RightInverse, LE.le, Subgroup, MonoidHom.ker
Proof uses: MonoidHom.mk, OneHom.mk
21 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
def liftOfRightInverseAux' (hf : Function.RightInverse f_inv f) (g : G₁ →* G₃)
    (hg : f.ker ≤ g.ker) :
    G₂ →* G₃ where
…
```
theorem MonoidHom.liftOfRightInverseAux'_comp_apply line 207 source
standard axioms: Quot.sound, propext what this means
Statement uses: Group, Monoid, MonoidHom, Function.RightInverse, LE.le, Subgroup, MonoidHom.ker, Eq, MonoidHom.liftOfRightInverseAux'
Proof uses: id, IsUnit.mul_left_injective, Inv.inv, IsUnit.map, Group.isUnit, Eq.mpr, HMul.hMul, OfNat.ofNat, congr, congrArg, Eq.trans, mul_inv_cancel, map_one, Eq.symm, inv_mul_cancel_right, one_mul, of_eq_true, True, eq_self
30 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
def MonoidHom.liftOfRightInverse' line 249 source
standard axioms: Quot.sound, propext what this means
Statement uses: Group, Monoid, MonoidHom, Function.RightInverse, Equiv, Subtype, LE.le, Subgroup, MonoidHom.ker
Proof uses: Equiv.mk, MonoidHom.liftOfRightInverseAux', Subtype.mk, MonoidHom.comp
23 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
abbrev MonoidHom.liftOfSurjective' line 265 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Monoid, MonoidHom, Function.Surjective, Equiv, Subtype, LE.le, Subgroup, MonoidHom.ker
Proof uses: MonoidHom.liftOfRightInverse', Function.surjInv
16 instances, coercions and auxiliary constants left out.
theorem MonoidHom.liftOfRightInverse'_comp_apply line 270 source
standard axioms: Quot.sound, propext what this means
Statement uses: Group, Monoid, MonoidHom, Function.RightInverse, Subtype, LE.le, Subgroup, MonoidHom.ker, Eq, Equiv, MonoidHom.liftOfRightInverse'
Proof uses: MonoidHom.liftOfRightInverseAux'_comp_apply, Subtype.property
22 instances, coercions and auxiliary constants left out.
theorem MonoidHom.liftOfRightInverse'_comp line 276 source
standard axioms: Quot.sound, propext what this means
Statement uses: Group, Monoid, MonoidHom, Function.RightInverse, Subtype, LE.le, Subgroup, MonoidHom.ker, Eq, MonoidHom.comp, Equiv, MonoidHom.liftOfRightInverse'
Proof uses: MonoidHom.ext, MonoidHom.liftOfRightInverse'_comp_apply
24 instances, coercions and auxiliary constants left out.
theorem MonoidHom.eq_liftOfRightInverse' line 281 source
standard axioms: Quot.sound, propext what this means
Statement uses: Group, Monoid, MonoidHom, Function.RightInverse, LE.le, Subgroup, MonoidHom.ker, Eq, MonoidHom.comp, Equiv, Subtype, MonoidHom.liftOfRightInverse', Subtype.mk
Proof uses: Eq.mpr, Eq.symm, id, congrArg, Subtype.mk.congr_simp, Equiv.symm, Equiv.apply_symm_apply
23 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Subgroup.inclusion_mk line 292 source
standard axioms: Quot.sound, propext what this means
Statement uses: Group, Subgroup, LE.le, Membership.mem, Eq, Subtype, MonoidHom, Subgroup.inclusion, Subtype.mk
Proof uses: rfl
28 instances, coercions and auxiliary constants left out.
lemma MonoidHom.ker_le_ker_comp line 295 source
standard axioms: Quot.sound, propext what this means
Statement uses: Group, Monoid, MonoidHom, LE.le, Subgroup, MonoidHom.ker, MonoidHom.comp
Proof uses: Membership.mem, of_eq_true, Eq.trans, Eq, OfNat.ofNat, True, congrFun', congrArg, id, Eq.mp, map_one, eq_self
20 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem ConjAct.toConjAct_inv_smul' line 298 source
standard axioms: Quot.sound, propext what this means
Statement uses: Group, Eq, HSMul.hSMul, ConjAct, Inv.inv, MulEquiv, ConjAct.toConjAct, HMul.hMul
Proof uses: Eq.mpr, id, congrArg, Eq.symm, ConjAct.toConjAct_inv, ConjAct.toConjAct_inv_smul, Eq.refl
35 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma map_inv_eq_iff line 302 source
standard axioms: propext what this means
Statement uses: FunLike, Group, Monoid, MonoidHomClass, Iff, Eq, Inv.inv
Proof uses: Eq.mpr, HMul.hMul, id, congrArg, Eq.symm, propext, IsUnit.mul_left_inj, IsUnit.map, Group.isUnit, IsUnit.mul_right_inj, of_eq_true, Eq.trans, True, congrFun', congr, OfNat.ofNat, inv_mul_cancel, map_one, mul_one, mul_inv_cancel_left and 1 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma map_inv_eq_map_comm line 307 source
standard axioms: propext what this means
Statement uses: FunLike, Group, Monoid, MonoidHomClass, Iff, Eq, Inv.inv
Proof uses: Eq.mpr, HMul.hMul, id, congrArg, Eq.symm, propext, IsUnit.mul_left_inj, IsUnit.map, Group.isUnit, iff_comm, IsUnit.mul_right_inj, of_eq_true, Eq.trans, OfNat.ofNat, True, congr, mul_inv_cancel, map_one, inv_mul_cancel, iff_self
25 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Units.range_map_subtype line 314 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monoid, Submonoid, Eq, Subgroup, Units, MonoidHom.range, Subtype, Membership.mem, Units.map, Submonoid.subtype, Submonoid.units
Proof uses: Subgroup.ext, Iff.intro, MonoidHom, of_eq_true, Eq.trans, And, Inv.inv, True, congr, congrArg, and_self, Set, Submonoid.comap, Units.coeHom, Submonoid.inv, Exists.intro, Units.mk, Subtype.mk, HMul.hMul, OfNat.ofNat and 9 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
instance (instance at line 321) line 321 source
lemma Group.dvd_natCard_iff_of_prime line 326 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Finite, Nat, Nat.Prime, Iff, Dvd.dvd, Nat.card, Exists, Eq, orderOf
Proof uses: Iff.intro, exists_prime_orderOf_dvd_card', Fact.mk, Eq.rec, Exists.choose, orderOf_dvd_natCard, Exists.choose_spec
6 instances, coercions and auxiliary constants left out.
lemma Group.not_dvd_natCard_iff_of_prime line 330 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Finite, Nat, Nat.Prime, Iff, Not, Dvd.dvd, Nat.card, Ne, orderOf
Proof uses: of_eq_true, Eq, Eq.trans, True, congrFun', congrArg, Exists, iff_self
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Subgroup.dvd_index_iff_of_prime line 334 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Subgroup.FiniteIndex, Subgroup.Normal, Nat, Nat.Prime, Iff, Dvd.dvd, Subgroup.index, Exists, And, Not, Membership.mem, HPow.hPow
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Nat.card, HasQuotient.Quotient, Eq, orderOf, MonoidHom, QuotientGroup.mk', OfNat.ofNat, funext, Ne, Monoid, propext, orderOf_eq_prime_iff, Fact.mk, Function.Surjective.exists, QuotientGroup.mk'_surjective and 2 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Subgroup.dvd_relIndex_iff_of_prime line 341 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Subgroup.Normal, Subtype, Membership.mem, Subgroup.subgroupOf, Subgroup.IsFiniteRelIndex, Nat, Nat.Prime, Iff, Dvd.dvd, Subgroup.relIndex, Exists, And, Not, HPow.hPow
Proof uses: Eq.mpr, id, Eq, congrFun', congrArg, Eq.trans, Subgroup.index, Subtype.mk, funext, congr, propext, exists_prop_congr, Iff.of_eq, Eq.refl
26 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
instance Subgroup.mulActionMulOppositeNormalizerQuotient line 346 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, MulAction, MulOpposite, Subtype, Membership.mem, Subgroup.normalizer, HasQuotient.Quotient
Proof uses: MulAction.mk, SemigroupAction.mk, SMul.mk, Quotient.map, QuotientGroup.leftRel, HMul.hMul, MulOpposite.unop
28 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma normalizer_smul_mk line 354 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, MulOpposite, Subtype, Membership.mem, Subgroup.normalizer, Eq, HasQuotient.Quotient, HSMul.hSMul, HMul.hMul, MulOpposite.unop
Proof uses: rfl
37 instances, coercions and auxiliary constants left out.
lemma mem_of_pow_mem_of_pow_mem_of_coprime line 357 source
standard axioms: Quot.sound, propext what this means
Statement uses: Group, Subgroup, Nat, Nat.Coprime, Membership.mem, HPow.hPow
Proof uses: Eq.mpr, Int, OfNat.ofNat, id, Eq, congrArg, Eq.symm, zpow_one, Nat.cast_one, Nat.gcd, Int.gcd, Int.gcd_natCast_natCast, HAdd.hAdd, HMul.hMul, Int.gcdA, Int.gcdB, Int.gcd_eq_gcd_ab, zpow_add, zpow_mul, zpow_natCast and 2 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MonoidHom.range_comp_eq_range line 363 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, MonoidHom, Function.Surjective, Eq, Subgroup, MonoidHom.range, MonoidHom.comp
Proof uses: Subgroup.ext, of_eq_true, Iff, Membership.mem, Eq.trans, Exists, True, congr, congrArg, propext, Function.Surjective.exists, iff_self
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MonoidHom.range_comp_mulEquiv line 368 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, MulEquiv, MonoidHom, Eq, Subgroup, MonoidHom.range, MonoidHom.comp
Proof uses: MonoidHom.range_comp_eq_range, MulEquiv.surjective
20 instances, coercions and auxiliary constants left out.
lemma IsUnit.unit_val_mul line 373 source
standard axioms: Classical.choice, propext what this means
Statement uses: Monoid, Units, IsUnit, HMul.hMul, Eq, IsUnit.unit
Proof uses: Units.ext, of_eq_true, eq_self
14 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MulEquivClass.coe_toMulEquiv line 377 source
standard axioms: Quot.sound what this means
Statement uses: Mul, EquivLike, MulEquivClass, Eq, MulEquiv
Proof uses: rfl
8 instances, coercions and auxiliary constants left out.
lemma Units.range_val line 381 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monoid, Eq, Set, Set.range, Units, Set.ofPred, IsUnit
Proof uses: Set.ext, Iff.intro, Membership.mem, Eq.rec, Units.isUnit, Exists.intro, IsUnit.unit, rfl
4 instances, coercions and auxiliary constants left out.