case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
p0 : p = 0
⊢ natDegree (↑(opRingEquiv R) p) = natDegree (unop p)

case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
p0 : ¬p = 0
⊢ natDegree (↑(opRingEquiv R) p) = natDegree (unop p)
R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
⊢ natDegree (↑(opRingEquiv R) p) = natDegree (unop p)
by_cases p0 : p = 0
no goals
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
p0 : p = 0
⊢ natDegree (↑(opRingEquiv R) p) = natDegree (unop p)
simp only [p0, _root_.map_zero, natDegree_zero, unop_zero]
no goals
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
p0 : ¬p = 0
⊢ natDegree (↑(opRingEquiv R) p) = natDegree (unop p)
simp only [p0, natDegree_eq_support_max', Ne.def, AddEquivClass.map_eq_zero_iff, not_false_iff,
  support_opRingEquiv, unop_eq_zero_iff]