G : Type u_1
H : Type ?u.22432
A : Type ?u.22435
a✝ a₁ a₂ b✝ c : G
inst✝ : Group G
s : Set G
hs : IsNormalSubgroup s
a b : G
hab : a * b ∈ s
h : a⁻¹ * (a * b) * a⁻¹⁻¹ ∈ s
⊢ b * a ∈ s
G : Type u_1
H : Type ?u.22432
A : Type ?u.22435
a✝ a₁ a₂ b✝ c : G
inst✝ : Group G
s : Set G
hs : IsNormalSubgroup s
a b : G
hab : a * b ∈ s
⊢ b * a ∈ s
have h : a⁻¹ * (a * b) * a⁻¹⁻¹ ∈ s := hs.normal (a * b) hab a⁻¹
G : Type u_1
H : Type ?u.22432
A : Type ?u.22435
a✝ a₁ a₂ b✝ c : G
inst✝ : Group G
s : Set G
hs : IsNormalSubgroup s
a b : G
hab : a * b ∈ s
h : b * a ∈ s
⊢ b * a ∈ s
G : Type u_1
H : Type ?u.22432
A : Type ?u.22435
a✝ a₁ a₂ b✝ c : G
inst✝ : Group G
s : Set G
hs : IsNormalSubgroup s
a b : G
hab : a * b ∈ s
h : a⁻¹ * (a * b) * a⁻¹⁻¹ ∈ s
⊢ b * a ∈ s
simp at h
no goals
G : Type u_1
H : Type ?u.22432
A : Type ?u.22435
a✝ a₁ a₂ b✝ c : G
inst✝ : Group G
s : Set G
hs : IsNormalSubgroup s
a b : G
hab : a * b ∈ s
h : b * a ∈ s
⊢ b * a ∈ s
exact h