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

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
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
by_cases hp : p = 0
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
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
rw [cancelLeads, sub_eq_add_neg, tsub_eq_zero_iff_le.mpr h, pow_zero, mul_one]
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

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
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
by_cases h0 :
  C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p) = 0
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

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
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
apply lt_of_le_of_ne
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
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
convert hq
no goals
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
simp [hp, cancelLeads]
no goals
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
exact (le_of_eq (by simp only [h0, natDegree_zero])).trans_lt hq
no goals
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
simp only [h0, natDegree_zero]
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

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
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
rw [natDegree_add_le_iff_left]
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
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
refine (natDegree_neg (C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).le.trans ?_
no goals
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
exact natDegree_mul_le.trans <| Nat.add_le_of_le_sub h <| natDegree_C_mul_X_pow_le _ _
no goals
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
apply natDegree_C_mul_le
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
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
contrapose! h0
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
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
rw [← leadingCoeff_eq_zero, leadingCoeff, h0, mul_assoc, X_pow_mul, ← tsub_add_cancel_of_le h,
  add_comm _ p.natDegree]
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
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
simp only [coeff_mul_X_pow, coeff_neg, coeff_C_mul, add_tsub_cancel_left, coeff_add]
no goals
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
rw [add_comm p.natDegree, tsub_add_cancel_of_le h, ← leadingCoeff, ← leadingCoeff, comm,
  add_right_neg]