rw [Subgroup.mem_closure_singleton] at ha hb
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
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