case pos
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
ha : a = 0
⊢ natDegree (↑C a) = 0

case neg
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
ha : ¬a = 0
⊢ natDegree (↑C a) = 0
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
⊢ natDegree (↑C a) = 0
by_cases ha : a = 0
case pos
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
ha : a = 0
this : ↑C a = 0
⊢ natDegree (↑C a) = 0
case pos
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
ha : a = 0
⊢ natDegree (↑C a) = 0
have : C a = 0 := by rw [ha, C_0]
case pos
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
ha : a = 0
this : ↑C a = 0
⊢ WithBot.unbot' 0 ⊥ = 0
case pos
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
ha : a = 0
this : ↑C a = 0
⊢ natDegree (↑C a) = 0
rw [natDegree, degree_eq_bot.2 this]
no goals
case pos
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
ha : a = 0
this : ↑C a = 0
⊢ WithBot.unbot' 0 ⊥ = 0
rfl
no goals
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
ha : a = 0
⊢ ↑C a = 0
rw [ha, C_0]
case neg
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
ha : ¬a = 0
⊢ WithBot.unbot' 0 0 = 0
case neg
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
ha : ¬a = 0
⊢ natDegree (↑C a) = 0
rw [natDegree, degree_C ha]
no goals
case neg
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
ha : ¬a = 0
⊢ WithBot.unbot' 0 0 = 0
rfl