R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
⊢ natDegree f = 0 ∨ M f
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
⊢ M f
suffices f.natDegree = 0 ∨ M f from Or.recOn this (fun h => (f0 h).elim) id
case refine_1
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
⊢ ∀ (a : R), natDegree (↑C a) = 0 ∨ M (↑C a)

case refine_2
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
⊢ ∀ (p q : R[X]), natDegree p = 0 ∨ M p → natDegree q = 0 ∨ M q → natDegree (p + q) = 0 ∨ M (p + q)

case refine_3
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
⊢ ∀ (n : ℕ) (a : R),
    natDegree (↑C a * X ^ n) = 0 ∨ M (↑C a * X ^ n) → natDegree (↑C a * X ^ (n + 1)) = 0 ∨ M (↑C a * X ^ (n + 1))
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
⊢ natDegree f = 0 ∨ M f
refine Polynomial.induction_on f ?_ ?_ ?_
no goals
case refine_1
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
⊢ ∀ (a : R), natDegree (↑C a) = 0 ∨ M (↑C a)
exact fun a => Or.inl (natDegree_C _)
case refine_2.inl.inl
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
p q : R[X]
hp : natDegree p = 0
hq : natDegree q = 0
⊢ natDegree (p + q) = 0 ∨ M (p + q)

case refine_2.inl.inr
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
p q : R[X]
hp : natDegree p = 0
hq : M q
⊢ natDegree (p + q) = 0 ∨ M (p + q)

case refine_2.inr.inl
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
p q : R[X]
hp : M p
hq : natDegree q = 0
⊢ natDegree (p + q) = 0 ∨ M (p + q)

case refine_2.inr.inr
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
p q : R[X]
hp : M p
hq : M q
⊢ natDegree (p + q) = 0 ∨ M (p + q)
case refine_2
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
⊢ ∀ (p q : R[X]), natDegree p = 0 ∨ M p → natDegree q = 0 ∨ M q → natDegree (p + q) = 0 ∨ M (p + q)
rintro p q (hp | hp) (hq | hq)
case refine_2.inl.inl
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
p q : R[X]
hp : natDegree p = 0
hq : natDegree q = 0
⊢ natDegree (p + q) = 0
case refine_2.inl.inl
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
p q : R[X]
hp : natDegree p = 0
hq : natDegree q = 0
⊢ natDegree (p + q) = 0 ∨ M (p + q)
refine' Or.inl _
no goals
case refine_2.inl.inl
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
p q : R[X]
hp : natDegree p = 0
hq : natDegree q = 0
⊢ natDegree (p + q) = 0
rw [eq_C_of_natDegree_eq_zero hp, eq_C_of_natDegree_eq_zero hq, ← C_add, natDegree_C]
case refine_2.inl.inr
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
p q : R[X]
hp : natDegree p = 0
hq : M q
⊢ M (p + q)
case refine_2.inl.inr
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
p q : R[X]
hp : natDegree p = 0
hq : M q
⊢ natDegree (p + q) = 0 ∨ M (p + q)
refine' Or.inr _
case refine_2.inl.inr
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
p q : R[X]
hp : natDegree p = 0
hq : M q
⊢ M (↑C (coeff p 0) + q)
case refine_2.inl.inr
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
p q : R[X]
hp : natDegree p = 0
hq : M q
⊢ M (p + q)
rw [eq_C_of_natDegree_eq_zero hp]
no goals
case refine_2.inl.inr
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
p q : R[X]
hp : natDegree p = 0
hq : M q
⊢ M (↑C (coeff p 0) + q)
exact h_C_add hq
case refine_2.inr.inl
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
p q : R[X]
hp : M p
hq : natDegree q = 0
⊢ M (p + q)
case refine_2.inr.inl
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
p q : R[X]
hp : M p
hq : natDegree q = 0
⊢ natDegree (p + q) = 0 ∨ M (p + q)
refine' Or.inr _
case refine_2.inr.inl
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
p q : R[X]
hp : M p
hq : natDegree q = 0
⊢ M (↑C (coeff q 0) + p)
case refine_2.inr.inl
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
p q : R[X]
hp : M p
hq : natDegree q = 0
⊢ M (p + q)
rw [eq_C_of_natDegree_eq_zero hq, add_comm]
no goals
case refine_2.inr.inl
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
p q : R[X]
hp : M p
hq : natDegree q = 0
⊢ M (↑C (coeff q 0) + p)
exact h_C_add hp
no goals
case refine_2.inr.inr
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
p q : R[X]
hp : M p
hq : M q
⊢ natDegree (p + q) = 0 ∨ M (p + q)
exact Or.inr (h_add hp hq)
case refine_3
R : Type u
S : Type v
T : Type w
A : Type z
a✝¹ b : R
n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
n : ℕ
a : R
a✝ : natDegree (↑C a * X ^ n) = 0 ∨ M (↑C a * X ^ n)
⊢ natDegree (↑C a * X ^ (n + 1)) = 0 ∨ M (↑C a * X ^ (n + 1))
case refine_3
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
⊢ ∀ (n : ℕ) (a : R),
    natDegree (↑C a * X ^ n) = 0 ∨ M (↑C a * X ^ n) → natDegree (↑C a * X ^ (n + 1)) = 0 ∨ M (↑C a * X ^ (n + 1))
intro n a _
case pos
R : Type u
S : Type v
T : Type w
A : Type z
a✝¹ b : R
n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
n : ℕ
a : R
a✝ : natDegree (↑C a * X ^ n) = 0 ∨ M (↑C a * X ^ n)
a0 : a = 0
⊢ natDegree (↑C a * X ^ (n + 1)) = 0 ∨ M (↑C a * X ^ (n + 1))

case neg
R : Type u
S : Type v
T : Type w
A : Type z
a✝¹ b : R
n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
n : ℕ
a : R
a✝ : natDegree (↑C a * X ^ n) = 0 ∨ M (↑C a * X ^ n)
a0 : ¬a = 0
⊢ natDegree (↑C a * X ^ (n + 1)) = 0 ∨ M (↑C a * X ^ (n + 1))
case refine_3
R : Type u
S : Type v
T : Type w
A : Type z
a✝¹ b : R
n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
n : ℕ
a : R
a✝ : natDegree (↑C a * X ^ n) = 0 ∨ M (↑C a * X ^ n)
⊢ natDegree (↑C a * X ^ (n + 1)) = 0 ∨ M (↑C a * X ^ (n + 1))
by_cases a0 : a = 0
no goals
case pos
R : Type u
S : Type v
T : Type w
A : Type z
a✝¹ b : R
n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
n : ℕ
a : R
a✝ : natDegree (↑C a * X ^ n) = 0 ∨ M (↑C a * X ^ n)
a0 : a = 0
⊢ natDegree (↑C a * X ^ (n + 1)) = 0 ∨ M (↑C a * X ^ (n + 1))
exact Or.inl (by rw [a0, C_0, zero_mul, natDegree_zero])
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a✝¹ b : R
n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
n : ℕ
a : R
a✝ : natDegree (↑C a * X ^ n) = 0 ∨ M (↑C a * X ^ n)
a0 : a = 0
⊢ natDegree (↑C a * X ^ (n + 1)) = 0
rw [a0, C_0, zero_mul, natDegree_zero]
case neg
R : Type u
S : Type v
T : Type w
A : Type z
a✝¹ b : R
n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
n : ℕ
a : R
a✝ : natDegree (↑C a * X ^ n) = 0 ∨ M (↑C a * X ^ n)
a0 : ¬a = 0
⊢ M (↑C a * X ^ (n + 1))
case neg
R : Type u
S : Type v
T : Type w
A : Type z
a✝¹ b : R
n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
n : ℕ
a : R
a✝ : natDegree (↑C a * X ^ n) = 0 ∨ M (↑C a * X ^ n)
a0 : ¬a = 0
⊢ natDegree (↑C a * X ^ (n + 1)) = 0 ∨ M (↑C a * X ^ (n + 1))
refine' Or.inr _
case neg
R : Type u
S : Type v
T : Type w
A : Type z
a✝¹ b : R
n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
n : ℕ
a : R
a✝ : natDegree (↑C a * X ^ n) = 0 ∨ M (↑C a * X ^ n)
a0 : ¬a = 0
⊢ M (↑(monomial (n + 1)) a)
case neg
R : Type u
S : Type v
T : Type w
A : Type z
a✝¹ b : R
n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
n : ℕ
a : R
a✝ : natDegree (↑C a * X ^ n) = 0 ∨ M (↑C a * X ^ n)
a0 : ¬a = 0
⊢ M (↑C a * X ^ (n + 1))
rw [C_mul_X_pow_eq_monomial]
no goals
case neg
R : Type u
S : Type v
T : Type w
A : Type z
a✝¹ b : R
n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
M : R[X] → Prop
f : R[X]
f0 : natDegree f ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (↑C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M (↑(monomial n) a)
n : ℕ
a : R
a✝ : natDegree (↑C a * X ^ n) = 0 ∨ M (↑C a * X ^ n)
a0 : ¬a = 0
⊢ M (↑(monomial (n + 1)) a)
exact h_monomial a0 n.succ_ne_zero