G : Type u
inst✝ : Group G
⊢ ⁅⁅Subgroup.centralizer (commutator G), Subgroup.centralizer (commutator G)⁆, ⊤⁆ = ⊥
G : Type u
inst✝ : Group G
⊢ ⁅Subgroup.centralizer (commutator G), Subgroup.centralizer (commutator G)⁆ ≤ Subgroup.center G
rw [← Subgroup.centralizer_top, ← Subgroup.commutator_eq_bot_iff_le_centralizer]
G : Type u
inst✝ : Group G
⊢ ⁅⁅⊤, Subgroup.centralizer (commutator G)⁆, Subgroup.centralizer (commutator G)⁆ = ⊥
G : Type u
inst✝ : Group G
⊢ ⁅⁅Subgroup.centralizer (commutator G), Subgroup.centralizer (commutator G)⁆, ⊤⁆ = ⊥
suffices ⁅⁅⊤, (commutator G).centralizer⁆, (commutator G).centralizer⁆ = ⊥ by
  refine' Subgroup.commutator_commutator_eq_bot_of_rotate _ this
  rwa [Subgroup.commutator_comm (commutator G).centralizer]
G : Type u
inst✝ : Group G
⊢ Subgroup.centralizer (commutator G) ≤ Subgroup.centralizer ⁅⊤, Subgroup.centralizer (commutator G)⁆
G : Type u
inst✝ : Group G
⊢ ⁅⁅⊤, Subgroup.centralizer (commutator G)⁆, Subgroup.centralizer (commutator G)⁆ = ⊥
rw [Subgroup.commutator_comm, Subgroup.commutator_eq_bot_iff_le_centralizer]
no goals
G : Type u
inst✝ : Group G
⊢ Subgroup.centralizer (commutator G) ≤ Subgroup.centralizer ⁅⊤, Subgroup.centralizer (commutator G)⁆
exact Set.centralizer_subset (Subgroup.commutator_mono le_top le_top)
G : Type u
inst✝ : Group G
this : ⁅⁅⊤, Subgroup.centralizer (commutator G)⁆, Subgroup.centralizer (commutator G)⁆ = ⊥
⊢ ⁅⁅Subgroup.centralizer (commutator G), ⊤⁆, Subgroup.centralizer (commutator G)⁆ = ⊥
G : Type u
inst✝ : Group G
this : ⁅⁅⊤, Subgroup.centralizer (commutator G)⁆, Subgroup.centralizer (commutator G)⁆ = ⊥
⊢ ⁅⁅Subgroup.centralizer (commutator G), Subgroup.centralizer (commutator G)⁆, ⊤⁆ = ⊥
refine' Subgroup.commutator_commutator_eq_bot_of_rotate _ this
no goals
G : Type u
inst✝ : Group G
this : ⁅⁅⊤, Subgroup.centralizer (commutator G)⁆, Subgroup.centralizer (commutator G)⁆ = ⊥
⊢ ⁅⁅Subgroup.centralizer (commutator G), ⊤⁆, Subgroup.centralizer (commutator G)⁆ = ⊥
rwa [Subgroup.commutator_comm (commutator G).centralizer]