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