chore(data/polynomial/derivative): golf proof of mem_support_derivative (#4134)

Golfed proof to be similar to what it was like prior to the refactor.

Author: shingtaklam1324

src/data/polynomial/coeff.lean

@@ -39,6 +39,9 @@ lemma coeff_sum [semiring S] (n : ℕ) (f : ℕ → R → polynomial S) :
 @[simp] lemma coeff_smul (p : polynomial R) (r : R) (n : ℕ) :
 coeff (r • p) n = r * coeff p n := finsupp.smul_apply
 
+lemma mem_support_iff_coeff_ne_zero : n ∈ p.support ↔ p.coeff n ≠ 0 :=
+by { rw mem_support_to_fun, refl }
+
 variable (R)
 /-- The nth coefficient, as a linear map. -/
 def lcoeff (n : ℕ) : polynomial R →ₗ[R] R :=

src/data/polynomial/derivative.lean

@@ -185,18 +185,12 @@ end comm_semiring
 
 section domain
 variables [integral_domain R]
--- TODO: golf this, dunno how i broke it so bad
+
 lemma mem_support_derivative [char_zero R] (p : polynomial R) (n : ℕ) :
   n ∈ (derivative p).support ↔ n + 1 ∈ p.support :=
-begin
-rw finsupp.mem_support_iff, split; intro h,
-suffices h1 : p.coeff (n+1) ≠ 0, simp; tauto, contrapose! h,
-convert coeff_derivative _ _, simp [h],
-contrapose! h, simp,
-suffices : p.to_fun (n + 1) * (n + 1) = 0, simp only [mul_eq_zero] at this, cases this,
-{ exact this }, { norm_cast at this },
-erw ← h, symmetry, convert coeff_derivative _ _,
-end
+suffices (¬(coeff p (n + 1) = 0 ∨ ((n + 1:ℕ) : R) = 0)) ↔ coeff p (n + 1) ≠ 0,
+  by simpa only [mem_support_iff_coeff_ne_zero, coeff_derivative, ne.def, mul_eq_zero],
+by { rw [nat.cast_eq_zero], simp only [nat.succ_ne_zero, or_false] }
 
 @[simp] lemma degree_derivative_eq [char_zero R] (p : polynomial R) (hp : 0 < nat_degree p) :
   degree (derivative p) = (nat_degree p - 1 : ℕ) :=