refactor(MonoidAlgebra/Support): reformulate support_mul (#8953)

Use pointwise multiplication/addition of `Finset`s in `MonoidAlgebra.support_mul` and `AddMonoidAlgebra.support_mul`.

Mathlib/Algebra/MonoidAlgebra/Degree.lean

@@ -102,19 +102,15 @@ variable [Add A] [Add B] [Add T] [CovariantClass B B (· + ·) (· ≤ ·)]
 
 theorem sup_support_mul_le {degb : A → B} (degbm : ∀ {a b}, degb (a + b) ≤ degb a + degb b)
     (f g : R[A]) :
-    (f * g).support.sup degb ≤ f.support.sup degb + g.support.sup degb := by
-  refine' (Finset.sup_mono <| support_mul _ _).trans _
-  simp_rw [Finset.sup_biUnion, Finset.sup_singleton]
-  refine' Finset.sup_le fun fd fds => Finset.sup_le fun gd gds => degbm.trans <| add_le_add _ _ <;>
-    exact Finset.le_sup ‹_›
+    (f * g).support.sup degb ≤ f.support.sup degb + g.support.sup degb :=
+  (Finset.sup_mono <| support_mul _ _).trans <| Finset.sup_add_le.2 fun _fd fds _gd gds ↦
+    degbm.trans <| add_le_add (Finset.le_sup fds) (Finset.le_sup gds)
 #align add_monoid_algebra.sup_support_mul_le AddMonoidAlgebra.sup_support_mul_le
 
 theorem le_inf_support_mul {degt : A → T} (degtm : ∀ {a b}, degt a + degt b ≤ degt (a + b))
     (f g : R[A]) :
-    f.support.inf degt + g.support.inf degt ≤ (f * g).support.inf degt := by
-    refine' OrderDual.ofDual_le_ofDual.mpr <| sup_support_mul_le _ f g
-    intros a b
-    exact OrderDual.ofDual_le_ofDual.mp degtm
+    f.support.inf degt + g.support.inf degt ≤ (f * g).support.inf degt :=
+  sup_support_mul_le (B := Tᵒᵈ) degtm f g
 #align add_monoid_algebra.le_inf_support_mul AddMonoidAlgebra.le_inf_support_mul
 
 end AddOnly

Mathlib/Algebra/MonoidAlgebra/Grading.lean

@@ -100,17 +100,12 @@ instance gradeBy.gradedMonoid [AddMonoid M] [AddMonoid ι] [CommSemiring R] (f :
     SetLike.GradedMonoid (gradeBy R f : ι → Submodule R R[M]) where
   one_mem m h := by
     rw [one_def] at h
-    by_cases H : (1 : R) = (0 : R)
-    · rw [H, single, Finsupp.single_zero] at h
-      cases h
-    · rw [Finsupp.support_single_ne_zero _ H, Finset.mem_singleton] at h
-      rw [h, AddMonoidHom.map_zero]
+    obtain rfl : m = 0 := Finset.mem_singleton.1 <| Finsupp.support_single_subset h
+    apply map_zero
   mul_mem i j a b ha hb c hc := by
-    set h := support_mul a b hc
-    simp only [Finset.mem_biUnion] at h
-    rcases h with ⟨ma, ⟨hma, ⟨mb, ⟨hmb, hmc⟩⟩⟩⟩
-    rw [← ha ma hma, ← hb mb hmb, Finset.mem_singleton.mp hmc]
-    apply AddMonoidHom.map_add
+    obtain ⟨ma, hma, mb, hmb, rfl⟩ : ∃ y ∈ a.support, ∃ z ∈ b.support, y + z = c :=
+      Finset.mem_add.1 <| support_mul a b hc
+    rw [map_add, ha ma hma, hb mb hmb]
 #align add_monoid_algebra.grade_by.graded_monoid AddMonoidAlgebra.gradeBy.gradedMonoid
 
 instance grade.gradedMonoid [AddMonoid M] [CommSemiring R] :

Mathlib/Algebra/MonoidAlgebra/Support.lean

@@ -4,13 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
 import Mathlib.Algebra.MonoidAlgebra.Basic
+import Mathlib.Data.Finset.Pointwise
 
 #align_import algebra.monoid_algebra.support from "leanprover-community/mathlib"@"16749fc4661828cba18cd0f4e3c5eb66a8e80598"
 
 /-!
 #  Lemmas about the support of a finitely supported function
 -/
 
+open scoped Pointwise
 
 universe u₁ u₂ u₃
 
@@ -20,36 +22,23 @@ open Finset Finsupp
 
 variable {k : Type u₁} {G : Type u₂} [Semiring k]
 
+theorem support_mul [Mul G] [DecidableEq G] (a b : MonoidAlgebra k G) :
+    (a * b).support ⊆ a.support * b.support :=
+  support_sum.trans <| biUnion_subset.2 fun _x hx ↦
+    support_sum.trans <| biUnion_subset.2 fun _y hy ↦
+      support_single_subset.trans <| singleton_subset_iff.2 <| mem_image₂_of_mem hx hy
+#align monoid_algebra.support_mul MonoidAlgebra.support_mul
+
 theorem support_single_mul_subset [DecidableEq G] [Mul G] (f : MonoidAlgebra k G) (r : k) (a : G) :
-    (single a r * f : MonoidAlgebra k G).support ⊆ Finset.image (a * ·) f.support := by
-  intro x hx
-  contrapose hx
-  have : ∀ y, a * y = x → f y = 0 := by
-    simpa only [not_and', mem_image, mem_support_iff, exists_prop, not_exists,
-      Classical.not_not] using hx
-  simp only [mem_support_iff, mul_apply, sum_single_index, zero_mul, ite_self, sum_zero,
-    Classical.not_not]
-  exact
-    Finset.sum_eq_zero
-      (by
-        simp (config := { contextual := true }) only [this, mem_support_iff, mul_zero, Ne.def,
-          ite_eq_right_iff, eq_self_iff_true, imp_true_iff])
+    (single a r * f : MonoidAlgebra k G).support ⊆ Finset.image (a * ·) f.support :=
+  (support_mul _ _).trans <| (Finset.image₂_subset_right support_single_subset).trans <| by
+    rw [Finset.image₂_singleton_left]
 #align monoid_algebra.support_single_mul_subset MonoidAlgebra.support_single_mul_subset
 
 theorem support_mul_single_subset [DecidableEq G] [Mul G] (f : MonoidAlgebra k G) (r : k) (a : G) :
-    (f * single a r).support ⊆ Finset.image (· * a) f.support := by
-  intro x hx
-  contrapose hx
-  have : ∀ y, y * a = x → f y = 0 := by
-    simpa only [not_and', mem_image, mem_support_iff, exists_prop, not_exists,
-      Classical.not_not] using hx
-  simp only [mem_support_iff, mul_apply, sum_single_index, zero_mul, ite_self, sum_zero,
-    Classical.not_not]
-  exact
-    Finset.sum_eq_zero
-      (by
-        simp (config := { contextual := true }) only [this, sum_single_index, ite_eq_right_iff,
-          eq_self_iff_true, imp_true_iff, zero_mul])
+    (f * single a r).support ⊆ Finset.image (· * a) f.support :=
+  (support_mul _ _).trans <| (Finset.image₂_subset_left support_single_subset).trans <| by
+    rw [Finset.image₂_singleton_right]
 #align monoid_algebra.support_mul_single_subset MonoidAlgebra.support_mul_single_subset
 
 theorem support_single_mul_eq_image [DecidableEq G] [Mul G] (f : MonoidAlgebra k G) {r : k}
@@ -72,13 +61,6 @@ theorem support_mul_single_eq_image [DecidableEq G] [Mul G] (f : MonoidAlgebra k
     Finsupp.sum_ite_eq', Ne.def, not_false_iff, if_true, mul_zero, ite_self, sum_zero, rx.eq_iff]
 #align monoid_algebra.support_mul_single_eq_image MonoidAlgebra.support_mul_single_eq_image
 
-theorem support_mul [Mul G] [DecidableEq G] (a b : MonoidAlgebra k G) :
-    (a * b).support ⊆ a.support.biUnion fun a₁ => b.support.biUnion fun a₂ => {a₁ * a₂} :=
-  Subset.trans support_sum <|
-    biUnion_mono fun _ _ =>
-      Subset.trans support_sum <| biUnion_mono fun _a₂ _ => support_single_subset
-#align monoid_algebra.support_mul MonoidAlgebra.support_mul
-
 theorem support_mul_single [Mul G] [IsRightCancelMul G] (f : MonoidAlgebra k G) (r : k)
     (hr : ∀ y, y * r = 0 ↔ y = 0) (x : G) :
     (f * single x r).support = f.support.map (mulRightEmbedding x) := by
@@ -97,6 +79,13 @@ theorem support_single_mul [Mul G] [IsLeftCancelMul G] (f : MonoidAlgebra k G) (
       mem_map, mulLeftEmbedding_apply]
 #align monoid_algebra.support_single_mul MonoidAlgebra.support_single_mul
 
+lemma support_one_subset [One G] : (1 : MonoidAlgebra k G).support ⊆ 1 :=
+  Finsupp.support_single_subset
+
+@[simp]
+lemma support_one [One G] [NeZero (1 : k)] : (1 : MonoidAlgebra k G).support = 1 :=
+  Finsupp.support_single_ne_zero _ one_ne_zero
+
 section Span
 
 variable [MulOneClass G]
@@ -118,7 +107,7 @@ open Finset Finsupp MulOpposite
 variable {k : Type u₁} {G : Type u₂} [Semiring k]
 
 theorem support_mul [DecidableEq G] [Add G] (a b : k[G]) :
-    (a * b).support ⊆ a.support.biUnion fun a₁ => b.support.biUnion fun a₂ => {a₁ + a₂} :=
+    (a * b).support ⊆ a.support + b.support :=
   @MonoidAlgebra.support_mul k (Multiplicative G) _ _ _ _ _
 #align add_monoid_algebra.support_mul AddMonoidAlgebra.support_mul
 
@@ -134,6 +123,12 @@ theorem support_single_mul [Add G] [IsLeftCancelAdd G] (f : k[G]) (r : k)
   MonoidAlgebra.support_single_mul (G := Multiplicative G) _ _ hr _
 #align add_monoid_algebra.support_single_mul AddMonoidAlgebra.support_single_mul
 
+lemma support_one_subset [Zero G] : (1 : k[G]).support ⊆ 0 := Finsupp.support_single_subset
+
+@[simp]
+lemma support_one [Zero G] [NeZero (1 : k)] : (1 : k[G]).support = 0 :=
+  Finsupp.support_single_ne_zero _ one_ne_zero
+
 section Span
 
 /-- An element of `k[G]` is in the submodule generated by its support. -/

Mathlib/Data/MvPolynomial/Basic.lean

@@ -71,14 +71,10 @@ polynomial, multivariate polynomial, multivariable polynomial
 
 set_option autoImplicit true
 
-
 noncomputable section
 
-open BigOperators
-
 open Set Function Finsupp AddMonoidAlgebra
-
-open BigOperators
+open scoped BigOperators Pointwise
 
 universe u v w x
 
@@ -597,8 +593,8 @@ theorem sum_def {A} [AddCommMonoid A] {p : MvPolynomial σ R} {b : (σ →₀ 
 #align mv_polynomial.sum_def MvPolynomial.sum_def
 
 theorem support_mul [DecidableEq σ] (p q : MvPolynomial σ R) :
-    (p * q).support ⊆ p.support.biUnion fun a => q.support.biUnion fun b => {a + b} := by
-  convert AddMonoidAlgebra.support_mul p q
+    (p * q).support ⊆ p.support + q.support :=
+  AddMonoidAlgebra.support_mul p q
 #align mv_polynomial.support_mul MvPolynomial.support_mul
 
 @[ext]
@@ -772,23 +768,15 @@ theorem support_symmDiff_support_subset_support_add [DecidableEq σ] (p q : MvPo
 theorem coeff_mul_monomial' (m) (s : σ →₀ ℕ) (r : R) (p : MvPolynomial σ R) :
     coeff m (p * monomial s r) = if s ≤ m then coeff (m - s) p * r else 0 := by
   classical
-  obtain rfl | hr := eq_or_ne r 0
-  · simp only [monomial_zero, coeff_zero, mul_zero, ite_self]
-  haveI : Nontrivial R := nontrivial_of_ne _ _ hr
   split_ifs with h
   · conv_rhs => rw [← coeff_mul_monomial _ s]
     congr with t
     rw [tsub_add_cancel_of_le h]
-  · rw [← not_mem_support_iff]
-    intro hm
-    apply h
-    have H := support_mul _ _ hm
-    simp only [Finset.mem_biUnion] at H
-    rcases H with ⟨j, _hj, i', hi', H⟩
-    rw [support_monomial, if_neg hr, Finset.mem_singleton] at hi'
-    subst i'
-    rw [Finset.mem_singleton] at H
-    subst m
+  · contrapose! h
+    rw [← mem_support_iff] at h
+    obtain ⟨j, -, rfl⟩ : ∃ j ∈ support p, j + s = m := by
+      simpa [Finset.add_singleton]
+        using Finset.add_subset_add_left support_monomial_subset <| support_mul _ _ h
     exact le_add_left le_rfl
 #align mv_polynomial.coeff_mul_monomial' MvPolynomial.coeff_mul_monomial'
 

Mathlib/Data/MvPolynomial/Variables.lean

@@ -159,29 +159,18 @@ theorem degrees_sum {ι : Type*} [DecidableEq σ] (s : Finset ι) (f : ι → Mv
 
 theorem degrees_mul (p q : MvPolynomial σ R) : (p * q).degrees ≤ p.degrees + q.degrees := by
   classical
-  refine' Finset.sup_le fun b hb => _
-  have := support_mul p q hb
-  simp only [Finset.mem_biUnion, Finset.mem_singleton] at this
-  rcases this with ⟨a₁, h₁, a₂, h₂, rfl⟩
+  refine (Finset.sup_mono <| support_mul p q).trans <| Finset.sup_add_le.2 fun a ha b hb ↦ ?_
   rw [Finsupp.toMultiset_add]
-  exact add_le_add (Finset.le_sup h₁) (Finset.le_sup h₂)
+  exact add_le_add (Finset.le_sup ha) (Finset.le_sup hb)
 #align mv_polynomial.degrees_mul MvPolynomial.degrees_mul
 
 theorem degrees_prod {ι : Type*} (s : Finset ι) (f : ι → MvPolynomial σ R) :
-    (∏ i in s, f i).degrees ≤ ∑ i in s, (f i).degrees := by
-  classical
-  refine' s.induction _ _
-  · simp only [Finset.prod_empty, Finset.sum_empty, degrees_one, le_refl]
-  · intro i s his ih
-    rw [Finset.prod_insert his, Finset.sum_insert his]
-    exact le_trans (degrees_mul _ _) (add_le_add_left ih _)
+    (∏ i in s, f i).degrees ≤ ∑ i in s, (f i).degrees :=
+  Finset.le_prod_of_submultiplicative (Multiplicative.ofAdd ∘ degrees) degrees_one degrees_mul _ _
 #align mv_polynomial.degrees_prod MvPolynomial.degrees_prod
 
-theorem degrees_pow (p : MvPolynomial σ R) : ∀ n : ℕ, (p ^ n).degrees ≤ n • p.degrees
-  | 0 => by rw [pow_zero, degrees_one]; exact Multiset.zero_le _
-  | n + 1 => by
-    rw [pow_succ, add_smul, add_comm, one_smul]
-    exact le_trans (degrees_mul _ _) (add_le_add_left (degrees_pow _ n) _)
+theorem degrees_pow (p : MvPolynomial σ R) (n : ℕ) : (p ^ n).degrees ≤ n • p.degrees := by
+  simpa using degrees_prod (Finset.range n) fun _ ↦ p
 #align mv_polynomial.degrees_pow MvPolynomial.degrees_pow
 
 theorem mem_degrees {p : MvPolynomial σ R} {i : σ} :

Mathlib/Data/Polynomial/Coeff.lean

@@ -66,17 +66,13 @@ theorem support_smul [Monoid S] [DistribMulAction S R] (r : S) (p : R[X]) :
   simp [hi]
 #align polynomial.support_smul Polynomial.support_smul
 
+open scoped Pointwise in
 theorem card_support_mul_le : (p * q).support.card ≤ p.support.card * q.support.card := by
   calc (p * q).support.card
    _ = (p.toFinsupp * q.toFinsupp).support.card := by rw [← support_toFinsupp, toFinsupp_mul]
-   _ ≤ _ := Finset.card_le_card (AddMonoidAlgebra.support_mul p.toFinsupp q.toFinsupp)
-   _ ≤ _ := by
-    apply Finset.card_biUnion_le_card_mul
-    intro _ _
-    rw [← mul_one q.support.card]
-    apply Finset.card_biUnion_le_card_mul
-    intro _ _
-    exact (Finset.card_singleton _) ▸ le_rfl
+   _ ≤ (p.toFinsupp.support + q.toFinsupp.support).card :=
+    Finset.card_le_card (AddMonoidAlgebra.support_mul p.toFinsupp q.toFinsupp)
+   _ ≤ p.support.card * q.support.card := Finset.card_image₂_le ..
 
 /-- `Polynomial.sum` as a linear map. -/
 @[simps]