chore(data/mv_polynomials): golf, add a lemma (#9132)

* add `monoid_algebra.support_mul_single`;
* transfer a few more lemmas from `monoid_algebra` to `add_monoid_algebra`
* add `mv_polynomial.support_mul_X`
* reuse a proof.

src/algebra/monoid_algebra/basic.lean

@@ -359,6 +359,19 @@ lemma mul_single_one_apply [mul_one_class G] (f : monoid_algebra k G) (r : k) (x
   (f * single 1 r) x = f x * r :=
 f.mul_single_apply_aux $ λ a, by rw [mul_one]
 
+lemma support_mul_single [right_cancel_semigroup G]
+  (f : monoid_algebra k G) (r : k) (hr : ∀ y, y * r = 0 ↔ y = 0) (x : G) :
+  (f * single x r).support = f.support.map (mul_right_embedding x) :=
+begin
+  ext y, simp only [mem_support_iff, mem_map, exists_prop, mul_right_embedding_apply],
+  by_cases H : ∃ a, a * x = y,
+  { rcases H with ⟨a, rfl⟩,
+    rw [mul_single_apply_aux f (λ _, mul_left_inj x)],
+    simp [hr] },
+  { push_neg at H,
+    simp [mul_apply, H] }
+end
+
 lemma single_mul_apply_aux [has_mul G] (f : monoid_algebra k G) {r : k} {x y z : G}
   (H : ∀ a, x * a = y ↔ a = z) :
   (single x r * f) y = r * f z :=
@@ -1052,6 +1065,20 @@ lemma single_zero_mul_apply [add_zero_class G] (f : add_monoid_algebra k G) (r :
   (single 0 r * f : add_monoid_algebra k G) x = r * f x :=
 f.single_mul_apply_aux r _ _ _ $ λ a, by rw [zero_add]
 
+lemma mul_single_apply [add_group G] (f : add_monoid_algebra k G) (r : k) (x y : G) :
+  (f * single x r) y = f (y - x) * r :=
+(sub_eq_add_neg y x).symm ▸
+  @monoid_algebra.mul_single_apply k (multiplicative G) _ _ _ _ _ _
+
+lemma single_mul_apply [add_group G] (r : k) (x : G) (f : add_monoid_algebra k G) (y : G) :
+  (single x r * f : add_monoid_algebra k G) y = r * f (- x + y) :=
+@monoid_algebra.single_mul_apply k (multiplicative G) _ _ _ _ _ _
+
+lemma support_mul_single [add_right_cancel_semigroup G]
+  (f : add_monoid_algebra k G) (r : k) (hr : ∀ y, y * r = 0 ↔ y = 0) (x : G) :
+  (f * single x r : add_monoid_algebra k G).support = f.support.map (add_right_embedding x) :=
+@monoid_algebra.support_mul_single k (multiplicative G) _ _ _ _ hr _
+
 lemma lift_nc_smul {R : Type*} [add_zero_class G] [semiring R] (f : k →+* R)
   (g : multiplicative G →* R) (c : k) (φ : monoid_algebra k G) :
   lift_nc (f : k →+ R) g (c • φ) = f c * lift_nc (f : k →+ R) g φ :=

src/data/mv_polynomial/basic.lean

@@ -423,51 +423,15 @@ end
 
 lemma coeff_mul (p q : mv_polynomial σ R) (n : σ →₀ ℕ) :
   coeff n (p * q) = ∑ x in antidiagonal n, coeff x.1 p * coeff x.2 q :=
-begin
-  rw mul_def,
-  -- We need to manipulate both sides into a shape to which we can apply `finset.sum_bij_ne_zero`,
-  -- so we need to turn both sides into a sum over a product.
-  have := @finset.sum_product R (σ →₀ ℕ) _ _ p.support q.support
-    (λ x, if (x.1 + x.2 = n) then coeff x.1 p * coeff x.2 q else 0),
-  convert this.symm using 1; clear this,
-  { rw [coeff],
-    iterate 2 { rw sum_apply, apply finset.sum_congr rfl, intros, dsimp only },
-    exact single_apply },
-  symmetry,
-  -- We are now ready to show that both sums are equal using `finset.sum_bij_ne_zero`.
-  apply finset.sum_bij_ne_zero (λ (x : (σ →₀ ℕ) × (σ →₀ ℕ)) _ _, (x.1, x.2)),
-  { intros x hx hx',
-    simp only [mem_antidiagonal, eq_self_iff_true, if_false, forall_true_iff],
-    contrapose! hx',
-    rw [if_neg hx'] },
-  { rintros ⟨i, j⟩ ⟨k, l⟩ hij hij' hkl hkl',
-    simpa only [and_imp, prod.mk.inj_iff, heq_iff_eq] using and.intro },
-  { rintros ⟨i, j⟩ hij hij',
-    refine ⟨⟨i, j⟩, _, _⟩,
-    { simp only [mem_support_iff, finset.mem_product],
-      contrapose! hij',
-      exact mul_eq_zero_of_ne_zero_imp_eq_zero hij' },
-    { rw [mem_antidiagonal] at hij,
-      simp only [exists_prop, true_and, ne.def, if_pos hij, hij', not_false_iff] } },
-  { intros x hx hx',
-    simp only [ne.def] at hx' ⊢,
-    split_ifs with H,
-    { refl },
-    { rw if_neg H at hx', contradiction } }
-end
+add_monoid_algebra.mul_apply_antidiagonal p q _ _ $ λ p, mem_antidiagonal
 
 @[simp] lemma coeff_mul_X (m) (s : σ) (p : mv_polynomial σ R) :
   coeff (m + single s 1) (p * X s) = coeff m p :=
-begin
-  have : (m, single s 1) ∈ (m + single s 1).antidiagonal := mem_antidiagonal.2 rfl,
-  rw [coeff_mul, ← finset.insert_erase this, finset.sum_insert (finset.not_mem_erase _ _),
-      finset.sum_eq_zero, add_zero, coeff_X, mul_one],
-  rintros ⟨i,j⟩ hij,
-  rw [finset.mem_erase, mem_antidiagonal] at hij,
-  by_cases H : single s 1 = j,
-  { subst j, simpa using hij },
-  { rw [coeff_X', if_neg H, mul_zero] },
-end
+(add_monoid_algebra.mul_single_apply_aux p _ _ _ _ (λ a, add_left_inj _)).trans (mul_one _)
+
+@[simp] lemma support_mul_X (s : σ) (p : mv_polynomial σ R) :
+  (p * X s).support = p.support.map (add_right_embedding (single s 1)) :=
+add_monoid_algebra.support_mul_single p _ (by simp) _ 
 
 lemma coeff_mul_X' [decidable_eq σ] (m) (s : σ) (p : mv_polynomial σ R) :
   coeff m (p * X s) = if s ∈ m.support then coeff (m - single s 1) p else 0 :=