R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.652536
h : degree p = degree q
hlc : leadingCoeff p + leadingCoeff q ≠ 0
this : natDegree (p + q) = natDegree p
⊢ leadingCoeff (p + q) = leadingCoeff p + leadingCoeff q
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.652536
h : degree p = degree q
hlc : leadingCoeff p + leadingCoeff q ≠ 0
⊢ leadingCoeff (p + q) = leadingCoeff p + leadingCoeff q
have : natDegree (p + q) = natDegree p := by
  apply natDegree_eq_of_degree_eq;
    rw [degree_add_eq_of_leadingCoeff_add_ne_zero hlc, h, max_self]
no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.652536
h : degree p = degree q
hlc : leadingCoeff p + leadingCoeff q ≠ 0
this : natDegree (p + q) = natDegree p
⊢ leadingCoeff (p + q) = leadingCoeff p + leadingCoeff q
simp only [leadingCoeff, this, natDegree_eq_of_degree_eq h, coeff_add]
case h
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.652536
h : degree p = degree q
hlc : leadingCoeff p + leadingCoeff q ≠ 0
⊢ degree (p + q) = degree p
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.652536
h : degree p = degree q
hlc : leadingCoeff p + leadingCoeff q ≠ 0
⊢ natDegree (p + q) = natDegree p
apply natDegree_eq_of_degree_eq
no goals
case h
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.652536
h : degree p = degree q
hlc : leadingCoeff p + leadingCoeff q ≠ 0
⊢ degree (p + q) = degree p
rw [degree_add_eq_of_leadingCoeff_add_ne_zero hlc, h, max_self]