Theorem: Tutorial.Subgroup.mem_comm (Solution/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:
calc
  b * a = b * a⁻¹⁻¹ := by simp
  _ = a⁻¹ * (a * b) * a⁻¹⁻¹ := by simp
  _ ∈ N := by
    apply Normal.conj_mem a⁻¹ (a * b) hab
State after:
no goals

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

State before:
G : Type
inst✝¹ : Group G
N : Subgroup G
inst✝ : Normal N
a b : G
hab : a * b ∈ N
⊢ b * a⁻¹⁻¹ = a⁻¹ * (a * b) * a⁻¹⁻¹
Tactic:
simp
State after:
no goals

State before:
G : Type
inst✝¹ : Group G
N : Subgroup G
inst✝ : Normal N
a b : G
hab : a * b ∈ N
⊢ a⁻¹ * (a * b) * a⁻¹⁻¹ ∈ N
Tactic:
apply Normal.conj_mem a⁻¹ (a * b) hab
State after:
no goals