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

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)
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
apply le_antisymm
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
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
refine' natTrailingDegree_le_of_ne_zero fun h => mt trailingCoeff_eq_zero.mp hp _
no goals
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
rwa [trailingCoeff, ← coeff_mul_X_pow]
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
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)
rw [natTrailingDegree_eq_support_min' fun h => hp (mul_X_pow_eq_zero h), Finset.le_min'_iff]
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
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
intro y hy
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
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
have key : n ≤ y := by
  rw [mem_support_iff, coeff_mul_X_pow'] at hy
  exact by_contra fun h => hy (if_neg h)
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
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
rw [mem_support_iff, coeff_mul_X_pow', if_pos key] at hy
no goals
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
exact (le_tsub_iff_right key).mp (natTrailingDegree_le_of_ne_zero hy)
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
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
rw [mem_support_iff, coeff_mul_X_pow'] at hy
no goals
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
exact by_contra fun h => hy (if_neg h)