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

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⁆
⊢ commutator ↥(commutator ↥H) ≤ Subgroup.center ↥(commutator ↥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

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⁆
⊢ Subgroup.map (commutator ↥H).subtype (commutator ↥(commutator ↥H)) ≤ Subgroup.centralizer ↑(commutator ↥H)

Proof state:
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⁆

Tactic:
specialize hH ⁅H, H⁆ (IsSolvable.commutator_lt_of_ne_bot h)

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

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

Tactic:
let f := Subgroup.equivMapOfInjective ⁅commutator H, commutator H⁆ _ H.subtype_injective

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic ↥⁅⁅H, H⁆, ⁅H, H⁆⁆
f : ↥⁅commutator ↥H, commutator ↥H⁆ ≃* ↥(Subgroup.map H.subtype ⁅commutator ↥H, commutator ↥H⁆) :=
  ⁅commutator ↥H, commutator ↥H⁆.equivMapOfInjective H.subtype ⋯
⊢ IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆

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)
x✝ : CommGroup ↥(commutator ↥H) := commGroupOfCyclicCenterQuotient Abelianization.of h
⊢ IsCyclic ↥(commutator ↥H)

Tactic:
infer_instance

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 ↥⁅⁅H, H⁆, ⁅H, H⁆⁆
f : ↥⁅commutator ↥H, commutator ↥H⁆ ≃* ↥(Subgroup.map H.subtype ⁅commutator ↥H, commutator ↥H⁆) :=
  ⁅commutator ↥H, commutator ↥H⁆.equivMapOfInjective H.subtype ⋯
⊢ IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆

Tactic:
rw [Subgroup.map_commutator, Subgroup.map_subtype_commutator] at f

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

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 : Subgroup.map (commutator ↥H).subtype (commutator ↥(commutator ↥H)) ≤ Subgroup.centralizer ↑(commutator ↥H)
⊢ commutator ↥(commutator ↥H) ≤ Subgroup.center ↥(commutator ↥H)

Tactic:
simpa [SetLike.le_def, Subgroup.mem_center_iff, Subgroup.mem_centralizer_iff] using 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 ↥⁅⁅H, H⁆, ⁅H, H⁆⁆
f : ↥⁅commutator ↥H, commutator ↥H⁆ ≃* ↥⁅⁅H, H⁆, ⁅H, H⁆⁆
⊢ IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆

Tactic:
exact isCyclic_of_surjective f.symm f.symm.surjective

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⁆
h : commutator ↥(commutator ↥H) ≤ Subgroup.center ↥(commutator ↥H)
⊢ IsCyclic ↥(commutator ↥H)

Tactic:
rw [← Abelianization.ker_of (commutator H)] at 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)
⊢ 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⁆
⊢ commutator ↥H ≤ Subgroup.centralizer ↑⁅commutator ↥H, commutator ↥H⁆

Tactic:
let _ := (hH.mulAutMulEquiv _).toMonoidHom.commGroupOfInjective (hH.mulAutMulEquiv _).injective

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⁆
x✝ : CommGroup (MulAut ↥⁅commutator ↥H, commutator ↥H⁆) :=
  (IsCyclic.mulAutMulEquiv ↥⁅commutator ↥H, commutator ↥H⁆).toMonoidHom.commGroupOfInjective ⋯
⊢ commutator ↥H ≤ Subgroup.centralizer ↑⁅commutator ↥H, 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 ⋯
⊢ commutator ↥H ≤ Subgroup.centralizer ↑⁅commutator ↥H, commutator ↥H⁆

Tactic:
have h := Abelianization.commutator_subset_ker ⁅commutator H, commutator H⁆.normalizerMonoidHom

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⁆
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⁆

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

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 ↥⁅H, H⁆

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)
⊢ IsCyclic ↥⁅H, H⁆

Tactic:
let f := Subgroup.equivMapOfInjective (commutator H) _ H.subtype_injective

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⁆
this : IsCyclic ↥(commutator ↥H)
f : ↥(commutator ↥H) ≃* ↥(Subgroup.map H.subtype (commutator ↥H)) := (commutator ↥H).equivMapOfInjective H.subtype ⋯
⊢ IsCyclic ↥⁅H, H⁆

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:
infer_instance

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) ≃* ↥(Subgroup.map H.subtype (commutator ↥H)) := (commutator ↥H).equivMapOfInjective H.subtype ⋯
⊢ IsCyclic ↥⁅H, H⁆

Tactic:
rw [Subgroup.map_subtype_commutator] at f

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⁆
this : IsCyclic ↥(commutator ↥H)
f : ↥(commutator ↥H) ≃* ↥⁅H, H⁆
⊢ IsCyclic ↥⁅H, H⁆