case hz
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m : ℤ
⊢ a ^ (m + 0) = a ^ m * a ^ 0

case hp
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m : ℤ
n : ℕ
ihn : a ^ (m + ↑n) = a ^ m * a ^ ↑n
⊢ a ^ (m + (↑n + 1)) = a ^ m * a ^ (↑n + 1)

case hn
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m : ℤ
n : ℕ
ihn : a ^ (m + -↑n) = a ^ m * a ^ (-↑n)
⊢ a ^ (m + (-↑n - 1)) = a ^ m * a ^ (-↑n - 1)
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m n : ℤ
⊢ a ^ (m + n) = a ^ m * a ^ n
induction' n using Int.induction_on with n ihn n ihn
no goals
case hz
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m : ℤ
⊢ a ^ (m + 0) = a ^ m * a ^ 0
simp
no goals
case hp
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m : ℤ
n : ℕ
ihn : a ^ (m + ↑n) = a ^ m * a ^ ↑n
⊢ a ^ (m + (↑n + 1)) = a ^ m * a ^ (↑n + 1)
simp only [← add_assoc, zpow_add_one₀ ha, ihn, mul_assoc]
no goals
case hn
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m : ℤ
n : ℕ
ihn : a ^ (m + -↑n) = a ^ m * a ^ (-↑n)
⊢ a ^ (m + (-↑n - 1)) = a ^ m * a ^ (-↑n - 1)
rw [zpow_sub_one₀ ha, ← mul_assoc, ← ihn, ← zpow_sub_one₀ ha, add_sub_assoc]