From 8a9d4f034673409da1c1f45e4737c26168e99164 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Thu, 7 Dec 2023 09:40:49 +0000
Subject: [PATCH] feat(Set/Pointwise/SMul): add 2 missing instances (#8856)

---
 Mathlib/Data/Finset/Pointwise.lean   | 30 ++++++++++++++++++----------
 Mathlib/Data/Set/Pointwise/SMul.lean | 28 ++++++++++++++++++--------
 2 files changed, 39 insertions(+), 19 deletions(-)

diff --git a/Mathlib/Data/Finset/Pointwise.lean b/Mathlib/Data/Finset/Pointwise.lean
index 36eeaeb618d61..1b20af2e9d3d9 100644
--- a/Mathlib/Data/Finset/Pointwise.lean
+++ b/Mathlib/Data/Finset/Pointwise.lean
@@ -1772,6 +1772,22 @@ scoped[Pointwise]
   attribute [instance]
     Finset.mulActionFinset Finset.addActionFinset Finset.mulAction Finset.addAction
 
+/-- If scalar multiplication by elements of `α` sends `(0 : β)` to zero,
+then the same is true for `(0 : Finset β)`. -/
+protected def smulZeroClassFinset [Zero β] [SMulZeroClass α β] :
+    SMulZeroClass α (Finset β) :=
+  coe_injective.smulZeroClass ⟨(↑), coe_zero⟩ coe_smul_finset
+
+scoped[Pointwise] attribute [instance] Finset.smulZeroClassFinset
+
+/-- If the scalar multiplication `(· • ·) : α → β → β` is distributive,
+then so is `(· • ·) : α → Finset β → Finset β`. -/
+protected def distribSMulFinset [AddZeroClass β] [DistribSMul α β] :
+    DistribSMul α (Finset β) :=
+  coe_injective.distribSMul coeAddMonoidHom coe_smul_finset
+
+scoped[Pointwise] attribute [instance] Finset.distribSMulFinset
+
 /-- A distributive multiplicative action of a monoid on an additive monoid `β` gives a distributive
 multiplicative action on `Finset β`. -/
 protected def distribMulActionFinset [Monoid α] [AddMonoid β] [DistribMulAction α β] :
@@ -1792,17 +1808,9 @@ instance [DecidableEq α] [Zero α] [Mul α] [NoZeroDivisors α] : NoZeroDivisor
   Function.Injective.noZeroDivisors (↑) coe_injective coe_zero coe_mul
 
 instance noZeroSMulDivisors [Zero α] [Zero β] [SMul α β] [NoZeroSMulDivisors α β] :
-    NoZeroSMulDivisors (Finset α) (Finset β) :=
-  ⟨by
-    intro s t h
-    by_contra H
-    have hst : (s • t).Nonempty := h.symm.subst zero_nonempty
-    rw [← hst.of_smul_left.subset_zero_iff, ← hst.of_smul_right.subset_zero_iff] at H
-    push_neg at H
-    simp_rw [not_subset, mem_zero] at H
-    obtain ⟨⟨a, hs, ha⟩, b, ht, hb⟩ := H
-    exact (eq_zero_or_eq_zero_of_smul_eq_zero <| mem_zero.1 <| subset_of_eq h
-      <| smul_mem_smul hs ht).elim ha hb⟩
+    NoZeroSMulDivisors (Finset α) (Finset β) where
+  eq_zero_or_eq_zero_of_smul_eq_zero {s t} := by
+    exact_mod_cast eq_zero_or_eq_zero_of_smul_eq_zero (c := s.toSet) (x := t.toSet)
 
 instance noZeroSMulDivisors_finset [Zero α] [Zero β] [SMul α β] [NoZeroSMulDivisors α β] :
     NoZeroSMulDivisors α (Finset β) :=
diff --git a/Mathlib/Data/Set/Pointwise/SMul.lean b/Mathlib/Data/Set/Pointwise/SMul.lean
index 4ec93b98e086f..c070bfffeb122 100644
--- a/Mathlib/Data/Set/Pointwise/SMul.lean
+++ b/Mathlib/Data/Set/Pointwise/SMul.lean
@@ -532,23 +532,35 @@ protected def mulAction [Monoid α] [MulAction α β] : MulAction (Set α) (Set
 @[to_additive
       "An additive action of an additive monoid on a type `β` gives an additive action on `Set β`."]
 protected def mulActionSet [Monoid α] [MulAction α β] : MulAction α (Set β) where
-  mul_smul := by
-    intros
-    simp only [← image_smul, image_image, ← mul_smul]
-  one_smul := by
-    intros
-    simp only [← image_smul, one_smul, image_id']
+  mul_smul _ _ _ := by simp only [← image_smul, image_image, ← mul_smul]
+  one_smul _ := by simp only [← image_smul, one_smul, image_id']
 #align set.mul_action_set Set.mulActionSet
 #align set.add_action_set Set.addActionSet
 
 scoped[Pointwise] attribute [instance] Set.mulActionSet Set.addActionSet Set.mulAction Set.addAction
 
+/-- If scalar multiplication by elements of `α` sends `(0 : β)` to zero,
+then the same is true for `(0 : Set β)`. -/
+protected def smulZeroClassSet [Zero β] [SMulZeroClass α β] :
+    SMulZeroClass α (Set β) where
+  smul_zero _ := image_singleton.trans <| by rw [smul_zero, singleton_zero]
+
+scoped[Pointwise] attribute [instance] Set.smulZeroClassSet
+
+/-- If the scalar multiplication `(· • ·) : α → β → β` is distributive,
+then so is `(· • ·) : α → Set β → Set β`. -/
+protected def distribSMulSet [AddZeroClass β] [DistribSMul α β] :
+    DistribSMul α (Set β) where
+  smul_add _ _ _ := image_image2_distrib <| smul_add _
+
+scoped[Pointwise] attribute [instance] Set.distribSMulSet
+
 /-- A distributive multiplicative action of a monoid on an additive monoid `β` gives a distributive
 multiplicative action on `Set β`. -/
 protected def distribMulActionSet [Monoid α] [AddMonoid β] [DistribMulAction α β] :
     DistribMulAction α (Set β) where
-  smul_add _ _ _ := image_image2_distrib <| smul_add _
-  smul_zero _ := image_singleton.trans <| by rw [smul_zero, singleton_zero]
+  smul_add := smul_add
+  smul_zero := smul_zero
 #align set.distrib_mul_action_set Set.distribMulActionSet
 
 /-- A multiplicative action of a monoid on a monoid `β` gives a multiplicative action on `Set β`. -/