-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
theorem natTrailingDegree_mul_X_pow {p : R[X]} (hp : p ≠ 0) (n : ℕ) :
    (p * X ^ n).natTrailingDegree = p.natTrailingDegree + n

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n y : ℕ
hy : y ∈ (p * X ^ n).support
⊢ n ≤ y

Tactic:
rw [mem_support_iff, coeff_mul_X_pow'] at hy

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n y : ℕ
hy : (if n ≤ y then p.coeff (y - n) else 0) ≠ 0
⊢ n ≤ y

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
⊢ (p * X ^ n).natTrailingDegree = p.natTrailingDegree + n

Tactic:
apply le_antisymm

Result:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
⊢ (p * X ^ n).natTrailingDegree ≤ p.natTrailingDegree + n

case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
⊢ p.natTrailingDegree + n ≤ (p * X ^ n).natTrailingDegree

Proof state:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n y : ℕ
hy : y ∈ (p * X ^ n).support
key : n ≤ y
⊢ p.natTrailingDegree + n ≤ y

Tactic:
rw [mem_support_iff, coeff_mul_X_pow', if_pos key] at hy

Result:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n y : ℕ
hy : p.coeff (y - n) ≠ 0
key : n ≤ y
⊢ p.natTrailingDegree + n ≤ y

Proof state:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n y : ℕ
hy : y ∈ (p * X ^ n).support
⊢ p.natTrailingDegree + n ≤ y

Tactic:
have key : n ≤ y := by
  rw [mem_support_iff, coeff_mul_X_pow'] at hy
  exact by_contra fun h => hy (if_neg h)

Result:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n y : ℕ
hy : y ∈ (p * X ^ n).support
key : n ≤ y
⊢ p.natTrailingDegree + n ≤ y

Proof state:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
⊢ (p * X ^ n).natTrailingDegree ≤ p.natTrailingDegree + n

Tactic:
refine natTrailingDegree_le_of_ne_zero fun h => mt trailingCoeff_eq_zero.mp hp ?_

Result:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
h : (p * X ^ n).coeff (p.natTrailingDegree + n) = 0
⊢ p.trailingCoeff = 0

Proof state:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
⊢ ∀ y ∈ (p * X ^ n).support, p.natTrailingDegree + n ≤ y

Tactic:
intro y hy

Result:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n y : ℕ
hy : y ∈ (p * X ^ n).support
⊢ p.natTrailingDegree + n ≤ y

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n y : ℕ
hy : (if n ≤ y then p.coeff (y - n) else 0) ≠ 0
⊢ n ≤ y

Tactic:
exact by_contra fun h => hy (if_neg h)

Result:
no goals

Proof state:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
h : (p * X ^ n).coeff (p.natTrailingDegree + n) = 0
⊢ p.trailingCoeff = 0

Tactic:
rwa [trailingCoeff, ← coeff_mul_X_pow]

Result:
no goals

Proof state:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
⊢ p.natTrailingDegree + n ≤ (p * X ^ n).natTrailingDegree

Tactic:
rw [natTrailingDegree_eq_support_min' fun h => hp (mul_X_pow_eq_zero h), Finset.le_min'_iff]

Result:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
⊢ ∀ y ∈ (p * X ^ n).support, p.natTrailingDegree + n ≤ y

Proof state:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n y : ℕ
hy : p.coeff (y - n) ≠ 0
key : n ≤ y
⊢ p.natTrailingDegree + n ≤ y

Tactic:
exact (le_tsub_iff_right key).mp (natTrailingDegree_le_of_ne_zero hy)

Result:
no goals