[GOAL]
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : leadingCoeff p * leadingCoeff q = leadingCoeff q * leadingCoeff p
h : natDegree p ≤ natDegree q
hq : 0 < natDegree q
⊢ natDegree (cancelLeads p q) < natDegree q
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : leadingCoeff p * leadingCoeff q = leadingCoeff q * leadingCoeff p
h : natDegree p ≤ natDegree q
hq : 0 < natDegree q
hp : p = 0
⊢ natDegree (cancelLeads p q) < natDegree q
[PROOFSTEP]
convert hq
[GOAL]
case h.e'_3
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : leadingCoeff p * leadingCoeff q = leadingCoeff q * leadingCoeff p
h : natDegree p ≤ natDegree q
hq : 0 < natDegree q
hp : p = 0
⊢ natDegree (cancelLeads p q) = 0
[PROOFSTEP]
simp [hp, cancelLeads]
[GOAL]
case neg
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : leadingCoeff p * leadingCoeff q = leadingCoeff q * leadingCoeff p
h : natDegree p ≤ natDegree q
hq : 0 < natDegree q
hp : ¬p = 0
⊢ natDegree (cancelLeads p q) < natDegree q
[PROOFSTEP]
rw [cancelLeads, sub_eq_add_neg, tsub_eq_zero_iff_le.mpr h, pow_zero, mul_one]
[GOAL]
case neg
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : leadingCoeff p * leadingCoeff q = leadingCoeff q * leadingCoeff p
h : natDegree p ≤ natDegree q
hq : 0 < natDegree q
hp : ¬p = 0
⊢ natDegree (↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p)) < natDegree q
[PROOFSTEP]
by_cases h0 : C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p) = 0
[GOAL]
case pos
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : leadingCoeff p * leadingCoeff q = leadingCoeff q * leadingCoeff p
h : natDegree p ≤ natDegree q
hq : 0 < natDegree q
hp : ¬p = 0
h0 : ↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p) = 0
⊢ natDegree (↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p)) < natDegree q
[PROOFSTEP]
exact (le_of_eq (by simp only [h0, natDegree_zero])).trans_lt hq
[GOAL]
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : leadingCoeff p * leadingCoeff q = leadingCoeff q * leadingCoeff p
h : natDegree p ≤ natDegree q
hq : 0 < natDegree q
hp : ¬p = 0
h0 : ↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p) = 0
⊢ natDegree (↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p)) = 0
[PROOFSTEP]
simp only [h0, natDegree_zero]
[GOAL]
case neg
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : leadingCoeff p * leadingCoeff q = leadingCoeff q * leadingCoeff p
h : natDegree p ≤ natDegree q
hq : 0 < natDegree q
hp : ¬p = 0
h0 : ¬↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p) = 0
⊢ natDegree (↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p)) < natDegree q
[PROOFSTEP]
apply lt_of_le_of_ne
[GOAL]
case neg.a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : leadingCoeff p * leadingCoeff q = leadingCoeff q * leadingCoeff p
h : natDegree p ≤ natDegree q
hq : 0 < natDegree q
hp : ¬p = 0
h0 : ¬↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p) = 0
⊢ natDegree (↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p)) ≤ natDegree q
[PROOFSTEP]
rw [natDegree_add_le_iff_left]
[GOAL]
case neg.a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : leadingCoeff p * leadingCoeff q = leadingCoeff q * leadingCoeff p
h : natDegree p ≤ natDegree q
hq : 0 < natDegree q
hp : ¬p = 0
h0 : ¬↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p) = 0
⊢ natDegree (↑C (leadingCoeff p) * q) ≤ natDegree q
[PROOFSTEP]
apply natDegree_C_mul_le
[GOAL]
case neg.a.qn
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : leadingCoeff p * leadingCoeff q = leadingCoeff q * leadingCoeff p
h : natDegree p ≤ natDegree q
hq : 0 < natDegree q
hp : ¬p = 0
h0 : ¬↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p) = 0
⊢ natDegree (-(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p)) ≤ natDegree q
[PROOFSTEP]
refine (natDegree_neg (C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).le.trans ?_
[GOAL]
case neg.a.qn
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : leadingCoeff p * leadingCoeff q = leadingCoeff q * leadingCoeff p
h : natDegree p ≤ natDegree q
hq : 0 < natDegree q
hp : ¬p = 0
h0 : ¬↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p) = 0
⊢ natDegree (↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p) ≤ natDegree q
[PROOFSTEP]
exact natDegree_mul_le.trans <| Nat.add_le_of_le_sub h <| natDegree_C_mul_X_pow_le _ _
[GOAL]
case neg.a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : leadingCoeff p * leadingCoeff q = leadingCoeff q * leadingCoeff p
h : natDegree p ≤ natDegree q
hq : 0 < natDegree q
hp : ¬p = 0
h0 : ¬↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p) = 0
⊢ natDegree (↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p)) ≠ natDegree q
[PROOFSTEP]
contrapose! h0
[GOAL]
case neg.a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : leadingCoeff p * leadingCoeff q = leadingCoeff q * leadingCoeff p
h : natDegree p ≤ natDegree q
hq : 0 < natDegree q
hp : ¬p = 0
h0 : natDegree (↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p)) = natDegree q
⊢ ↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p) = 0
[PROOFSTEP]
rw [← leadingCoeff_eq_zero, leadingCoeff, h0, mul_assoc, X_pow_mul, ← tsub_add_cancel_of_le h, add_comm _ p.natDegree]
[GOAL]
case neg.a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : leadingCoeff p * leadingCoeff q = leadingCoeff q * leadingCoeff p
h : natDegree p ≤ natDegree q
hq : 0 < natDegree q
hp : ¬p = 0
h0 : natDegree (↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p)) = natDegree q
⊢ coeff
      (↑C (leadingCoeff p) * q +
        -(↑C (leadingCoeff q) * (p * X ^ (natDegree p + (natDegree q - natDegree p) - natDegree p))))
      (natDegree p + (natDegree q - natDegree p)) =
    0
[PROOFSTEP]
simp only [coeff_mul_X_pow, coeff_neg, coeff_C_mul, add_tsub_cancel_left, coeff_add]
[GOAL]
case neg.a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : leadingCoeff p * leadingCoeff q = leadingCoeff q * leadingCoeff p
h : natDegree p ≤ natDegree q
hq : 0 < natDegree q
hp : ¬p = 0
h0 : natDegree (↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p)) = natDegree q
⊢ leadingCoeff p * coeff q (natDegree p + (natDegree q - natDegree p)) + -(leadingCoeff q * coeff p (natDegree p)) = 0
[PROOFSTEP]
rw [add_comm p.natDegree, tsub_add_cancel_of_le h, ← leadingCoeff, ← leadingCoeff, comm, add_right_neg]
