R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Ring R
p q : R[X]
hd : degree p = degree q
hp0 : p ≠ 0
hlc : leadingCoeff p = leadingCoeff q
hp : ↑(monomial (natDegree p)) (leadingCoeff p) + erase (natDegree p) p = p
hq : ↑(monomial (natDegree q)) (leadingCoeff q) + erase (natDegree q) q = q
⊢ WithBot.unbot' 0 (degree p) = WithBot.unbot' 0 (degree q)
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Ring R
p q : R[X]
hd : degree p = degree q
hp0 : p ≠ 0
hlc : leadingCoeff p = leadingCoeff q
hp : ↑(monomial (natDegree p)) (leadingCoeff p) + erase (natDegree p) p = p
hq : ↑(monomial (natDegree q)) (leadingCoeff q) + erase (natDegree q) q = q
⊢ natDegree p = natDegree q
unfold natDegree
no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Ring R
p q : R[X]
hd : degree p = degree q
hp0 : p ≠ 0
hlc : leadingCoeff p = leadingCoeff q
hp : ↑(monomial (natDegree p)) (leadingCoeff p) + erase (natDegree p) p = p
hq : ↑(monomial (natDegree q)) (leadingCoeff q) + erase (natDegree q) q = q
⊢ WithBot.unbot' 0 (degree p) = WithBot.unbot' 0 (degree q)
rw [hd]
no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Ring R
p q : R[X]
hd : degree p = degree q
hp0 : p ≠ 0
hlc : leadingCoeff p = leadingCoeff q
hp : ↑(monomial (natDegree p)) (leadingCoeff p) + erase (natDegree p) p = p
hq : ↑(monomial (natDegree q)) (leadingCoeff q) + erase (natDegree q) q = q
hd' : natDegree p = natDegree q
hq0 : q ≠ 0
⊢ degree (p - q) = degree (erase (natDegree q) p + -erase (natDegree q) q)
conv =>
  lhs
  rw [← hp, ← hq, hlc, hd', add_sub_add_left_eq_sub, sub_eq_add_neg]