feat(Pointwise): add smul_set_prod and smul_set_pi

Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

@@ -870,6 +870,21 @@ lemma smul_set_iInter₂_subset (a : α) (t : ∀ i, κ i → Set β) :
 
 end SMulSet
 
+section Pi
+
+variable {M ι : Type*} {π : ι → Type*} [∀ i, SMul M (π i)]
+
+@[to_additive]
+theorem smul_set_pi_of_surjective (c : M) (I : Set ι) (s : ∀ i, Set (π i))
+    (hsurj : ∀ i ∉ I, Function.Surjective (c • · : π i → π i)) : c • I.pi s = I.pi (c • s ·) :=
+  piMap_image_pi hsurj s
+
+@[to_additive]
+theorem smul_set_univ_pi (c : M) (s : ∀ i, Set (π i)) : c • univ.pi s = univ.pi (c • s ·) :=
+  piMap_image_univ_pi _ s
+
+end Pi
+
 variable {s : Set α} {t : Set β} {a : α} {b : β}
 
 @[to_additive]

Mathlib/Data/Set/Pointwise/SMul.lean

@@ -207,6 +207,26 @@ open scoped RightActions in
 lemma image_op_smul_distrib [MulOneClass α] [MulOneClass β] [FunLike F α β] [MonoidHomClass F α β]
     (f : F) (a : α) (s : Set α) : f '' (s <• a) = f '' s <• f a := image_comm fun _ ↦ map_mul _ _ _
 
+@[to_additive]
+theorem smul_set_prod {M : Type*} [SMul M α] [SMul M β] (c : M) (s : Set α) (t : Set β) :
+    c • (s ×ˢ t) = (c • s) ×ˢ (c • t) :=
+  prodMap_image_prod (c • ·) (c • ·) s t
+
+@[to_additive]
+theorem smul_set_pi {G ι : Type*} {α : ι → Type*} [Group G] [∀ i, MulAction G (α i)]
+    (c : G) (I : Set ι) (s : ∀ i, Set (α i)) : c • I.pi s = I.pi fun i ↦ c • s i :=
+  smul_set_pi_of_surjective c I s fun _ _ ↦ (MulAction.bijective c).surjective
+
+@[to_additive]
+theorem smul_set_pi_of_isUnit {M ι : Type*} {α : ι → Type*} [Monoid M] [∀ i, MulAction M (α i)]
+    {c : M} (hc : IsUnit c) (I : Set ι) (s : ∀ i, Set (α i)) : c • I.pi s = I.pi (c • s ·) := by
+  lift c to Mˣ using hc
+  exact smul_set_pi c I s
+
+theorem smul_set_pi₀ {M ι : Type*} {α : ι → Type*} [GroupWithZero M] [∀ i, MulAction M (α i)]
+    {c : M} (hc : c ≠ 0) (I : Set ι) (s : ∀ i, Set (α i)) : c • I.pi s = I.pi (c • s ·) :=
+  smul_set_pi_of_isUnit (.mk0 _ hc) I s
+
 section SMul
 
 variable [SMul αᵐᵒᵖ β] [SMul β γ] [SMul α γ]