-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem natDegree_eq_zero_of_derivative_eq_zero [NoZeroSMulDivisors ℕ R] {f : R[X]}
    (h : derivative f = 0) : f.natDegree = 0

Proof state:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : derivative f = 0
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
⊢ False

Tactic:
let m := f.natDegree - 1

Result:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : derivative f = 0
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
m : ℕ := f.natDegree - 1
⊢ False

Proof state:
case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
h : derivative 0 = 0
⊢ natDegree 0 = 0

Tactic:
exact natDegree_zero

Result:
no goals

Proof state:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : derivative f = 0
hf : f ≠ 0
⊢ f.natDegree = 0

Tactic:
rw [natDegree_eq_zero_iff_degree_le_zero]

Result:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : derivative f = 0
hf : f ≠ 0
⊢ f.degree ≤ 0

Proof state:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : derivative f = 0
hf : f ≠ 0
⊢ f.degree ≤ 0

Tactic:
by_contra! f_nat_degree_pos

Result:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : derivative f = 0
hf : f ≠ 0
f_nat_degree_pos : 0 < f.degree
⊢ False

Proof state:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : derivative f = 0
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
m : ℕ := f.natDegree - 1
hm : m + 1 = f.natDegree
h2 : (derivative f).coeff m = f.coeff (m + 1) * (↑m + 1)
⊢ False

Tactic:
rw [Polynomial.ext_iff] at h

Result:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ∀ (n : ℕ), (derivative f).coeff n = coeff 0 n
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
m : ℕ := f.natDegree - 1
hm : m + 1 = f.natDegree
h2 : (derivative f).coeff m = f.coeff (m + 1) * (↑m + 1)
⊢ False

Proof state:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : derivative f = 0
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
m : ℕ := f.natDegree - 1
hm : m + 1 = f.natDegree
⊢ False

Tactic:
have h2 := coeff_derivative f m

Result:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : derivative f = 0
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
m : ℕ := f.natDegree - 1
hm : m + 1 = f.natDegree
h2 : (derivative f).coeff m = f.coeff (m + 1) * (↑m + 1)
⊢ False

Proof state:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ∀ (n : ℕ), (derivative f).coeff n = coeff 0 n
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
m : ℕ := f.natDegree - 1
hm : m + 1 = f.natDegree
h2 : f = 0
⊢ False

Tactic:
exact hf h2

Result:
no goals

Proof state:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : derivative f = 0
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
m : ℕ := f.natDegree - 1
⊢ False

Tactic:
have hm : m + 1 = f.natDegree := tsub_add_cancel_of_le f_nat_degree_pos

Result:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : derivative f = 0
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
m : ℕ := f.natDegree - 1
hm : m + 1 = f.natDegree
⊢ False

Proof state:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : derivative f = 0
hf : f ≠ 0
f_nat_degree_pos : 0 < f.degree
⊢ False

Tactic:
rw [← natDegree_pos_iff_degree_pos] at f_nat_degree_pos

Result:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : derivative f = 0
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
⊢ False

Proof state:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ∀ (n : ℕ), (derivative f).coeff n = coeff 0 n
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
m : ℕ := f.natDegree - 1
hm : m + 1 = f.natDegree
h2 : m + 1 = 0 ∨ f.coeff (m + 1) = 0
⊢ False

Tactic:
replace h2 := h2.resolve_left m.succ_ne_zero

Result:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ∀ (n : ℕ), (derivative f).coeff n = coeff 0 n
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
m : ℕ := f.natDegree - 1
hm : m + 1 = f.natDegree
h2 : f.coeff (m + 1) = 0
⊢ False

Proof state:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ∀ (n : ℕ), (derivative f).coeff n = coeff 0 n
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
m : ℕ := f.natDegree - 1
hm : m + 1 = f.natDegree
h2 : f.coeff (m + 1) = 0
⊢ False

Tactic:
rw [hm, ← leadingCoeff, leadingCoeff_eq_zero] at h2

Result:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ∀ (n : ℕ), (derivative f).coeff n = coeff 0 n
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
m : ℕ := f.natDegree - 1
hm : m + 1 = f.natDegree
h2 : f = 0
⊢ False

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : derivative f = 0
⊢ f.natDegree = 0

Tactic:
rcases eq_or_ne f 0 with (rfl | hf)

Result:
case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
h : derivative 0 = 0
⊢ natDegree 0 = 0

case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : derivative f = 0
hf : f ≠ 0
⊢ f.natDegree = 0

Proof state:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ∀ (n : ℕ), (derivative f).coeff n = coeff 0 n
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
m : ℕ := f.natDegree - 1
hm : m + 1 = f.natDegree
h2 : (derivative f).coeff m = f.coeff (m + 1) * (↑m + 1)
⊢ False

Tactic:
rw [h m, coeff_zero, ← Nat.cast_add_one, ← nsmul_eq_mul', eq_comm, smul_eq_zero] at h2

Result:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ∀ (n : ℕ), (derivative f).coeff n = coeff 0 n
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
m : ℕ := f.natDegree - 1
hm : m + 1 = f.natDegree
h2 : m + 1 = 0 ∨ f.coeff (m + 1) = 0
⊢ False