case zero
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.456883
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a : MvPolynomial σ R
⊢ totalDegree (a ^ Nat.zero) ≤ Nat.zero * totalDegree a

case succ
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.456883
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a : MvPolynomial σ R
n : ℕ
ih : totalDegree (a ^ n) ≤ n * totalDegree a
⊢ totalDegree (a ^ Nat.succ n) ≤ Nat.succ n * totalDegree a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.456883
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a : MvPolynomial σ R
n : ℕ
⊢ totalDegree (a ^ n) ≤ n * totalDegree a
induction' n with n ih
case succ
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.456883
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a : MvPolynomial σ R
n : ℕ
ih : totalDegree (a ^ n) ≤ n * totalDegree a
⊢ totalDegree (a * a ^ n) ≤ Nat.succ n * totalDegree a
case succ
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.456883
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a : MvPolynomial σ R
n : ℕ
ih : totalDegree (a ^ n) ≤ n * totalDegree a
⊢ totalDegree (a ^ Nat.succ n) ≤ Nat.succ n * totalDegree a
rw [pow_succ]
no goals
case succ
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.456883
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a : MvPolynomial σ R
n : ℕ
ih : totalDegree (a ^ n) ≤ n * totalDegree a
⊢ totalDegree (a * a ^ n) ≤ Nat.succ n * totalDegree a
calc
  totalDegree (a * a ^ n) ≤ a.totalDegree + (a ^ n).totalDegree := totalDegree_mul _ _
  _ ≤ a.totalDegree + n * a.totalDegree := (add_le_add_left ih _)
  _ = (n + 1) * a.totalDegree := by rw [add_mul, one_mul, add_comm]
no goals
case zero
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.456883
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a : MvPolynomial σ R
⊢ totalDegree (a ^ Nat.zero) ≤ Nat.zero * totalDegree a
simp only [Nat.zero_eq, MulZeroClass.zero_mul, pow_zero, totalDegree_one]
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.456883
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q a : MvPolynomial σ R
n : ℕ
ih : totalDegree (a ^ n) ≤ n * totalDegree a
⊢ totalDegree a + n * totalDegree a = (n + 1) * totalDegree a
rw [add_mul, one_mul, add_comm]