refactor(data/polynomial/*): Make support_C_mul_X_pow match `suppor…

…t_monomial` (#14119)

This PR makes `support_C_mul_X_pow` match `support_monomial`.

src/data/polynomial/basic.lean

@@ -534,12 +534,21 @@ linear_map.to_add_monoid_hom_injective $ add_hom_ext $ λ n, linear_map.congr_fu
 lemma eq_zero_of_eq_zero (h : (0 : R) = (1 : R)) (p : R[X]) : p = 0 :=
 by rw [←one_smul R p, ←h, zero_smul]
 
-lemma support_monomial (n) (a : R) (H : a ≠ 0) : (monomial n a).support = singleton n :=
+lemma support_monomial (n) {a : R} (H : a ≠ 0) : (monomial n a).support = singleton n :=
 by rw [←of_finsupp_single, support, finsupp.support_single_ne_zero H]
 
 lemma support_monomial' (n) (a : R) : (monomial n a).support ⊆ singleton n :=
 by { rw [←of_finsupp_single, support], exact finsupp.support_single_subset }
 
+lemma support_C_mul_X_pow (n : ℕ) {c : R} (h : c ≠ 0) : (C c * X ^ n).support = singleton n :=
+by rw [←monomial_eq_C_mul_X, support_monomial n h]
+
+lemma support_C_mul_X_pow' (n : ℕ) (c : R) : (C c * X ^ n).support ⊆ singleton n :=
+begin
+  rw ← monomial_eq_C_mul_X,
+  exact support_monomial' n c,
+end
+
 lemma X_pow_eq_monomial (n) : X ^ n = monomial n (1:R) :=
 begin
   induction n with n hn,
@@ -554,7 +563,7 @@ calc monomial n a = monomial n (a * 1) : by simp
 
 lemma support_X_pow (H : ¬ (1:R) = 0) (n : ℕ) : (X^n : R[X]).support = singleton n :=
 begin
-  convert support_monomial n 1 H,
+  convert support_monomial n H,
   exact X_pow_eq_monomial n,
 end
 

src/data/polynomial/coeff.lean

@@ -187,13 +187,7 @@ lemma mul_X_injective : function.injective (λ P : R[X], X * P) :=
 pow_one (X : R[X]) ▸ mul_X_pow_injective 1
 
 lemma C_mul_X_pow_eq_monomial (c : R) (n : ℕ) : C c * X^n = monomial n c :=
-by { ext1, rw [monomial_eq_smul_X, coeff_smul, coeff_C_mul, smul_eq_mul] }
-
-lemma support_mul_X_pow (c : R) (n : ℕ) (H : c ≠ 0) : (C c * X^n).support = singleton n :=
-by rw [C_mul_X_pow_eq_monomial, support_monomial n c H]
-
-lemma support_C_mul_X_pow' {c : R} {n : ℕ} : (C c * X^n).support ⊆ singleton n :=
-by { rw [C_mul_X_pow_eq_monomial], exact support_monomial' n c }
+monomial_eq_C_mul_X.symm
 
 lemma coeff_X_add_C_pow (r : R) (n k : ℕ) :
   ((X + C r) ^ n).coeff k = r ^ (n - k) * (n.choose k : R) :=

src/data/polynomial/degree/definitions.lean

@@ -162,7 +162,7 @@ lemma nat_degree_le_nat_degree [semiring S] {q : S[X]} (hpq : p.degree ≤ q.deg
 with_bot.gi_get_or_else_bot.gc.monotone_l hpq
 
 @[simp] lemma degree_C (ha : a ≠ 0) : degree (C a) = (0 : with_bot ℕ) :=
-by { rw [degree, ← monomial_zero_left, support_monomial 0 _ ha, sup_singleton], refl }
+by { rw [degree, ← monomial_zero_left, support_monomial 0 ha, sup_singleton], refl }
 
 lemma degree_C_le : degree (C a) ≤ 0 :=
 begin
@@ -191,7 +191,7 @@ end
 by simp only [←C_eq_nat_cast, nat_degree_C]
 
 @[simp] lemma degree_monomial (n : ℕ) (ha : a ≠ 0) : degree (monomial n a) = n :=
-by rw [degree, support_monomial _ _ ha]; refl
+by rw [degree, support_monomial n ha]; refl
 
 @[simp] lemma degree_C_mul_X_pow (n : ℕ) (ha : a ≠ 0) : degree (C a * X ^ n) = n :=
 by rw [← monomial_eq_C_mul_X, degree_monomial n ha]
@@ -343,19 +343,13 @@ degree_monomial_le _ _
 lemma nat_degree_X_le : (X : R[X]).nat_degree ≤ 1 :=
 nat_degree_le_of_degree_le degree_X_le
 
-lemma support_C_mul_X_pow (c : R) (n : ℕ) : (C c * X ^ n).support ⊆ singleton n :=
-begin
-  rw [C_mul_X_pow_eq_monomial],
-  exact support_monomial' _ _
-end
-
 lemma mem_support_C_mul_X_pow {n a : ℕ} {c : R} (h : a ∈ (C c * X ^ n).support) : a = n :=
-mem_singleton.1 $ support_C_mul_X_pow _ _ h
+mem_singleton.1 $ support_C_mul_X_pow' n c h
 
 lemma card_support_C_mul_X_pow_le_one {c : R} {n : ℕ} : (C c * X ^ n).support.card ≤ 1 :=
 begin
   rw ← card_singleton n,
-  apply card_le_of_subset (support_C_mul_X_pow c n),
+  apply card_le_of_subset (support_C_mul_X_pow' n c),
 end
 
 lemma card_supp_le_succ_nat_degree (p : R[X]) : p.support.card ≤ p.nat_degree + 1 :=
@@ -371,13 +365,6 @@ le_degree_of_ne_zero ∘ mem_support_iff.mp
 lemma nonempty_support_iff : p.support.nonempty ↔ p ≠ 0 :=
 by rw [ne.def, nonempty_iff_ne_empty, ne.def, ← support_eq_empty]
 
-lemma support_C_mul_X_pow_nonzero {c : R} {n : ℕ} (h : c ≠ 0) :
-  (C c * X ^ n).support = singleton n :=
-begin
-  rw [C_mul_X_pow_eq_monomial],
-  exact support_monomial _ _ h
-end
-
 end semiring
 
 section nonzero_semiring

src/data/polynomial/degree/trailing_degree.lean

@@ -150,7 +150,7 @@ begin
 end
 
 @[simp] lemma trailing_degree_monomial (ha : a ≠ 0) : trailing_degree (monomial n a) = n :=
-by rw [trailing_degree, support_monomial _ _ ha, inf_singleton, with_top.some_eq_coe]
+by rw [trailing_degree, support_monomial n ha, inf_singleton, with_top.some_eq_coe]
 
 lemma nat_trailing_degree_monomial (ha : a ≠ 0) : nat_trailing_degree (monomial n a) = n :=
 by rw [nat_trailing_degree, trailing_degree_monomial ha]; refl

src/ring_theory/polynomial/content.lean

@@ -82,7 +82,7 @@ begin
   rw content,
   by_cases h0 : r = 0,
   { simp [h0] },
-  have h : (C r).support = {0} := support_monomial _ _ h0,
+  have h : (C r).support = {0} := support_monomial _ h0,
   simp [h],
 end