case intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℤ
hn : 0 ≤ n
k : ℕ
hm : 0 ≤ ↑k
⊢ A ^ (↑k + n) = A ^ ↑k * A ^ n
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m n : ℤ
hm : 0 ≤ m
hn : 0 ≤ n
⊢ A ^ (m + n) = A ^ m * A ^ n
obtain ⟨k, rfl⟩ := eq_ofNat_of_zero_le hm
case intro.intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
k : ℕ
hm : 0 ≤ ↑k
l : ℕ
hn : 0 ≤ ↑l
⊢ A ^ (↑k + ↑l) = A ^ ↑k * A ^ ↑l
case intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℤ
hn : 0 ≤ n
k : ℕ
hm : 0 ≤ ↑k
⊢ A ^ (↑k + n) = A ^ ↑k * A ^ n
obtain ⟨l, rfl⟩ := eq_ofNat_of_zero_le hn
no goals
case intro.intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
k : ℕ
hm : 0 ≤ ↑k
l : ℕ
hn : 0 ≤ ↑l
⊢ A ^ (↑k + ↑l) = A ^ ↑k * A ^ ↑l
rw [← Int.ofNat_add, zpow_ofNat, zpow_ofNat, zpow_ofNat, pow_add]