[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p = 0
⊢ trailingDegree p = ⊤
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p ≠ 0
⊢ trailingDegree p = ↑(natTrailingDegree p)
[PROOFSTEP]
let ⟨n, hn⟩ := not_forall.1 (mt Option.eq_none_iff_forall_not_mem.2 (mt trailingDegree_eq_top.1 hp))
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p ≠ 0
n : ℕ
hn : ¬¬n ∈ trailingDegree p
⊢ trailingDegree p = ↑(natTrailingDegree p)
[PROOFSTEP]
have hn : trailingDegree p = n := Classical.not_not.1 hn
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p ≠ 0
n : ℕ
hn✝ : ¬¬n ∈ trailingDegree p
hn : trailingDegree p = ↑n
⊢ trailingDegree p = ↑(natTrailingDegree p)
[PROOFSTEP]
rw [natTrailingDegree, hn]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p ≠ 0
n : ℕ
hn✝ : ¬¬n ∈ trailingDegree p
hn : trailingDegree p = ↑n
⊢ ↑n = ↑(Option.getD (↑n) 0)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hp : p ≠ 0
⊢ trailingDegree p = ↑n ↔ natTrailingDegree p = n
[PROOFSTEP]
rw [trailingDegree_eq_natTrailingDegree hp]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hp : p ≠ 0
⊢ ↑(natTrailingDegree p) = ↑n ↔ natTrailingDegree p = n
[PROOFSTEP]
exact WithTop.coe_eq_coe
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
⊢ trailingDegree p = ↑n ↔ natTrailingDegree p = n
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
⊢ trailingDegree p = ↑n → natTrailingDegree p = n
[PROOFSTEP]
intro H
[GOAL]
case mp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
H : trailingDegree p = ↑n
⊢ natTrailingDegree p = n
[PROOFSTEP]
rwa [← trailingDegree_eq_iff_natTrailingDegree_eq]
[GOAL]
case mp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
H : trailingDegree p = ↑n
⊢ p ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : 0 < n
H : trailingDegree 0 = ↑n
⊢ False
[PROOFSTEP]
rw [trailingDegree_zero] at H 
[GOAL]
case mp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : 0 < n
H : ⊤ = ↑n
⊢ False
[PROOFSTEP]
exact Option.noConfusion H
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
⊢ natTrailingDegree p = n → trailingDegree p = ↑n
[PROOFSTEP]
intro H
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
H : natTrailingDegree p = n
⊢ trailingDegree p = ↑n
[PROOFSTEP]
rwa [trailingDegree_eq_iff_natTrailingDegree_eq]
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
H : natTrailingDegree p = n
⊢ p ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : 0 < n
H : natTrailingDegree 0 = n
⊢ False
[PROOFSTEP]
rw [natTrailingDegree_zero] at H 
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : 0 < n
H : 0 = n
⊢ False
[PROOFSTEP]
rw [H] at hn 
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : n < n
H : 0 = n
⊢ False
[PROOFSTEP]
exact lt_irrefl _ hn
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : trailingDegree p = ↑n
hp0 : p = 0
⊢ False
[PROOFSTEP]
rw [hp0] at h 
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : trailingDegree 0 = ↑n
hp0 : p = 0
⊢ False
[PROOFSTEP]
exact Option.noConfusion h
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : trailingDegree p = ↑n
hp0 : p ≠ 0
⊢ ↑(natTrailingDegree p) = ↑n
[PROOFSTEP]
rwa [← trailingDegree_eq_natTrailingDegree hp0]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ ↑(natTrailingDegree p) ≤ trailingDegree p
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p = 0
⊢ ↑(natTrailingDegree p) ≤ trailingDegree p
[PROOFSTEP]
rw [hp, trailingDegree_zero]
[GOAL]
case pos
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p = 0
⊢ ↑(natTrailingDegree 0) ≤ ⊤
[PROOFSTEP]
exact le_top
[GOAL]
case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : ¬p = 0
⊢ ↑(natTrailingDegree p) ≤ trailingDegree p
[PROOFSTEP]
rw [trailingDegree_eq_natTrailingDegree hp]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝¹ : Semiring R
p q✝ r : R[X]
inst✝ : Semiring S
q : S[X]
h : trailingDegree p = trailingDegree q
⊢ natTrailingDegree p = natTrailingDegree q
[PROOFSTEP]
unfold natTrailingDegree
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝¹ : Semiring R
p q✝ r : R[X]
inst✝ : Semiring S
q : S[X]
h : trailingDegree p = trailingDegree q
⊢ Option.getD (trailingDegree p) 0 = Option.getD (trailingDegree q) 0
[PROOFSTEP]
rw [h]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff p n ≠ 0
⊢ natTrailingDegree p ≤ n
[PROOFSTEP]
have : WithTop.some (natTrailingDegree p) = Nat.cast (natTrailingDegree p) := rfl
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff p n ≠ 0
this : ↑(natTrailingDegree p) = ↑(natTrailingDegree p)
⊢ natTrailingDegree p ≤ n
[PROOFSTEP]
rw [← WithTop.coe_le_coe, this, ← trailingDegree_eq_natTrailingDegree]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff p n ≠ 0
this : ↑(natTrailingDegree p) = ↑(natTrailingDegree p)
⊢ trailingDegree p ≤ ↑n
[PROOFSTEP]
exact le_trailingDegree_of_ne_zero h
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff p n ≠ 0
this : ↑(natTrailingDegree p) = ↑(natTrailingDegree p)
⊢ p ≠ 0
[PROOFSTEP]
intro h
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h✝ : coeff p n ≠ 0
this : ↑(natTrailingDegree p) = ↑(natTrailingDegree p)
h : p = 0
⊢ False
[PROOFSTEP]
subst h
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
q r : R[X]
h : coeff 0 n ≠ 0
this : ↑(natTrailingDegree 0) = ↑(natTrailingDegree 0)
⊢ False
[PROOFSTEP]
exact h rfl
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff q (natTrailingDegree p) ≠ 0
⊢ trailingDegree q ≤ trailingDegree p
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff q (natTrailingDegree p) ≠ 0
hp : p = 0
⊢ trailingDegree q ≤ trailingDegree p
[PROOFSTEP]
rw [hp]
[GOAL]
case pos
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff q (natTrailingDegree p) ≠ 0
hp : p = 0
⊢ trailingDegree q ≤ trailingDegree 0
[PROOFSTEP]
exact le_top
[GOAL]
case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff q (natTrailingDegree p) ≠ 0
hp : ¬p = 0
⊢ trailingDegree q ≤ trailingDegree p
[PROOFSTEP]
rw [trailingDegree_eq_natTrailingDegree hp]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff q (natTrailingDegree p) ≠ 0
hp : ¬p = 0
⊢ trailingDegree q ≤ ↑(natTrailingDegree p)
[PROOFSTEP]
exact le_trailingDegree_of_ne_zero h
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
⊢ natTrailingDegree p ≠ n → trailingDegree p ≠ ↑n
[PROOFSTEP]
have : Nat.cast n = WithTop.some n := rfl
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
this : ↑n = ↑n
⊢ natTrailingDegree p ≠ n → trailingDegree p ≠ ↑n
[PROOFSTEP]
exact mt fun h => by rw [natTrailingDegree, h, this, ← WithTop.some_eq_coe, Option.getD_some]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
this : ↑n = ↑n
h : trailingDegree p = ↑n
⊢ natTrailingDegree p = n
[PROOFSTEP]
rw [natTrailingDegree, h, this, ← WithTop.some_eq_coe, Option.getD_some]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hp : p ≠ 0
H : ↑n ≤ trailingDegree p
⊢ n ≤ natTrailingDegree p
[PROOFSTEP]
rw [trailingDegree_eq_natTrailingDegree hp] at H 
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hp : p ≠ 0
H : ↑n ≤ ↑(natTrailingDegree p)
⊢ n ≤ natTrailingDegree p
[PROOFSTEP]
exact WithTop.coe_le_coe.mp H
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
hq : q ≠ 0
hpq : trailingDegree p ≤ trailingDegree q
⊢ natTrailingDegree p ≤ natTrailingDegree q
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
hq : q ≠ 0
hpq : trailingDegree p ≤ trailingDegree q
hp : p = 0
⊢ natTrailingDegree p ≤ natTrailingDegree q
[PROOFSTEP]
rw [hp, natTrailingDegree_zero]
[GOAL]
case pos
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
hq : q ≠ 0
hpq : trailingDegree p ≤ trailingDegree q
hp : p = 0
⊢ 0 ≤ natTrailingDegree q
[PROOFSTEP]
exact zero_le _
[GOAL]
case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
hq : q ≠ 0
hpq : trailingDegree p ≤ trailingDegree q
hp : ¬p = 0
⊢ natTrailingDegree p ≤ natTrailingDegree q
[PROOFSTEP]
rw [trailingDegree_eq_natTrailingDegree hp, trailingDegree_eq_natTrailingDegree hq] at hpq 
[GOAL]
case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
hq : q ≠ 0
hpq : ↑(natTrailingDegree p) ≤ ↑(natTrailingDegree q)
hp : ¬p = 0
⊢ natTrailingDegree p ≤ natTrailingDegree q
[PROOFSTEP]
exact WithTop.coe_le_coe.1 hpq
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
ha : a ≠ 0
⊢ trailingDegree (↑(monomial n) a) = ↑n
[PROOFSTEP]
rw [trailingDegree, support_monomial n ha, min_singleton]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
ha : a ≠ 0
⊢ ↑n = ↑n
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
ha : a ≠ 0
⊢ natTrailingDegree (↑(monomial n) a) = n
[PROOFSTEP]
rw [natTrailingDegree, trailingDegree_monomial ha]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
ha : a ≠ 0
⊢ Option.getD (↑n) 0 = n
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
ha : a = 0
⊢ natTrailingDegree (↑(monomial n) a) ≤ n
[PROOFSTEP]
simp [ha]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
ha : a = 0
⊢ ↑n ≤ trailingDegree (↑(monomial n) a)
[PROOFSTEP]
simp [ha]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ 0 ≤ trailingDegree 1
[PROOFSTEP]
rw [← C_1]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ 0 ≤ trailingDegree (↑C 1)
[PROOFSTEP]
exact le_trailingDegree_C
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
⊢ natTrailingDegree ↑n = 0
[PROOFSTEP]
simp only [← C_eq_nat_cast, natTrailingDegree_C]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
ha : a ≠ 0
⊢ trailingDegree (↑C a * X ^ n) = ↑n
[PROOFSTEP]
rw [C_mul_X_pow_eq_monomial, trailingDegree_monomial ha]
[GOAL]
R : Type u
S : Type v
a✝ b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
a : R
⊢ ↑n ≤ trailingDegree (↑C a * X ^ n)
[PROOFSTEP]
rw [C_mul_X_pow_eq_monomial]
[GOAL]
R : Type u
S : Type v
a✝ b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
a : R
⊢ ↑n ≤ trailingDegree (↑(monomial n) a)
[PROOFSTEP]
exact le_trailingDegree_monomial
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : n < natTrailingDegree p
⊢ coeff p n = 0
[PROOFSTEP]
apply coeff_eq_zero_of_trailingDegree_lt
[GOAL]
case h
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : n < natTrailingDegree p
⊢ ↑n < trailingDegree p
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : n < natTrailingDegree p
hp : p = 0
⊢ ↑n < trailingDegree p
[PROOFSTEP]
rw [hp, trailingDegree_zero]
[GOAL]
case pos
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : n < natTrailingDegree p
hp : p = 0
⊢ ↑n < ⊤
[PROOFSTEP]
exact WithTop.coe_lt_top n
[GOAL]
case neg
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : n < natTrailingDegree p
hp : ¬p = 0
⊢ ↑n < trailingDegree p
[PROOFSTEP]
rw [trailingDegree_eq_natTrailingDegree hp]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : n < natTrailingDegree p
hp : ¬p = 0
⊢ ↑n < ↑(natTrailingDegree p)
[PROOFSTEP]
exact WithTop.coe_lt_coe.2 h
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
⊢ ↑n ≤ trailingDegree (X ^ n)
[PROOFSTEP]
simpa only [C_1, one_mul] using le_trailingDegree_C_mul_X_pow n (1 : R)
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p ≠ 0
⊢ natTrailingDegree p = min' (support p) (_ : Finset.Nonempty (support p))
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p ≠ 0
⊢ natTrailingDegree p ≤ min' (support p) (_ : Finset.Nonempty (support p))
[PROOFSTEP]
apply le_min'
[GOAL]
case a.H2
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p ≠ 0
⊢ ∀ (y : ℕ), y ∈ support p → natTrailingDegree p ≤ y
[PROOFSTEP]
intro y hy
[GOAL]
case a.H2
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p ≠ 0
y : ℕ
hy : y ∈ support p
⊢ natTrailingDegree p ≤ y
[PROOFSTEP]
exact natTrailingDegree_le_of_mem_supp y hy
[GOAL]
case a
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p ≠ 0
⊢ min' (support p) (_ : Finset.Nonempty (support p)) ≤ natTrailingDegree p
[PROOFSTEP]
apply Finset.min'_le
[GOAL]
case a.H2
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p ≠ 0
⊢ natTrailingDegree p ∈ support p
[PROOFSTEP]
exact mem_support_iff.mpr (trailingCoeff_nonzero_iff_nonzero.mpr h)
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p ≠ 0
hn : ∀ (m : ℕ), m < n → coeff p m = 0
⊢ n ≤ natTrailingDegree p
[PROOFSTEP]
rw [natTrailingDegree_eq_support_min' hp]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p ≠ 0
hn : ∀ (m : ℕ), m < n → coeff p m = 0
⊢ n ≤ min' (support p) (_ : Finset.Nonempty (support p))
[PROOFSTEP]
exact Finset.le_min' _ _ _ fun m hm => not_lt.1 fun hmn => mem_support_iff.1 hm <| hn _ hmn
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
⊢ natTrailingDegree p ≤ natDegree p
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p = 0
⊢ natTrailingDegree p ≤ natDegree p
[PROOFSTEP]
rw [hp, natDegree_zero, natTrailingDegree_zero]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : ¬p = 0
⊢ natTrailingDegree p ≤ natDegree p
[PROOFSTEP]
exact le_natDegree_of_ne_zero (mt trailingCoeff_eq_zero.mp hp)
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
n : ℕ
⊢ natTrailingDegree (p * X ^ n) = natTrailingDegree p + n
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
n : ℕ
⊢ natTrailingDegree (p * X ^ n) ≤ natTrailingDegree p + n
[PROOFSTEP]
refine' natTrailingDegree_le_of_ne_zero fun h => mt trailingCoeff_eq_zero.mp hp _
[GOAL]
case a
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
n : ℕ
h : coeff (p * X ^ n) (natTrailingDegree p + n) = 0
⊢ trailingCoeff p = 0
[PROOFSTEP]
rwa [trailingCoeff, ← coeff_mul_X_pow]
[GOAL]
case a
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
n : ℕ
⊢ natTrailingDegree p + n ≤ natTrailingDegree (p * X ^ n)
[PROOFSTEP]
rw [natTrailingDegree_eq_support_min' fun h => hp (mul_X_pow_eq_zero h), Finset.le_min'_iff]
[GOAL]
case a
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
n : ℕ
⊢ ∀ (y : ℕ), y ∈ support (p * X ^ n) → natTrailingDegree p + n ≤ y
[PROOFSTEP]
intro y hy
[GOAL]
case a
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
n y : ℕ
hy : y ∈ support (p * X ^ n)
⊢ natTrailingDegree p + n ≤ y
[PROOFSTEP]
have key : n ≤ y := by
  rw [mem_support_iff, coeff_mul_X_pow'] at hy 
  exact by_contra fun h => hy (if_neg h)
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
n y : ℕ
hy : y ∈ support (p * X ^ n)
⊢ n ≤ y
[PROOFSTEP]
rw [mem_support_iff, coeff_mul_X_pow'] at hy 
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
n y : ℕ
hy : (if n ≤ y then coeff p (y - n) else 0) ≠ 0
⊢ n ≤ y
[PROOFSTEP]
exact by_contra fun h => hy (if_neg h)
[GOAL]
case a
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
n y : ℕ
hy : y ∈ support (p * X ^ n)
key : n ≤ y
⊢ natTrailingDegree p + n ≤ y
[PROOFSTEP]
rw [mem_support_iff, coeff_mul_X_pow', if_pos key] at hy 
[GOAL]
case a
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
n y : ℕ
hy : coeff p (y - n) ≠ 0
key : n ≤ y
⊢ natTrailingDegree p + n ≤ y
[PROOFSTEP]
exact (le_tsub_iff_right key).mp (natTrailingDegree_le_of_ne_zero hy)
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ trailingDegree p + trailingDegree q ≤ trailingDegree (p * q)
[PROOFSTEP]
refine' Finset.le_min fun n hn => _
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : n ∈ support (p * q)
⊢ trailingDegree p + trailingDegree q ≤ ↑n
[PROOFSTEP]
rw [mem_support_iff, coeff_mul] at hn 
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : ∑ x in Nat.antidiagonal n, coeff p x.fst * coeff q x.snd ≠ 0
⊢ trailingDegree p + trailingDegree q ≤ ↑n
[PROOFSTEP]
obtain ⟨⟨i, j⟩, hij, hpq⟩ := exists_ne_zero_of_sum_ne_zero hn
[GOAL]
case intro.mk.intro
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : ∑ x in Nat.antidiagonal n, coeff p x.fst * coeff q x.snd ≠ 0
i j : ℕ
hij : (i, j) ∈ Nat.antidiagonal n
hpq : coeff p (i, j).fst * coeff q (i, j).snd ≠ 0
⊢ trailingDegree p + trailingDegree q ≤ ↑n
[PROOFSTEP]
refine'
  (add_le_add (min_le (mem_support_iff.mpr (left_ne_zero_of_mul hpq)))
        (min_le (mem_support_iff.mpr (right_ne_zero_of_mul hpq)))).trans
    (le_of_eq _)
[GOAL]
case intro.mk.intro
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : ∑ x in Nat.antidiagonal n, coeff p x.fst * coeff q x.snd ≠ 0
i j : ℕ
hij : (i, j) ∈ Nat.antidiagonal n
hpq : coeff p (i, j).fst * coeff q (i, j).snd ≠ 0
⊢ ↑(i, j).fst + ↑(i, j).snd = ↑n
[PROOFSTEP]
rwa [← WithTop.coe_add, WithTop.coe_eq_coe, ← Nat.mem_antidiagonal]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p * q ≠ 0
⊢ natTrailingDegree p + natTrailingDegree q ≤ natTrailingDegree (p * q)
[PROOFSTEP]
have hp : p ≠ 0 := fun hp => h (by rw [hp, zero_mul])
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p * q ≠ 0
hp : p = 0
⊢ p * q = 0
[PROOFSTEP]
rw [hp, zero_mul]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p * q ≠ 0
hp : p ≠ 0
⊢ natTrailingDegree p + natTrailingDegree q ≤ natTrailingDegree (p * q)
[PROOFSTEP]
have hq : q ≠ 0 := fun hq =>
  h
    (by rw [hq, mul_zero])
      -- Porting note: Needed to account for different coercion behaviour & add the lemma below
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p * q ≠ 0
hp : p ≠ 0
hq : q = 0
⊢ p * q = 0
[PROOFSTEP]
rw [hq, mul_zero]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ natTrailingDegree p + natTrailingDegree q ≤ natTrailingDegree (p * q)
[PROOFSTEP]
have : ∀ (p : R[X]), WithTop.some (natTrailingDegree p) = Nat.cast (natTrailingDegree p) := fun p ↦ rfl
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
this : ∀ (p : R[X]), ↑(natTrailingDegree p) = ↑(natTrailingDegree p)
⊢ natTrailingDegree p + natTrailingDegree q ≤ natTrailingDegree (p * q)
[PROOFSTEP]
rw [← WithTop.coe_le_coe, WithTop.coe_add, this p, this q, this (p * q), ← trailingDegree_eq_natTrailingDegree hp, ←
  trailingDegree_eq_natTrailingDegree hq, ← trailingDegree_eq_natTrailingDegree h]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
this : ∀ (p : R[X]), ↑(natTrailingDegree p) = ↑(natTrailingDegree p)
⊢ trailingDegree p + trailingDegree q ≤ trailingDegree (p * q)
[PROOFSTEP]
exact le_trailingDegree_mul
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ coeff (p * q) (natTrailingDegree p + natTrailingDegree q) = trailingCoeff p * trailingCoeff q
[PROOFSTEP]
rw [coeff_mul]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ ∑ x in Nat.antidiagonal (natTrailingDegree p + natTrailingDegree q), coeff p x.fst * coeff q x.snd =
    trailingCoeff p * trailingCoeff q
[PROOFSTEP]
refine'
  Finset.sum_eq_single (p.natTrailingDegree, q.natTrailingDegree) _ fun h => (h (Nat.mem_antidiagonal.mpr rfl)).elim
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ ∀ (b : ℕ × ℕ),
    b ∈ Nat.antidiagonal (natTrailingDegree p + natTrailingDegree q) →
      b ≠ (natTrailingDegree p, natTrailingDegree q) → coeff p b.fst * coeff q b.snd = 0
[PROOFSTEP]
rintro ⟨i, j⟩ h₁ h₂
[GOAL]
case mk
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
i j : ℕ
h₁ : (i, j) ∈ Nat.antidiagonal (natTrailingDegree p + natTrailingDegree q)
h₂ : (i, j) ≠ (natTrailingDegree p, natTrailingDegree q)
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
[PROOFSTEP]
rw [Nat.mem_antidiagonal] at h₁ 
[GOAL]
case mk
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natTrailingDegree p + natTrailingDegree q
h₂ : (i, j) ≠ (natTrailingDegree p, natTrailingDegree q)
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
[PROOFSTEP]
by_cases hi : i < p.natTrailingDegree
[GOAL]
case pos
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natTrailingDegree p + natTrailingDegree q
h₂ : (i, j) ≠ (natTrailingDegree p, natTrailingDegree q)
hi : i < natTrailingDegree p
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
[PROOFSTEP]
rw [coeff_eq_zero_of_lt_natTrailingDegree hi, zero_mul]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natTrailingDegree p + natTrailingDegree q
h₂ : (i, j) ≠ (natTrailingDegree p, natTrailingDegree q)
hi : ¬i < natTrailingDegree p
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
[PROOFSTEP]
by_cases hj : j < q.natTrailingDegree
[GOAL]
case pos
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natTrailingDegree p + natTrailingDegree q
h₂ : (i, j) ≠ (natTrailingDegree p, natTrailingDegree q)
hi : ¬i < natTrailingDegree p
hj : j < natTrailingDegree q
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
[PROOFSTEP]
rw [coeff_eq_zero_of_lt_natTrailingDegree hj, mul_zero]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natTrailingDegree p + natTrailingDegree q
h₂ : (i, j) ≠ (natTrailingDegree p, natTrailingDegree q)
hi : ¬i < natTrailingDegree p
hj : ¬j < natTrailingDegree q
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
[PROOFSTEP]
rw [not_lt] at hi hj 
[GOAL]
case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natTrailingDegree p + natTrailingDegree q
h₂ : (i, j) ≠ (natTrailingDegree p, natTrailingDegree q)
hi : natTrailingDegree p ≤ i
hj : natTrailingDegree q ≤ j
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
[PROOFSTEP]
refine' (h₂ (Prod.ext_iff.mpr _).symm).elim
[GOAL]
case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natTrailingDegree p + natTrailingDegree q
h₂ : (i, j) ≠ (natTrailingDegree p, natTrailingDegree q)
hi : natTrailingDegree p ≤ i
hj : natTrailingDegree q ≤ j
⊢ (natTrailingDegree p, natTrailingDegree q).fst = (i, j).fst ∧
    (natTrailingDegree p, natTrailingDegree q).snd = (i, j).snd
[PROOFSTEP]
exact (add_eq_add_iff_eq_and_eq hi hj).mp h₁.symm
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
⊢ trailingDegree (p * q) = trailingDegree p + trailingDegree q
[PROOFSTEP]
have hp : p ≠ 0 := fun hp => h (by rw [hp, trailingCoeff_zero, zero_mul])
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p = 0
⊢ trailingCoeff p * trailingCoeff q = 0
[PROOFSTEP]
rw [hp, trailingCoeff_zero, zero_mul]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
⊢ trailingDegree (p * q) = trailingDegree p + trailingDegree q
[PROOFSTEP]
have hq : q ≠ 0 := fun hq => h (by rw [hq, trailingCoeff_zero, mul_zero])
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q = 0
⊢ trailingCoeff p * trailingCoeff q = 0
[PROOFSTEP]
rw [hq, trailingCoeff_zero, mul_zero]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ trailingDegree (p * q) = trailingDegree p + trailingDegree q
[PROOFSTEP]
refine' le_antisymm _ le_trailingDegree_mul
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ trailingDegree (p * q) ≤ trailingDegree p + trailingDegree q
[PROOFSTEP]
rw [trailingDegree_eq_natTrailingDegree hp, trailingDegree_eq_natTrailingDegree hq, ← ENat.coe_add]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ trailingDegree (p * q) ≤ ↑(natTrailingDegree p + natTrailingDegree q)
[PROOFSTEP]
apply le_trailingDegree_of_ne_zero
[GOAL]
case h
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ coeff (p * q) (natTrailingDegree p + natTrailingDegree q) ≠ 0
[PROOFSTEP]
rwa [coeff_mul_natTrailingDegree_add_natTrailingDegree]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
⊢ natTrailingDegree (p * q) = natTrailingDegree p + natTrailingDegree q
[PROOFSTEP]
have hp : p ≠ 0 := fun hp => h (by rw [hp, trailingCoeff_zero, zero_mul])
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p = 0
⊢ trailingCoeff p * trailingCoeff q = 0
[PROOFSTEP]
rw [hp, trailingCoeff_zero, zero_mul]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
⊢ natTrailingDegree (p * q) = natTrailingDegree p + natTrailingDegree q
[PROOFSTEP]
have hq : q ≠ 0 := fun hq =>
  h
    (by rw [hq, trailingCoeff_zero, mul_zero])
      -- Porting note: Needed to account for different coercion behaviour & add the lemmas below
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q = 0
⊢ trailingCoeff p * trailingCoeff q = 0
[PROOFSTEP]
rw [hq, trailingCoeff_zero, mul_zero]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ natTrailingDegree (p * q) = natTrailingDegree p + natTrailingDegree q
[PROOFSTEP]
have aux1 : ∀ n, Nat.cast n = WithTop.some (n) := fun n ↦ rfl
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
aux1 : ∀ (n : ℕ), ↑n = ↑n
⊢ natTrailingDegree (p * q) = natTrailingDegree p + natTrailingDegree q
[PROOFSTEP]
have aux2 : ∀ (p : R[X]), WithTop.some (natTrailingDegree p) = Nat.cast (natTrailingDegree p) := fun p ↦ rfl
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
aux1 : ∀ (n : ℕ), ↑n = ↑n
aux2 : ∀ (p : R[X]), ↑(natTrailingDegree p) = ↑(natTrailingDegree p)
⊢ natTrailingDegree (p * q) = natTrailingDegree p + natTrailingDegree q
[PROOFSTEP]
apply natTrailingDegree_eq_of_trailingDegree_eq_some
[GOAL]
case h
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
aux1 : ∀ (n : ℕ), ↑n = ↑n
aux2 : ∀ (p : R[X]), ↑(natTrailingDegree p) = ↑(natTrailingDegree p)
⊢ trailingDegree (p * q) = ↑(natTrailingDegree p + natTrailingDegree q)
[PROOFSTEP]
rw [trailingDegree_mul' h, aux1 (natTrailingDegree p + natTrailingDegree q), WithTop.coe_add, aux2 p, aux2 q, ←
  trailingDegree_eq_natTrailingDegree hp, ← trailingDegree_eq_natTrailingDegree hq]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Ring R
p : R[X]
⊢ trailingDegree (-p) = trailingDegree p
[PROOFSTEP]
unfold trailingDegree
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Ring R
p : R[X]
⊢ Finset.min (support (-p)) = Finset.min (support p)
[PROOFSTEP]
rw [support_neg]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Ring R
p : R[X]
⊢ natTrailingDegree (-p) = natTrailingDegree p
[PROOFSTEP]
simp [natTrailingDegree]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Ring R
n : ℤ
⊢ natTrailingDegree ↑n = 0
[PROOFSTEP]
simp only [← C_eq_int_cast, natTrailingDegree_C]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
c : R
⊢ nextCoeffUp (↑C c) = 0
[PROOFSTEP]
rw [nextCoeffUp]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
c : R
⊢ (if natTrailingDegree (↑C c) = 0 then 0 else coeff (↑C c) (natTrailingDegree (↑C c) + 1)) = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p : R[X]
hp : 0 < natTrailingDegree p
⊢ nextCoeffUp p = coeff p (natTrailingDegree p + 1)
[PROOFSTEP]
rw [nextCoeffUp, if_neg]
[GOAL]
case hnc
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p : R[X]
hp : 0 < natTrailingDegree p
⊢ ¬natTrailingDegree p = 0
[PROOFSTEP]
contrapose! hp
[GOAL]
case hnc
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p : R[X]
hp : natTrailingDegree p = 0
⊢ natTrailingDegree p ≤ 0
[PROOFSTEP]
simpa
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
n : ℕ∞
h : trailingDegree p < n
h₀ : p = 0
⊢ n ≤ trailingDegree p
[PROOFSTEP]
simp [h₀]
