refactor(data/polynomial): Golf proofs with existing lemmas

This allows the lemma which "ideally wouldn't be necessary" to not be necessary

src/data/polynomial/basic.lean

@@ -86,13 +86,6 @@ def coeff (p : polynomial R) : ℕ → R := @coe_fn (ℕ →₀ R) _ p
 lemma coeff_monomial : coeff (monomial n a) m = if n = m then a else 0 :=
 by { dsimp [monomial, coeff], rw finsupp.single_apply, congr }
 
-/--
-This lemma is needed for occasions when we break through the abstraction from
-`polynomial` to `finsupp`; ideally it wouldn't be necessary at all.
--/
-lemma coeff_single : coeff (single n a) m = if n = m then a else 0 :=
-coeff_monomial
-
 @[simp] lemma coeff_zero (n : ℕ) : coeff (0 : polynomial R) n = 0 := rfl
 
 @[simp] lemma coeff_one_zero : coeff (1 : polynomial R) 0 = 1 := coeff_monomial

src/data/polynomial/coeff.lean

@@ -75,27 +75,14 @@ lemma coeff_C_mul_X (x : R) (k n : ℕ) :
 by rw [← single_eq_C_mul_X]; simp [monomial, single, eq_comm, coeff]; congr
 
 @[simp] lemma coeff_C_mul (p : polynomial R) : coeff (C a * p) n = a * coeff p n :=
-begin
-  conv in (a * _) { rw [← @sum_single _ _ _ p, coeff_sum] },
-  rw [add_monoid_algebra.mul_def, ←monomial_zero_left, monomial, sum_single_index],
-  { simp only [coeff_single, finsupp.mul_sum, coeff_sum],
-    apply sum_congr rfl,
-    assume i hi, by_cases i = n; simp [h] },
-  { simp [finsupp.sum] }
-end
+add_monoid_algebra.single_zero_mul_apply p a n
 
 lemma C_mul' (a : R) (f : polynomial R) : C a * f = a • f :=
 ext $ λ n, coeff_C_mul f
 
 @[simp] lemma coeff_mul_C (p : polynomial R) (n : ℕ) (a : R) :
   coeff (p * C a) n = coeff p n * a :=
-begin
-  conv_rhs { rw [← @finsupp.sum_single _ _ _ p, coeff_sum] },
-  rw [add_monoid_algebra.mul_def, ←monomial_zero_left], simp_rw [sum_single_index],
-  { simp only [coeff_single, finsupp.sum_mul, coeff_sum],
-    apply sum_congr rfl,
-    assume i hi, by_cases i = n; simp [h], },
-end
+add_monoid_algebra.mul_single_zero_apply p a n
 
 lemma coeff_X_pow (k n : ℕ) :
   coeff (X^k : polynomial R) n = if n = k then 1 else 0 :=