-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
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))
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))
ind₄ ind₅ ind₆ ind₇ :
  ∀
    (h :
      LE.le (α := Subgroup ↥H) (Bracket.bracket (L := Subgroup ↥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))
⊢ 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

Premises used: Subgroup.map_subgroupOf_eq_of_le, Subgroup.normalizerMonoidHom_ker, Subgroup.normalizer_eq_top, Subgroup.map_subtype_le_map_subtype, le_top, Subgroup.map_subtype_commutator