α : Type ?u.125817
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
b : G
m : ℤ
⊢ b ^ 1 * b ^ m = b ^ (m + 1)
α : Type ?u.125817
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
b : G
m : ℤ
⊢ b * b ^ m = b ^ (m + 1)
conv_lhs =>
  congr
  rw [← zpow_one b]
no goals
α : Type ?u.125817
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
b : G
m : ℤ
⊢ b ^ 1 * b ^ m = b ^ (m + 1)
rw [← zpow_add, add_comm]