no goals
G : Type u_1
G' : Type ?u.412647
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.412656
inst✝ : AddGroup A
H K : Subgroup G
g : G
⊢ g ∈ centralizer H ↔ ∀ (h : G), h ∈ H → h * g * h⁻¹ * g⁻¹ = 1
simp only [mem_centralizer_iff, mul_inv_eq_iff_eq_mul, one_mul]