awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
P : Sylow p G := default
⊢ LE.le (α := ℕ) (((Nat.card G).factorization : (a : ℕ) → ℕ) p : ℕ)
    (((Monoid.exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
have rw : Monoid.exponent.{u_1} ↥(↑P : Subgroup G) ∣ Monoid.exponent G
Tactic: rw [← hp.pow_dvd_iff_le_factorization Monoid.exponent_ne_zero_of_finite,
      ← P.card_eq_multiplicity, ← (isZGroup p hp P).exponent_eq_card]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
f : G →* G'
f' : G' →* G''
inst_3 : Finite G
inst_4 : IsZGroup G
hG : Group.IsNilpotent G
⊢ IsCyclic G
have this : ∀ (p : ↥(Nat.card G).primeFactors), Fact (Nat.Prime (↑p : ℕ))
Tactic: have (p : { x // x ∈ (Nat.card G).primeFactors }) : Fact p.1.Prime :=
    ⟨Nat.prime_of_mem_primeFactors p.2⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
f : G →* G'
f' : G' →* G''
inst_3 : Finite G
inst_4 : IsZGroup G
hG : Group.IsNilpotent G
this : ∀ (p : ↥(Nat.card G).primeFactors), Fact (Nat.Prime (↑p : ℕ))
⊢ IsCyclic G
have obtain : ∀ (ϕ : ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) ≃* G), IsCyclic G
Tactic: obtain ⟨ϕ⟩ := ((Group.isNilpotent_of_finite_tfae (G := G)).out 0 4).mp hG
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
f : G →* G'
f' : G' →* G''
inst_3 : Finite G
inst_4 : IsZGroup G
hG : Group.IsNilpotent G
this : ∀ (p : ↥(Nat.card G).primeFactors), Fact (Nat.Prime (↑p : ℕ))
ϕ : ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) ≃* G
g h : G
⊢ g * h = h * g
have rw : Eq (α := (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
  ((ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) (g * h) :
    (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
  ((ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) (h * g) :
    (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
Tactic: rw [← ϕ.symm.injective.eq_iff, map_mul, mul_comm, ← map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
f : G →* G'
f' : G' →* G''
inst_3 : Finite G
inst_4 : IsZGroup G
hG : Group.IsNilpotent G
this : ∀ (p : ↥(Nat.card G).primeFactors), Fact (Nat.Prime (↑p : ℕ))
ϕ : ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) ≃* G
g h : G
rw :
  Eq (α := (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
    ((ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) (g * h) :
      (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
    ((ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) (h * g) :
      (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
⊢ g * h = h * g
have rw₁ : HMul.hMul (α := (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) (β :=
    (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
    ((ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) g :
      (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
    ((ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) h :
      (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) =
  (ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) (h * g)
Tactic: rw [← ϕ.symm.injective.eq_iff, map_mul, mul_comm, ← map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
f : G →* G'
f' : G' →* G''
inst_3 : Finite G
inst_4 : IsZGroup G
hG : Group.IsNilpotent G
this : ∀ (p : ↥(Nat.card G).primeFactors), Fact (Nat.Prime (↑p : ℕ))
ϕ : ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) ≃* G
g h : G
rw :
  Eq (α := (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
    ((ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) (g * h) :
      (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
    ((ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) (h * g) :
      (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
rw₁ :
  HMul.hMul (α := (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) (β :=
      (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
      ((ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) g :
        (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
      ((ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) h :
        (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) =
    (ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) (h * g)
⊢ g * h = h * g
have rw₂ : HMul.hMul (α := (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) (β :=
    (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
    ((ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) h :
      (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
    ((ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) g :
      (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) =
  (ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) (h * g)
Tactic: rw [← ϕ.symm.injective.eq_iff, map_mul, mul_comm, ← map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
f : G →* G'
f' : G' →* G''
inst_3 : Finite G
inst_4 : IsZGroup G
hG : Group.IsNilpotent G
this : ∀ (p : ↥(Nat.card G).primeFactors), Fact (Nat.Prime (↑p : ℕ))
ϕ : ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) ≃* G
g h : G
rw :
  Eq (α := (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
    ((ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) (g * h) :
      (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
    ((ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) (h * g) :
      (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
rw₁ :
  HMul.hMul (α := (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) (β :=
      (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
      ((ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) g :
        (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
      ((ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) h :
        (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) =
    (ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) (h * g)
rw₂ :
  HMul.hMul (α := (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) (β :=
      (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
      ((ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) h :
        (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
      ((ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) g :
        (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) =
    (ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) (h * g)
⊢ g * h = h * g
have rw₃ : Eq (α := (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
  ((ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) (h * g) :
    (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
  ((ϕ.symm : (a : G) → (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G)) (h * g) :
    (p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p : ℕ) G) → ↥(↑P : Subgroup G))
Tactic: rw [← ϕ.symm.injective.eq_iff, map_mul, mul_comm, ← map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
⊢ IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup G) ⊤ ⊤)
have ind : ∀ (H : Subgroup G) (hH : ∀ y < H, IsCyclic.{u_1} ↥⁅y, y⁆), IsCyclic.{u_1} ↥⁅H, H⁆
Tactic: induction (⊤ : Subgroup G) using WellFoundedLT.induction with | ind H hH
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
H : Subgroup G
hH : ∀ y < H, IsCyclic.{u_1} ↥⁅y, y⁆
⊢ IsCyclic.{u_1} ↥⁅H, H⁆
have ind : ∀ (hH : ∀ y < ⊥, IsCyclic.{u_1} ↥⁅y, y⁆), IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup G) ⊥ ⊥)
Tactic: rcases eq_or_ne H ⊥ with rfl | h
Cleared hypotheses: H, hH
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
H : Subgroup G
hH : ∀ y < H, IsCyclic.{u_1} ↥⁅y, y⁆
ind : ∀ (hH : ∀ y < ⊥, IsCyclic.{u_1} ↥⁅y, y⁆), IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup G) ⊥ ⊥)
⊢ IsCyclic.{u_1} ↥⁅H, H⁆
have ind₁ : ∀ (h : H ≠ ⊥), IsCyclic.{u_1} ↥⁅H, H⁆
Tactic: rcases eq_or_ne H ⊥ with rfl | h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
hH : ∀ y < ⊥, IsCyclic.{u_1} ↥⁅y, y⁆
⊢ IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup G) ⊥ ⊥)
have ind : IsCyclic.{u_1} ↥⊥
Tactic: rw [Subgroup.commutator_bot_left]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
H : Subgroup G
hH : ∀ y < H, IsCyclic.{u_1} ↥⁅y, y⁆
h : H ≠ ⊥
⊢ IsCyclic.{u_1} ↥⁅H, H⁆
have hH₁ : IsCyclic.{u_1} ↥⁅⁅H, H⁆, ⁅H, H⁆⁆
Tactic: specialize hH ⁅H, H⁆ (IsSolvable.commutator_lt_of_ne_bot h)
Cleared hypotheses: hH
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic.{u_1} ↥⁅⁅H, H⁆, ⁅H, H⁆⁆
f : ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) ≃*
  ↥(Subgroup.map H.subtype (Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))) :=
  Subgroup.equivMapOfInjective (Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) H.subtype ⋯
⊢ IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))
have rw : ∀ (f : ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) ≃* ↥⁅⁅H, H⁆, ⁅H, H⁆⁆),
  IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))
Tactic: rw [Subgroup.map_commutator, Subgroup.map_subtype_commutator] at f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic.{u_1} ↥⁅⁅H, H⁆, ⁅H, H⁆⁆
⊢ IsCyclic.{u_1} ↥⁅H, H⁆
have hH₁ : IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))
Tactic: replace hH : IsCyclic (⁅commutator H, commutator H⁆ : Subgroup H) := by
      let f := Subgroup.equivMapOfInjective ⁅commutator H, commutator H⁆ _ H.subtype_injective
      rw [Subgroup.map_commutator, Subgroup.map_subtype_commutator] at f
      exact isCyclic_of_surjective f.symm f.symm.surjective
Cleared hypotheses: hH
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))
this : IsCyclic.{u_1} ↥(commutator ↥H)
f : ↥(commutator ↥H) ≃* ↥(Subgroup.map H.subtype (commutator ↥H)) :=
  Subgroup.equivMapOfInjective (commutator ↥H) H.subtype ⋯
⊢ IsCyclic.{u_1} ↥⁅H, H⁆
have rw : ∀ (f : ↥(commutator ↥H) ≃* ↥⁅H, H⁆), IsCyclic.{u_1} ↥⁅H, H⁆
Tactic: rw [Subgroup.map_subtype_commutator] at f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))
⊢ IsCyclic.{u_1} ↥⁅H, H⁆
have ind : IsCyclic.{u_1} ↥(commutator ↥H)
Tactic: suffices IsCyclic (commutator H) by
      let f := Subgroup.equivMapOfInjective (commutator H) _ H.subtype_injective
      rw [Subgroup.map_subtype_commutator] at f
      exact isCyclic_of_surjective f f.surjective
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
H : Subgroup G
h_1 : H ≠ ⊥
hH : IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))
h : LE.le.{u_1} (α := Subgroup ↥(commutator ↥H)) (commutator ↥(commutator ↥H)) (Subgroup.center ↥(commutator ↥H))
⊢ IsCyclic.{u_1} ↥(commutator ↥H)
have h₁ : LE.le.{u_1} (α := Subgroup ↥(commutator ↥H)) (MonoidHom.ker Abelianization.of) (Subgroup.center ↥(commutator ↥H))
Tactic: rw [← Abelianization.ker_of (commutator H)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))
⊢ IsCyclic.{u_1} ↥(commutator ↥H)
have ind : LE.le.{u_1} (α := Subgroup ↥(commutator ↥H)) (commutator ↥(commutator ↥H)) (Subgroup.center ↥(commutator ↥H))
Tactic: suffices h : commutator (commutator H) ≤ Subgroup.center (commutator H) by
      rw [← Abelianization.ker_of (commutator H)] at h
      let _ := commGroupOfCyclicCenterQuotient Abelianization.of h
      infer_instance
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))
⊢ LE.le.{u_1} (α := Subgroup ↥(commutator ↥H)) (commutator ↥(commutator ↥H)) (Subgroup.center ↥(commutator ↥H))
have ind : LE.le (α := Subgroup ↥H)
  (Subgroup.map (G := ↥(commutator ↥H)) (Subgroup.subtype (commutator ↥H)) (commutator ↥(commutator ↥H)))
  (Subgroup.centralizer (↑(commutator ↥H) : Set ↥H))
Tactic: suffices h : (commutator (commutator H)).map (commutator H).subtype ≤
        Subgroup.centralizer (commutator H) by
      simpa [SetLike.le_def, Subgroup.mem_center_iff, Subgroup.mem_centralizer_iff] using h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))
⊢ LE.le (α := Subgroup ↥H)
    (Subgroup.map (G := ↥(commutator ↥H)) (Subgroup.subtype (commutator ↥H)) (commutator ↥(commutator ↥H)))
    (Subgroup.centralizer (↑(commutator ↥H) : Set ↥H))
have ind : LE.le (α := Subgroup ↥H) (commutator ↥H)
  (Subgroup.centralizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H))
Tactic: rw [Subgroup.map_subtype_commutator, Subgroup.le_centralizer_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))
x : CommGroup (MulAut ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))) :=
  MonoidHom.commGroupOfInjective
    (MulEquiv.toMonoidHom
      (IsCyclic.mulAutMulEquiv ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))))
    ⋯
⊢ LE.le (α := Subgroup ↥H) (commutator ↥H)
    (Subgroup.centralizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H))
have h₁ : LE.le.{u_1} (α :=
  Subgroup ↥(Subgroup.normalizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H)))
  (commutator ↥(Subgroup.normalizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H)))
  (MonoidHom.ker (Subgroup.normalizerMonoidHom (Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))))
Tactic: have h := Abelianization.commutator_subset_ker ⁅commutator H, commutator H⁆.normalizerMonoidHom
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
H : Subgroup G
h_1 : H ≠ ⊥
hH : IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))
x : CommGroup (MulAut ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))) :=
  MonoidHom.commGroupOfInjective
    (MulEquiv.toMonoidHom
      (IsCyclic.mulAutMulEquiv ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))))
    ⋯
h :
  LE.le.{u_1} (α :=
    Subgroup ↥(Subgroup.normalizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H)))
    (commutator ↥(Subgroup.normalizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H)))
    (MonoidHom.ker (Subgroup.normalizerMonoidHom (Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))))
⊢ LE.le (α := Subgroup ↥H) (commutator ↥H)
    (Subgroup.centralizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H))
have ind : ∀
  (h :
    LE.le (α :=
      Subgroup ↥(Subgroup.normalizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H)))
      (commutator
        ↥(Subgroup.normalizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H)))
      (Subgroup.subgroupOf
        (Subgroup.centralizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H))
        (Subgroup.normalizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H)))),
  LE.le (α := Subgroup ↥H) (commutator ↥H)
    (Subgroup.centralizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H))
Tactic: rwa [Subgroup.normalizerMonoidHom_ker, Subgroup.normalizer_eq_top,
      ← Subgroup.map_subtype_le_map_subtype, Subgroup.map_subtype_commutator,
        Subgroup.map_subgroupOf_eq_of_le le_top] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
H : Subgroup G
h_1 : H ≠ ⊥
hH : IsCyclic.{u_1} ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))
x : CommGroup (MulAut ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))) :=
  MonoidHom.commGroupOfInjective
    (MulEquiv.toMonoidHom
      (IsCyclic.mulAutMulEquiv ↥(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))))
    ⋯
h :
  LE.le.{u_1} (α :=
    Subgroup ↥(Subgroup.normalizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H)))
    (commutator ↥(Subgroup.normalizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H)))
    (MonoidHom.ker (Subgroup.normalizerMonoidHom (Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H))))
ind :
  ∀
    (h :
      LE.le (α :=
        Subgroup
          ↥(Subgroup.normalizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H)))
        (commutator
          ↥(Subgroup.normalizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H)))
        (Subgroup.subgroupOf
          (Subgroup.centralizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H))
          (Subgroup.normalizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H)))),
    LE.le (α := Subgroup ↥H) (commutator ↥H)
      (Subgroup.centralizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H))
⊢ LE.le (α := Subgroup ↥H) (commutator ↥H)
    (Subgroup.centralizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H))
have ind₁ : ∀
  (h :
    LE.le (α := Subgroup ↥⊤) (commutator ↥⊤)
      (Subgroup.subgroupOf
        (Subgroup.centralizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H)) ⊤)),
  LE.le (α := Subgroup ↥H) (commutator ↥H)
    (Subgroup.centralizer (↑(Bracket.bracket (L := Subgroup ↥H) (commutator ↥H) (commutator ↥H)) : Set ↥H))
Tactic: rwa [Subgroup.normalizerMonoidHom_ker, Subgroup.normalizer_eq_top,
      ← Subgroup.map_subtype_le_map_subtype, Subgroup.map_subtype_commutator,
        Subgroup.map_subgroupOf_eq_of_le le_top] at h
Cleared hypotheses: h