-- Mathlib/GroupTheory/SpecificGroups/ZGroup.lean
theorem isCyclic_commutator [Finite G] [IsZGroup G] : IsCyclic (commutator G)

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h✝ : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
h : Abelianization.of.ker ≤ Subgroup.center ↥(commutator ↥H)
⊢ IsCyclic ↥(commutator ↥H)

Tactic:
let _ := commGroupOfCyclicCenterQuotient Abelianization.of h

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h✝ : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
h : Abelianization.of.ker ≤ Subgroup.center ↥(commutator ↥H)
x✝ : CommGroup ↥(commutator ↥H) := commGroupOfCyclicCenterQuotient Abelianization.of h
⊢ IsCyclic ↥(commutator ↥H)

Proof state:
case inr
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h✝ : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
x✝ : CommGroup (MulAut ↥⁅commutator ↥H, commutator ↥H⁆) :=
  (IsCyclic.mulAutMulEquiv ↥⁅commutator ↥H, commutator ↥H⁆).toMonoidHom.commGroupOfInjective ⋯
h : commutator ↥⁅commutator ↥H, commutator ↥H⁆.normalizer ≤ ⁅commutator ↥H, commutator ↥H⁆.normalizerMonoidHom.ker
⊢ commutator ↥H ≤ Subgroup.centralizer ↑⁅commutator ↥H, commutator ↥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

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
this : IsCyclic ↥(commutator ↥H)
f : ↥(commutator ↥H) ≃* ↥⁅H, H⁆
⊢ IsCyclic ↥⁅H, H⁆

Tactic:
exact isCyclic_of_surjective f f.surjective

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
⊢ ∀ (x : Subgroup G), (∀ y < x, (fun H => IsCyclic ↥⁅H, H⁆) y) → (fun H => IsCyclic ↥⁅H, H⁆) x

Tactic:
intro H hH

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
hH : ∀ y < H, (fun H => IsCyclic ↥⁅H, H⁆) y
⊢ IsCyclic ↥⁅H, H⁆

Proof state:
case inr
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
⊢ Subgroup.map (commutator ↥H).subtype (commutator ↥(commutator ↥H)) ≤ Subgroup.centralizer ↑(commutator ↥H)

Tactic:
rw [Subgroup.map_subtype_commutator, Subgroup.le_centralizer_iff]

Result:
case inr
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
⊢ commutator ↥H ≤ Subgroup.centralizer ↑⁅commutator ↥H, commutator ↥H⁆

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
⊢ IsCyclic ↥(commutator G)

Tactic:
refine WellFoundedLT.induction (C := fun H ↦ IsCyclic (⁅H, H⁆ : Subgroup G)) (⊤ : Subgroup G) ?_

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
⊢ ∀ (x : Subgroup G), (∀ y < x, (fun H => IsCyclic ↥⁅H, H⁆) y) → (fun H => IsCyclic ↥⁅H, H⁆) x

Proof state:
case inl
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
hH : ∀ y < ⊥, (fun H => IsCyclic ↥⁅H, H⁆) y
⊢ IsCyclic ↥⁅⊥, ⊥⁆

Tactic:
rw [Subgroup.commutator_bot_left]

Result:
case inl
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
hH : ∀ y < ⊥, (fun H => IsCyclic ↥⁅H, H⁆) y
⊢ IsCyclic ↥⊥

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
hH : ∀ y < H, (fun H => IsCyclic ↥⁅H, H⁆) y
⊢ IsCyclic ↥⁅H, H⁆

Tactic:
rcases eq_or_ne H ⊥ with rfl | h

Result:
case inl
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
hH : ∀ y < ⊥, (fun H => IsCyclic ↥⁅H, H⁆) y
⊢ IsCyclic ↥⁅⊥, ⊥⁆

case inr
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
hH : ∀ y < H, (fun H => IsCyclic ↥⁅H, H⁆) y
h : H ≠ ⊥
⊢ IsCyclic ↥⁅H, H⁆

Proof state:
case inr
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
⊢ IsCyclic ↥⁅H, 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

Result:
case inr
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
⊢ IsCyclic ↥(commutator ↥H)

Proof state:
case inr
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
⊢ IsCyclic ↥(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

Result:
case inr
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
⊢ commutator ↥(commutator ↥H) ≤ Subgroup.center ↥(commutator ↥H)