-- Mathlib/Algebra/Polynomial/Reverse.lean
theorem natDegree_eq_reverse_natDegree_add_natTrailingDegree (f : R[X]) :
    f.natDegree = f.reverse.natDegree + f.natTrailingDegree

Proof state:
case neg.a.h
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.coeff f.natTrailingDegree ≠ 0

Tactic:
exact trailingCoeff_nonzero_iff_nonzero.mpr hf

Result:
no goals

Proof state:
case neg.a.h
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.coeff (f.natDegree - f.reverse.natDegree) ≠ 0

Tactic:
have key := mt leadingCoeff_eq_zero.mp (mt reverse_eq_zero.mp hf)

Result:
case neg.a.h
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
key : ¬f.reverse.leadingCoeff = 0
⊢ f.coeff (f.natDegree - f.reverse.natDegree) ≠ 0

Proof state:
case neg.a
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.reverse.natDegree + f.natTrailingDegree ≤ f.natDegree

Tactic:
rw [← le_tsub_iff_left f.reverse_natDegree_le]

Result:
case neg.a
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.natTrailingDegree ≤ f.natDegree - f.reverse.natDegree

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.natDegree = f.reverse.natDegree + f.natTrailingDegree

Tactic:
by_cases hf : f = 0

Result:
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : f = 0
⊢ f.natDegree = f.reverse.natDegree + f.natTrailingDegree

case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.natDegree = f.reverse.natDegree + f.natTrailingDegree

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : f = 0
⊢ f.natDegree = f.reverse.natDegree + f.natTrailingDegree

Tactic:
rw [hf, reverse_zero, natDegree_zero, natTrailingDegree_zero]

Result:
no goals

Proof state:
case neg.a.h
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.reverse.coeff (f.natDegree - f.natTrailingDegree) ≠ 0

Tactic:
rw [reverse, coeff_reflect, ← revAt_le f.natTrailingDegree_le_natDegree, revAt_invol]

Result:
case neg.a.h
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.coeff f.natTrailingDegree ≠ 0

Proof state:
case neg.a
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.natDegree - f.natTrailingDegree ≤ f.reverse.natDegree

Tactic:
apply le_natDegree_of_ne_zero

Result:
case neg.a.h
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.reverse.coeff (f.natDegree - f.natTrailingDegree) ≠ 0

Proof state:
case neg.a.h
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
key : ¬f.reverse.leadingCoeff = 0
⊢ f.coeff (f.natDegree - f.reverse.natDegree) ≠ 0

Tactic:
rwa [leadingCoeff, coeff_reverse, revAt_le f.reverse_natDegree_le] at key

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.natDegree = f.reverse.natDegree + f.natTrailingDegree

Tactic:
apply le_antisymm

Result:
case neg.a
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.natDegree ≤ f.reverse.natDegree + f.natTrailingDegree

case neg.a
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.reverse.natDegree + f.natTrailingDegree ≤ f.natDegree

Proof state:
case neg.a
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.natDegree ≤ f.reverse.natDegree + f.natTrailingDegree

Tactic:
refine tsub_le_iff_right.mp ?_

Result:
case neg.a
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.natDegree - f.natTrailingDegree ≤ f.reverse.natDegree

Proof state:
case neg.a
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.natTrailingDegree ≤ f.natDegree - f.reverse.natDegree

Tactic:
apply natTrailingDegree_le_of_ne_zero

Result:
case neg.a.h
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.coeff (f.natDegree - f.reverse.natDegree) ≠ 0