case zero
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r : R
⊢ ↑(monomial n) r * X ^ Nat.zero = ↑(monomial (n + Nat.zero)) r

case succ
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r : R
k : ℕ
ih : ↑(monomial n) r * X ^ k = ↑(monomial (n + k)) r
⊢ ↑(monomial n) r * X ^ Nat.succ k = ↑(monomial (n + Nat.succ k)) r
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r : R
k : ℕ
⊢ ↑(monomial n) r * X ^ k = ↑(monomial (n + k)) r
induction' k with k ih
no goals
case zero
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r : R
⊢ ↑(monomial n) r * X ^ Nat.zero = ↑(monomial (n + Nat.zero)) r
simp
no goals
case succ
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r : R
k : ℕ
ih : ↑(monomial n) r * X ^ k = ↑(monomial (n + k)) r
⊢ ↑(monomial n) r * X ^ Nat.succ k = ↑(monomial (n + Nat.succ k)) r
simp [ih, pow_succ', ← mul_assoc, add_assoc]