Theorem: Tutorial.Subgroup.mem_comm (Tutorial/Advanced/Algebra/Lecture5.lean)

State before:
G : Type
inst✝¹ : Group G
N : Subgroup G
inst✝ : Normal N
a b : G
⊢ a * b ∈ N → b * a ∈ N
Tactic:
intro hab
State after:
G : Type
inst✝¹ : Group G
N : Subgroup G
inst✝ : Normal N
a b : G
hab : a * b ∈ N
⊢ b * a ∈ N

State before:
G : Type
inst✝¹ : Group G
N : Subgroup G
inst✝ : Normal N
a b : G
hab : a * b ∈ N
⊢ b * a ∈ N
Tactic:
sorry
State after:
no goals