no goals
G : Type u_1
G' : Type ?u.381690
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.381699
inst✝ : AddGroup A
H K : Subgroup G
g : G
h : g ∈ normalizer H
n : G
⊢ n * g ∈ H ↔ g * n ∈ H
rw [h, mul_assoc, mul_inv_cancel_right]
no goals
G : Type u_1
G' : Type ?u.381690
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.381699
inst✝ : AddGroup A
H K : Subgroup G
g : G
h : ∀ (n : G), n * g ∈ H ↔ g * n ∈ H
n : G
⊢ n ∈ H ↔ g * n * g⁻¹ ∈ H
rw [mul_assoc, ← h, inv_mul_cancel_right]