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

case succ
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
ih : ↑(monomial n) 1 = X ^ n
⊢ ↑(monomial (Nat.succ n)) 1 = X ^ Nat.succ n
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ ↑(monomial n) 1 = X ^ n
induction' n with n ih
no goals
case zero
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ ↑(monomial Nat.zero) 1 = X ^ Nat.zero
simp [monomial_zero_one]
no goals
case succ
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
ih : ↑(monomial n) 1 = X ^ n
⊢ ↑(monomial (Nat.succ n)) 1 = X ^ Nat.succ n
rw [pow_succ, ← ih, ← monomial_one_one_eq_X, monomial_mul_monomial, add_comm, one_mul]