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

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

case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ natDegree (reverse f) + natTrailingDegree f ≤ natDegree f
case neg
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ natDegree f = natDegree (reverse f) + natTrailingDegree f
apply le_antisymm
no goals
case pos
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : f = 0
⊢ natDegree f = natDegree (reverse f) + natTrailingDegree f
rw [hf, reverse_zero, natDegree_zero, natTrailingDegree_zero]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ natDegree f - natTrailingDegree f ≤ natDegree (reverse f)
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ natDegree f ≤ natDegree (reverse f) + natTrailingDegree f
refine' tsub_le_iff_right.mp _
case neg.a.h
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ coeff (reverse f) (natDegree f - natTrailingDegree f) ≠ 0
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ natDegree f - natTrailingDegree f ≤ natDegree (reverse f)
apply le_natDegree_of_ne_zero
case neg.a.h
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ coeff f (natTrailingDegree f) ≠ 0
case neg.a.h
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ coeff (reverse f) (natDegree f - natTrailingDegree f) ≠ 0
rw [reverse, coeff_reflect, ← revAt_le f.natTrailingDegree_le_natDegree, revAt_invol]
no goals
case neg.a.h
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ coeff f (natTrailingDegree f) ≠ 0
exact trailingCoeff_nonzero_iff_nonzero.mpr hf
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ natTrailingDegree f ≤ natDegree f - natDegree (reverse f)
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ natDegree (reverse f) + natTrailingDegree f ≤ natDegree f
rw [← le_tsub_iff_left f.reverse_natDegree_le]
case neg.a.h
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ coeff f (natDegree f - natDegree (reverse f)) ≠ 0
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ natTrailingDegree f ≤ natDegree f - natDegree (reverse f)
apply natTrailingDegree_le_of_ne_zero
case neg.a.h
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
key : ¬leadingCoeff (reverse f) = 0
⊢ coeff f (natDegree f - natDegree (reverse f)) ≠ 0
case neg.a.h
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ coeff f (natDegree f - natDegree (reverse f)) ≠ 0
have key := mt leadingCoeff_eq_zero.mp (mt reverse_eq_zero.mp hf)
no goals
case neg.a.h
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
key : ¬leadingCoeff (reverse f) = 0
⊢ coeff f (natDegree f - natDegree (reverse f)) ≠ 0
rwa [leadingCoeff, coeff_reverse, revAt_le f.reverse_natDegree_le] at key