Theorem: l1_2_17 (AlgebraI/Subgroups.lean)

State before:
G : Type u_1
inst✝ : Group G
g a b : G
ha : a ∈ Subgroup.closure {g}
hb : b ∈ Subgroup.closure {g}
⊢ a * b = b * a
Tactic:
rw [Subgroup.mem_closure_singleton] at ha hb
State after:
G : Type u_1
inst✝ : Group G
g a b : G
ha : ∃ n, g ^ n = a
hb : ∃ n, g ^ n = b
⊢ a * b = b * a

State before:
G : Type u_1
inst✝ : Group G
g a b : G
ha : ∃ n, g ^ n = a
hb : ∃ n, g ^ n = b
⊢ a * b = b * a
Tactic:
obtain ⟨n, rfl⟩ := ha
State after:
case intro
G : Type u_1
inst✝ : Group G
g b : G
hb : ∃ n, g ^ n = b
n : ℤ
⊢ g ^ n * b = b * g ^ n

State before:
case intro
G : Type u_1
inst✝ : Group G
g b : G
hb : ∃ n, g ^ n = b
n : ℤ
⊢ g ^ n * b = b * g ^ n
Tactic:
obtain ⟨m, rfl⟩ := hb
State after:
case intro.intro
G : Type u_1
inst✝ : Group G
g : G
n m : ℤ
⊢ g ^ n * g ^ m = g ^ m * g ^ n

State before:
case intro.intro
G : Type u_1
inst✝ : Group G
g : G
n m : ℤ
⊢ g ^ n * g ^ m = g ^ m * g ^ n
Tactic:
rw [← zpow_add, ← zpow_add, add_comm]
State after:
no goals