-- 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))
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))
ind₂ :
  ∀
    (h :
      LE.le (α := Subgroup ↥H) (Subgroup.map (G := ↥⊤) (Subgroup.subtype ⊤) (commutator ↥⊤))
        (Subgroup.map (G := ↥⊤) (Subgroup.subtype ⊤)
          (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))
⊢ 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 ↥H) (Bracket.bracket (L := Subgroup ↥H) ⊤ ⊤)
      (Subgroup.map (G := ↥⊤) (Subgroup.subtype ⊤)
        (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