[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ coeff (divX p) n = coeff p (n + 1)
[PROOFSTEP]
rw [add_comm]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ coeff (divX p) n = coeff p (1 + n)
[PROOFSTEP]
cases p
[GOAL]
case ofFinsupp
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff (divX { toFinsupp := toFinsupp✝ }) n = coeff { toFinsupp := toFinsupp✝ } (1 + n)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
⊢ ∀ (n : ℕ), coeff (divX p * X + ↑C (coeff p 0)) n = coeff p n
[PROOFSTEP]
rintro ⟨_ | _⟩
[GOAL]
case zero
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
⊢ coeff (divX p * X + ↑C (coeff p 0)) Nat.zero = coeff p Nat.zero
[PROOFSTEP]
simp [coeff_C, Nat.succ_ne_zero, coeff_mul_X]
[GOAL]
case succ
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n✝ : ℕ
⊢ coeff (divX p * X + ↑C (coeff p 0)) (Nat.succ n✝) = coeff p (Nat.succ n✝)
[PROOFSTEP]
simp [coeff_C, Nat.succ_ne_zero, coeff_mul_X]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
a : R
n : ℕ
⊢ coeff (divX (↑C a)) n = coeff 0 n
[PROOFSTEP]
simp [coeff_divX, coeff_C, Finsupp.single_eq_of_ne _]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
h : divX p = 0
⊢ p = ↑C (coeff p 0)
[PROOFSTEP]
simpa [eq_comm, h] using divX_mul_X_add p
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
h : p = ↑C (coeff p 0)
⊢ divX p = 0
[PROOFSTEP]
rw [h, divX_C]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ ∀ (n : ℕ), coeff (divX (p + q)) n = coeff (divX p + divX q) n
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
⊢ degree (divX p) < degree p
[PROOFSTEP]
haveI := Nontrivial.of_polynomial_ne hp0
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this : Nontrivial R
⊢ degree (divX p) < degree p
[PROOFSTEP]
calc
  degree (divX p) < (divX p * X + C (p.coeff 0)).degree :=
    if h : degree p ≤ 0 then
      by
      have h' : C (p.coeff 0) ≠ 0 := by rwa [← eq_C_of_degree_le_zero h]
      rw [eq_C_of_degree_le_zero h, divX_C, degree_zero, zero_mul, zero_add]
      exact lt_of_le_of_ne bot_le (Ne.symm (mt degree_eq_bot.1 <| by simpa using h'))
    else by
      have hXp0 : divX p ≠ 0 := by simpa [divX_eq_zero_iff, -not_le, degree_le_zero_iff] using h
      have : leadingCoeff (divX p) * leadingCoeff X ≠ 0 := by simpa
      have : degree (C (p.coeff 0)) < degree (divX p * X) :=
        calc
          degree (C (p.coeff 0)) ≤ 0 := degree_C_le
          _ < 1 := by decide
          _ = degree (X : R[X]) := degree_X.symm
          _ ≤ degree (divX p * X) := by
            rw [← zero_add (degree X), degree_mul' this]
            exact
              add_le_add
                (by
                  rw [zero_le_degree_iff, Ne.def, divX_eq_zero_iff]
                  exact fun h0 => h (h0.symm ▸ degree_C_le))
                le_rfl
      rw [degree_add_eq_left_of_degree_lt this]; exact degree_lt_degree_mul_X hXp0
  _ = degree p := congr_arg _ (divX_mul_X_add _)
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : degree p ≤ 0
⊢ degree (divX p) < degree (divX p * X + ↑C (coeff p 0))
[PROOFSTEP]
have h' : C (p.coeff 0) ≠ 0 := by rwa [← eq_C_of_degree_le_zero h]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : degree p ≤ 0
⊢ ↑C (coeff p 0) ≠ 0
[PROOFSTEP]
rwa [← eq_C_of_degree_le_zero h]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : degree p ≤ 0
h' : ↑C (coeff p 0) ≠ 0
⊢ degree (divX p) < degree (divX p * X + ↑C (coeff p 0))
[PROOFSTEP]
rw [eq_C_of_degree_le_zero h, divX_C, degree_zero, zero_mul, zero_add]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : degree p ≤ 0
h' : ↑C (coeff p 0) ≠ 0
⊢ ⊥ < degree (↑C (coeff (↑C (coeff p 0)) 0))
[PROOFSTEP]
exact lt_of_le_of_ne bot_le (Ne.symm (mt degree_eq_bot.1 <| by simpa using h'))
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : degree p ≤ 0
h' : ↑C (coeff p 0) ≠ 0
⊢ ¬↑C (coeff (↑C (coeff p 0)) 0) = 0
[PROOFSTEP]
simpa using h'
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : ¬degree p ≤ 0
⊢ degree (divX p) < degree (divX p * X + ↑C (coeff p 0))
[PROOFSTEP]
have hXp0 : divX p ≠ 0 := by simpa [divX_eq_zero_iff, -not_le, degree_le_zero_iff] using h
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : ¬degree p ≤ 0
⊢ divX p ≠ 0
[PROOFSTEP]
simpa [divX_eq_zero_iff, -not_le, degree_le_zero_iff] using h
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : ¬degree p ≤ 0
hXp0 : divX p ≠ 0
⊢ degree (divX p) < degree (divX p * X + ↑C (coeff p 0))
[PROOFSTEP]
have : leadingCoeff (divX p) * leadingCoeff X ≠ 0 := by simpa
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : ¬degree p ≤ 0
hXp0 : divX p ≠ 0
⊢ leadingCoeff (divX p) * leadingCoeff X ≠ 0
[PROOFSTEP]
simpa
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬degree p ≤ 0
hXp0 : divX p ≠ 0
this : leadingCoeff (divX p) * leadingCoeff X ≠ 0
⊢ degree (divX p) < degree (divX p * X + ↑C (coeff p 0))
[PROOFSTEP]
have : degree (C (p.coeff 0)) < degree (divX p * X) :=
  calc
    degree (C (p.coeff 0)) ≤ 0 := degree_C_le
    _ < 1 := by decide
    _ = degree (X : R[X]) := degree_X.symm
    _ ≤ degree (divX p * X) := by
      rw [← zero_add (degree X), degree_mul' this]
      exact
        add_le_add
          (by
            rw [zero_le_degree_iff, Ne.def, divX_eq_zero_iff]
            exact fun h0 => h (h0.symm ▸ degree_C_le))
          le_rfl
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬degree p ≤ 0
hXp0 : divX p ≠ 0
this : leadingCoeff (divX p) * leadingCoeff X ≠ 0
⊢ 0 < 1
[PROOFSTEP]
decide
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬degree p ≤ 0
hXp0 : divX p ≠ 0
this : leadingCoeff (divX p) * leadingCoeff X ≠ 0
⊢ degree X ≤ degree (divX p * X)
[PROOFSTEP]
rw [← zero_add (degree X), degree_mul' this]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬degree p ≤ 0
hXp0 : divX p ≠ 0
this : leadingCoeff (divX p) * leadingCoeff X ≠ 0
⊢ 0 + degree X ≤ degree (divX p) + degree X
[PROOFSTEP]
exact
  add_le_add
    (by
      rw [zero_le_degree_iff, Ne.def, divX_eq_zero_iff]
      exact fun h0 => h (h0.symm ▸ degree_C_le))
    le_rfl
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬degree p ≤ 0
hXp0 : divX p ≠ 0
this : leadingCoeff (divX p) * leadingCoeff X ≠ 0
⊢ 0 ≤ degree (divX p)
[PROOFSTEP]
rw [zero_le_degree_iff, Ne.def, divX_eq_zero_iff]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬degree p ≤ 0
hXp0 : divX p ≠ 0
this : leadingCoeff (divX p) * leadingCoeff X ≠ 0
⊢ ¬p = ↑C (coeff p 0)
[PROOFSTEP]
exact fun h0 => h (h0.symm ▸ degree_C_le)
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this✝¹ : Nontrivial R
h : ¬degree p ≤ 0
hXp0 : divX p ≠ 0
this✝ : leadingCoeff (divX p) * leadingCoeff X ≠ 0
this : degree (↑C (coeff p 0)) < degree (divX p * X)
⊢ degree (divX p) < degree (divX p * X + ↑C (coeff p 0))
[PROOFSTEP]
rw [degree_add_eq_left_of_degree_lt this]
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this✝¹ : Nontrivial R
h : ¬degree p ≤ 0
hXp0 : divX p ≠ 0
this✝ : leadingCoeff (divX p) * leadingCoeff X ≠ 0
this : degree (↑C (coeff p 0)) < degree (divX p * X)
⊢ degree (divX p) < degree (divX p * X)
[PROOFSTEP]
exact degree_lt_degree_mul_X hXp0
[GOAL]
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] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → coeff p 0 = 0 → a ≠ 0 → M p → M (p + ↑C a)
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
hp : ¬p = 0
⊢ M p
[PROOFSTEP]
have wf : degree (divX p) < degree p := degree_divX_lt hp
[GOAL]
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] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → coeff p 0 = 0 → a ≠ 0 → M p → M (p + ↑C a)
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
hp : ¬p = 0
wf : degree (divX p) < degree p
⊢ M p
[PROOFSTEP]
rw [← divX_mul_X_add p] at *
[GOAL]
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] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → coeff p 0 = 0 → a ≠ 0 → M p → M (p + ↑C a)
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
hp : ¬divX p * X + ↑C (coeff p 0) = 0
wf : degree (divX (divX p * X + ↑C (coeff p 0))) < degree (divX p * X + ↑C (coeff p 0))
⊢ M (divX p * X + ↑C (coeff p 0))
[PROOFSTEP]
exact
  if hcp0 : coeff p 0 = 0 then by
    rw [hcp0, C_0, add_zero]
    exact MX _ (fun h : divX p = 0 => by simp [h, hcp0] at hp ) (recOnHorner (divX p) M0 MC MX)
  else
    MC _ _ (coeff_mul_X_zero _) hcp0
      (if hpX0 : divX p = 0 then show M (divX p * X) by rw [hpX0, zero_mul]; exact M0
      else MX (divX p) hpX0 (recOnHorner _ M0 MC MX))
[GOAL]
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] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → coeff p 0 = 0 → a ≠ 0 → M p → M (p + ↑C a)
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
hp : ¬divX p * X + ↑C (coeff p 0) = 0
wf : degree (divX (divX p * X + ↑C (coeff p 0))) < degree (divX p * X + ↑C (coeff p 0))
hcp0 : coeff p 0 = 0
⊢ M (divX p * X + ↑C (coeff p 0))
[PROOFSTEP]
rw [hcp0, C_0, add_zero]
[GOAL]
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] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → coeff p 0 = 0 → a ≠ 0 → M p → M (p + ↑C a)
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
hp : ¬divX p * X + ↑C (coeff p 0) = 0
wf : degree (divX (divX p * X + ↑C (coeff p 0))) < degree (divX p * X + ↑C (coeff p 0))
hcp0 : coeff p 0 = 0
⊢ M (divX p * X)
[PROOFSTEP]
exact MX _ (fun h : divX p = 0 => by simp [h, hcp0] at hp ) (recOnHorner (divX p) M0 MC MX)
[GOAL]
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] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → coeff p 0 = 0 → a ≠ 0 → M p → M (p + ↑C a)
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
hp : ¬divX p * X + ↑C (coeff p 0) = 0
wf : degree (divX (divX p * X + ↑C (coeff p 0))) < degree (divX p * X + ↑C (coeff p 0))
hcp0 : coeff p 0 = 0
h : divX p = 0
⊢ False
[PROOFSTEP]
simp [h, hcp0] at hp
[GOAL]
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] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → coeff p 0 = 0 → a ≠ 0 → M p → M (p + ↑C a)
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
hp : ¬divX p * X + ↑C (coeff p 0) = 0
wf : degree (divX (divX p * X + ↑C (coeff p 0))) < degree (divX p * X + ↑C (coeff p 0))
hcp0 : ¬coeff p 0 = 0
hpX0 : divX p = 0
⊢ M (divX p * X)
[PROOFSTEP]
rw [hpX0, zero_mul]
[GOAL]
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] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → coeff p 0 = 0 → a ≠ 0 → M p → M (p + ↑C a)
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
hp : ¬divX p * X + ↑C (coeff p 0) = 0
wf : degree (divX (divX p * X + ↑C (coeff p 0))) < degree (divX p * X + ↑C (coeff p 0))
hcp0 : ¬coeff p 0 = 0
hpX0 : divX p = 0
⊢ M 0
[PROOFSTEP]
exact M0
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q : R[X]
P : R[X] → Prop
p : R[X]
h0 : 0 < degree p
hC : ∀ {a : R}, a ≠ 0 → P (↑C a * X)
hX : ∀ {p : R[X]}, 0 < degree p → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < degree p → P p → P (p + ↑C a)
h : 0 < degree 0
⊢ P 0
[PROOFSTEP]
rw [degree_zero] at h
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q : R[X]
P : R[X] → Prop
p : R[X]
h0 : 0 < degree p
hC : ∀ {a : R}, a ≠ 0 → P (↑C a * X)
hX : ∀ {p : R[X]}, 0 < degree p → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < degree p → P p → P (p + ↑C a)
h : 0 < ⊥
⊢ P 0
[PROOFSTEP]
exact absurd h (by decide)
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q : R[X]
P : R[X] → Prop
p : R[X]
h0 : 0 < degree p
hC : ∀ {a : R}, a ≠ 0 → P (↑C a * X)
hX : ∀ {p : R[X]}, 0 < degree p → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < degree p → P p → P (p + ↑C a)
h : 0 < ⊥
⊢ ¬0 < ⊥
[PROOFSTEP]
decide
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a✝ b : R
n : ℕ
inst✝ : Semiring R
p✝¹ q : R[X]
P : R[X] → Prop
p✝ : R[X]
h0✝ : 0 < degree p✝
hC : ∀ {a : R}, a ≠ 0 → P (↑C a * X)
hX : ∀ {p : R[X]}, 0 < degree p → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < degree p → P p → P (p + ↑C a)
p : R[X]
a : R
x✝¹ : coeff p 0 = 0
x✝ : a ≠ 0
ih : 0 < degree p → P p
h0 : 0 < degree (p + ↑C a)
h : 0 ≥ degree p
⊢ 0 < degree (↑C (?m.252251 p a x✝¹ x✝ ih h0 h))
[PROOFSTEP]
rwa [eq_C_of_degree_le_zero h, ← C_add] at h0
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝¹ q : R[X]
P : R[X] → Prop
p✝ : R[X]
h0✝ : 0 < degree p✝
hC : ∀ {a : R}, a ≠ 0 → P (↑C a * X)
hX : ∀ {p : R[X]}, 0 < degree p → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < degree p → P p → P (p + ↑C a)
p : R[X]
x✝ : p ≠ 0
ih : 0 < degree p → P p
h0' : 0 < degree (p * X)
h0 : ¬0 < degree p
⊢ P (p * X)
[PROOFSTEP]
rw [eq_C_of_degree_le_zero (le_of_not_gt h0)] at h0' ⊢
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝¹ q : R[X]
P : R[X] → Prop
p✝ : R[X]
h0✝ : 0 < degree p✝
hC : ∀ {a : R}, a ≠ 0 → P (↑C a * X)
hX : ∀ {p : R[X]}, 0 < degree p → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < degree p → P p → P (p + ↑C a)
p : R[X]
x✝ : p ≠ 0
ih : 0 < degree p → P p
h0' : 0 < degree (↑C (coeff p 0) * X)
h0 : ¬0 < degree p
⊢ P (↑C (coeff p 0) * X)
[PROOFSTEP]
exact hC fun h : coeff p 0 = 0 => by simp [h, Nat.not_lt_zero] at h0'
[GOAL]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝¹ q : R[X]
P : R[X] → Prop
p✝ : R[X]
h0✝ : 0 < degree p✝
hC : ∀ {a : R}, a ≠ 0 → P (↑C a * X)
hX : ∀ {p : R[X]}, 0 < degree p → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < degree p → P p → P (p + ↑C a)
p : R[X]
x✝ : p ≠ 0
ih : 0 < degree p → P p
h0' : 0 < degree (↑C (coeff p 0) * X)
h0 : ¬0 < degree p
h : coeff p 0 = 0
⊢ False
[PROOFSTEP]
simp [h, Nat.not_lt_zero] at h0'
[GOAL]
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
[PROOFSTEP]
suffices f.natDegree = 0 ∨ M f from Or.recOn this (fun h => (f0 h).elim) id
[GOAL]
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
[PROOFSTEP]
refine Polynomial.induction_on f ?_ ?_ ?_
[GOAL]
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)
[PROOFSTEP]
exact fun a => Or.inl (natDegree_C _)
[GOAL]
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)
[PROOFSTEP]
rintro p q (hp | hp) (hq | hq)
[GOAL]
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)
[PROOFSTEP]
refine' Or.inl _
[GOAL]
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
[PROOFSTEP]
rw [eq_C_of_natDegree_eq_zero hp, eq_C_of_natDegree_eq_zero hq, ← C_add, natDegree_C]
[GOAL]
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)
[PROOFSTEP]
refine' Or.inr _
[GOAL]
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)
[PROOFSTEP]
rw [eq_C_of_natDegree_eq_zero hp]
[GOAL]
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)
[PROOFSTEP]
exact h_C_add hq
[GOAL]
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)
[PROOFSTEP]
refine' Or.inr _
[GOAL]
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)
[PROOFSTEP]
rw [eq_C_of_natDegree_eq_zero hq, add_comm]
[GOAL]
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)
[PROOFSTEP]
exact h_C_add hp
[GOAL]
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)
[PROOFSTEP]
exact Or.inr (h_add hp hq)
[GOAL]
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))
[PROOFSTEP]
intro n a _
[GOAL]
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))
[PROOFSTEP]
by_cases a0 : a = 0
[GOAL]
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))
[PROOFSTEP]
exact Or.inl (by rw [a0, C_0, zero_mul, natDegree_zero])
[GOAL]
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
[PROOFSTEP]
rw [a0, C_0, zero_mul, natDegree_zero]
[GOAL]
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))
[PROOFSTEP]
refine' Or.inr _
[GOAL]
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))
[PROOFSTEP]
rw [C_mul_X_pow_eq_monomial]
[GOAL]
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)
[PROOFSTEP]
exact h_monomial a0 n.succ_ne_zero