case inl
R : Type u_1
inst✝¹ : Semiring R
k : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : natDegree p < n
⊢ natDegree (↑(hasseDeriv n) p) = natDegree p - n

case inr
R : Type u_1
inst✝¹ : Semiring R
k : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ natDegree p
⊢ natDegree (↑(hasseDeriv n) p) = natDegree p - n
R : Type u_1
inst✝¹ : Semiring R
k : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
⊢ natDegree (↑(hasseDeriv n) p) = natDegree p - n
cases' lt_or_le p.natDegree n with hn hn
no goals
case inl
R : Type u_1
inst✝¹ : Semiring R
k : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : natDegree p < n
⊢ natDegree (↑(hasseDeriv n) p) = natDegree p - n
simpa [hasseDeriv_eq_zero_of_lt_natDegree, hn] using (tsub_eq_zero_of_le hn.le).symm
case inr.refine'_1
R : Type u_1
inst✝¹ : Semiring R
k : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ natDegree p
⊢ ∀ (f : R[X]), natDegree f < n → ↑(hasseDeriv n) f = 0

case inr.refine'_2
R : Type u_1
inst✝¹ : Semiring R
k : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ natDegree p
⊢ ∀ (n_1 : ℕ) (c : R), c ≠ 0 → natDegree (↑(hasseDeriv n) (↑(monomial n_1) c)) = n_1 - n
case inr
R : Type u_1
inst✝¹ : Semiring R
k : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ natDegree p
⊢ natDegree (↑(hasseDeriv n) p) = natDegree p - n
refine' map_natDegree_eq_sub _ _
no goals
case inr.refine'_1
R : Type u_1
inst✝¹ : Semiring R
k : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ natDegree p
⊢ ∀ (f : R[X]), natDegree f < n → ↑(hasseDeriv n) f = 0
exact fun h => hasseDeriv_eq_zero_of_lt_natDegree _ _
no goals
case inr.refine'_2
R : Type u_1
inst✝¹ : Semiring R
k : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ natDegree p
⊢ ∀ (n_1 : ℕ) (c : R), c ≠ 0 → natDegree (↑(hasseDeriv n) (↑(monomial n_1) c)) = n_1 - n
classical
  simp only [ite_eq_right_iff, Ne.def, natDegree_monomial, hasseDeriv_monomial]
  intro k c c0 hh
  rw [← nsmul_eq_mul, smul_eq_zero, Nat.choose_eq_zero_iff] at hh
  exact (tsub_eq_zero_of_le (Or.resolve_right hh c0).le).symm
case inr.refine'_2
R : Type u_1
inst✝¹ : Semiring R
k : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ natDegree p
⊢ ∀ (n_1 : ℕ) (c : R), ¬c = 0 → ↑(choose n_1 n) * c = 0 → 0 = n_1 - n
case inr.refine'_2
R : Type u_1
inst✝¹ : Semiring R
k : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ natDegree p
⊢ ∀ (n_1 : ℕ) (c : R), c ≠ 0 → natDegree (↑(hasseDeriv n) (↑(monomial n_1) c)) = n_1 - n
simp only [ite_eq_right_iff, Ne.def, natDegree_monomial, hasseDeriv_monomial]
case inr.refine'_2
R : Type u_1
inst✝¹ : Semiring R
k✝ : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ natDegree p
k : ℕ
c : R
c0 : ¬c = 0
hh : ↑(choose k n) * c = 0
⊢ 0 = k - n
case inr.refine'_2
R : Type u_1
inst✝¹ : Semiring R
k : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ natDegree p
⊢ ∀ (n_1 : ℕ) (c : R), ¬c = 0 → ↑(choose n_1 n) * c = 0 → 0 = n_1 - n
intro k c c0 hh
case inr.refine'_2
R : Type u_1
inst✝¹ : Semiring R
k✝ : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ natDegree p
k : ℕ
c : R
c0 : ¬c = 0
hh : k < n ∨ c = 0
⊢ 0 = k - n
case inr.refine'_2
R : Type u_1
inst✝¹ : Semiring R
k✝ : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ natDegree p
k : ℕ
c : R
c0 : ¬c = 0
hh : ↑(choose k n) * c = 0
⊢ 0 = k - n
rw [← nsmul_eq_mul, smul_eq_zero, Nat.choose_eq_zero_iff] at hh
no goals
case inr.refine'_2
R : Type u_1
inst✝¹ : Semiring R
k✝ : ℕ
f : R[X]
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ natDegree p
k : ℕ
c : R
c0 : ¬c = 0
hh : k < n ∨ c = 0
⊢ 0 = k - n
exact (tsub_eq_zero_of_le (Or.resolve_right hh c0).le).symm