-- Mathlib/Algebra/Polynomial/HasseDeriv.lean
theorem natDegree_hasseDeriv [NoZeroSMulDivisors ℕ R] (p : R[X]) (n : ℕ) :
    natDegree (hasseDeriv n p) = natDegree p - n

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

Tactic:
simpa [hasseDeriv_eq_zero_of_lt_natDegree, hn] using (tsub_eq_zero_of_le hn.le).symm

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
⊢ ((hasseDeriv n) p).natDegree = p.natDegree - n

Tactic:
rcases lt_or_le p.natDegree n with hn | hn

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

case inr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
⊢ ((hasseDeriv n) p).natDegree = p.natDegree - n

Proof state:
case inr.refine_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
⊢ ∀ (n_1 : ℕ) (c : R), c ≠ 0 → ((hasseDeriv n) ((monomial n_1) c)).natDegree = n_1 - n

Tactic:
classical
  simp only [ite_eq_right_iff, Ne, 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

Result:
no goals

Proof state:
case inr.refine_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
⊢ ∀ (n_1 : ℕ) (c : R), c ≠ 0 → ((hasseDeriv n) ((monomial n_1) c)).natDegree = n_1 - n

Tactic:
simp only [ite_eq_right_iff, Ne, natDegree_monomial, hasseDeriv_monomial]

Result:
case inr.refine_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
⊢ ∀ (n_1 : ℕ) (c : R), ¬c = 0 → ↑(n_1.choose n) * c = 0 → 0 = n_1 - n

Proof state:
case inr.refine_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
k : ℕ
c : R
c0 : ¬c = 0
hh : ↑(k.choose n) * c = 0
⊢ 0 = k - n

Tactic:
rw [← nsmul_eq_mul, smul_eq_zero, Nat.choose_eq_zero_iff] at hh

Result:
case inr.refine_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
k : ℕ
c : R
c0 : ¬c = 0
hh : k < n ∨ c = 0
⊢ 0 = k - n

Proof state:
case inr.refine_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
k : ℕ
c : R
c0 : ¬c = 0
hh : k < n ∨ c = 0
⊢ 0 = k - n

Tactic:
exact (tsub_eq_zero_of_le (Or.resolve_right hh c0).le).symm

Result:
no goals

Proof state:
case inr.refine_1
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
⊢ ∀ (f : R[X]), f.natDegree < n → (hasseDeriv n) f = 0

Tactic:
exact fun h => hasseDeriv_eq_zero_of_lt_natDegree _ _

Result:
no goals

Proof state:
case inr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
⊢ ((hasseDeriv n) p).natDegree = p.natDegree - n

Tactic:
refine map_natDegree_eq_sub ?_ ?_

Result:
case inr.refine_1
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
⊢ ∀ (f : R[X]), f.natDegree < n → (hasseDeriv n) f = 0

case inr.refine_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
⊢ ∀ (n_1 : ℕ) (c : R), c ≠ 0 → ((hasseDeriv n) ((monomial n_1) c)).natDegree = n_1 - n

Proof state:
case inr.refine_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
⊢ ∀ (n_1 : ℕ) (c : R), ¬c = 0 → ↑(n_1.choose n) * c = 0 → 0 = n_1 - n

Tactic:
intro k c c0 hh

Result:
case inr.refine_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
k : ℕ
c : R
c0 : ¬c = 0
hh : ↑(k.choose n) * c = 0
⊢ 0 = k - n