case zero
α : Type ?u.285909
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✝ : Ring R
n : ℤ
⊢ ↑(n ^ Nat.zero) = ↑n ^ Nat.zero

case succ
α : Type ?u.285909
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✝ : Ring R
n : ℤ
m : ℕ
ih : ↑(n ^ m) = ↑n ^ m
⊢ ↑(n ^ Nat.succ m) = ↑n ^ Nat.succ m
α : Type ?u.285909
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✝ : Ring R
n : ℤ
m : ℕ
⊢ ↑(n ^ m) = ↑n ^ m
induction' m with m ih
no goals
case zero
α : Type ?u.285909
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✝ : Ring R
n : ℤ
⊢ ↑(n ^ Nat.zero) = ↑n ^ Nat.zero
rw [pow_zero, pow_zero, Int.cast_one]
no goals
case succ
α : Type ?u.285909
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✝ : Ring R
n : ℤ
m : ℕ
ih : ↑(n ^ m) = ↑n ^ m
⊢ ↑(n ^ Nat.succ m) = ↑n ^ Nat.succ m
rw [pow_succ, pow_succ, Int.cast_mul, ih]