R : Type u
S : Type v
a✝ b c d : R
n m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
m : ℕ
⊢ (if a = 0 then 0 else m) ≤ m
R : Type u
S : Type v
a✝ b c d : R
n m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
m : ℕ
⊢ natDegree (↑(monomial m) a) ≤ m
rw [Polynomial.natDegree_monomial]
case inl
R : Type u
S : Type v
a✝ b c d : R
n m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
m : ℕ
h✝ : a = 0
⊢ 0 ≤ m

case inr
R : Type u
S : Type v
a✝ b c d : R
n m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
m : ℕ
h✝ : ¬a = 0
⊢ m ≤ m
R : Type u
S : Type v
a✝ b c d : R
n m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
m : ℕ
⊢ (if a = 0 then 0 else m) ≤ m
split_ifs
no goals
case inl
R : Type u
S : Type v
a✝ b c d : R
n m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
m : ℕ
h✝ : a = 0
⊢ 0 ≤ m

case inr
R : Type u
S : Type v
a✝ b c d : R
n m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
m : ℕ
h✝ : ¬a = 0
⊢ m ≤ m
exacts [Nat.zero_le _, rfl.le]