chore: forward-port mathlib #18682 (#3200)

Mathlib/Data/Finset/Image.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad, Minchao Wu, Mario Carneiro
 
 ! This file was ported from Lean 3 source module data.finset.image
-! leanprover-community/mathlib commit 9003f28797c0664a49e4179487267c494477d853
+! leanprover-community/mathlib commit b685f506164f8d17a6404048bc4d696739c5d976
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -488,10 +488,9 @@ theorem image_inter_subset [DecidableEq α] (f : α → β) (s t : Finset α) :
 
 theorem image_inter_of_injOn [DecidableEq α] {f : α → β} (s t : Finset α)
     (hf : Set.InjOn f (s ∪ t)) : (s ∩ t).image f = s.image f ∩ t.image f :=
-  (image_inter_subset _ _ _).antisymm fun x => by
-    simp only [mem_inter, mem_image]
-    rintro ⟨⟨a, ha, rfl⟩, b, hb, h⟩
-    exact ⟨a, ⟨ha, by rwa [← hf (Or.inr hb) (Or.inl ha) h]⟩, rfl⟩
+  coe_injective <| by
+    push_cast
+    exact Set.image_inter_on fun a ha b hb => hf (Or.inr ha) <| Or.inl hb
 #align finset.image_inter_of_inj_on Finset.image_inter_of_injOn
 
 theorem image_inter [DecidableEq α] (s₁ s₂ : Finset α) (hf : Injective f) :
@@ -532,6 +531,20 @@ theorem image_eq_empty : s.image f = ∅ ↔ s = ∅ :=
    fun e => e.symm ▸ rfl⟩
 #align finset.image_eq_empty Finset.image_eq_empty
 
+theorem image_sdiff [DecidableEq α] {f : α → β} (s t : Finset α) (hf : Injective f) :
+    (s \ t).image f = s.image f \ t.image f :=
+  coe_injective <| by
+    push_cast
+    exact Set.image_diff hf _ _
+#align finset.image_sdiff Finset.image_sdiff
+
+theorem image_symmDiff [DecidableEq α] {f : α → β} (s t : Finset α) (hf : Injective f) :
+    (s ∆ t).image f = s.image f ∆ t.image f :=
+  coe_injective <| by
+    push_cast
+    exact Set.image_symm_diff hf _ _
+#align finset.image_symm_diff Finset.image_symmDiff
+
 @[simp]
 theorem _root_.Disjoint.of_image_finset {s t : Finset α} {f : α → β}
     (h : Disjoint (s.image f) (t.image f)) : Disjoint s t :=

Mathlib/Data/Finset/Pointwise.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Yaël Dillies
 
 ! This file was ported from Lean 3 source module data.finset.pointwise
-! leanprover-community/mathlib commit 517cc149e0b515d2893baa376226ed10feb319c7
+! leanprover-community/mathlib commit b685f506164f8d17a6404048bc4d696739c5d976
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -1697,10 +1697,12 @@ instance isScalarTower'' [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower 
 #align finset.is_scalar_tower'' Finset.isScalarTower''
 #align finset.vadd_assoc_class'' Finset.vaddAssocClass''
 
+@[to_additive]
 instance isCentralScalar [SMul α β] [SMul αᵐᵒᵖ β] [IsCentralScalar α β] :
     IsCentralScalar α (Finset β) :=
   ⟨fun a s => coe_injective <| by simp only [coe_smul_finset, coe_smul, op_smul_eq_smul]⟩
 #align finset.is_central_scalar Finset.isCentralScalar
+#align finset.is_central_vadd Finset.isCentralVAdd
 
 /-- A multiplicative action of a monoid `α` on a type `β` gives a multiplicative action of
 `Finset α` on `Finset β`. -/
@@ -1882,6 +1884,38 @@ theorem subset_smul_finset_iff : s ⊆ a • t ↔ a⁻¹ • s ⊆ t := by
 #align finset.subset_smul_finset_iff Finset.subset_smul_finset_iff
 #align finset.subset_vadd_finset_iff Finset.subset_vadd_finset_iff
 
+@[to_additive]
+theorem smul_finset_inter : a • (s ∩ t) = a • s ∩ a • t :=
+  image_inter _ _ <| MulAction.injective a
+#align finset.smul_finset_inter Finset.smul_finset_inter
+#align finset.vadd_finset_inter Finset.vadd_finset_inter
+
+@[to_additive]
+theorem smul_finset_sdiff : a • (s \ t) = a • s \ a • t :=
+  image_sdiff _ _ <| MulAction.injective a
+#align finset.smul_finset_sdiff Finset.smul_finset_sdiff
+#align finset.vadd_finset_sdiff Finset.vadd_finset_sdiff
+
+@[to_additive]
+theorem smul_finset_symmDiff : a • s ∆ t = (a • s) ∆ (a • t) :=
+  image_symmDiff _ _ <| MulAction.injective a
+#align finset.smul_finset_symm_diff Finset.smul_finset_symmDiff
+#align finset.vadd_finset_symm_diff Finset.vadd_finset_symmDiff
+
+@[to_additive (attr := simp)]
+theorem smul_finset_univ [Fintype β] : a • (univ : Finset β) = univ :=
+  image_univ_of_surjective <| MulAction.surjective a
+#align finset.smul_finset_univ Finset.smul_finset_univ
+#align finset.vadd_finset_univ Finset.vadd_finset_univ
+
+@[to_additive (attr := simp)]
+theorem smul_univ [Fintype β] {s : Finset α} (hs : s.Nonempty) : s • (univ : Finset β) = univ :=
+  coe_injective <| by
+    push_cast
+    exact Set.smul_univ hs
+#align finset.smul_univ Finset.smul_univ
+#align finset.vadd_univ Finset.vadd_univ
+
 @[to_additive (attr := simp)]
 theorem card_smul_finset (a : α) (s : Finset β) : (a • s).card = s.card :=
   card_image_of_injective _ <| MulAction.injective _
@@ -1920,6 +1954,18 @@ theorem subset_smul_finset_iff₀ (ha : a ≠ 0) : s ⊆ a • t ↔ a⁻¹ •
   show _ ⊆ Units.mk0 a ha • _ ↔ _ from subset_smul_finset_iff
 #align finset.subset_smul_finset_iff₀ Finset.subset_smul_finset_iff₀
 
+theorem smul_finset_inter₀ (ha : a ≠ 0) : a • (s ∩ t) = a • s ∩ a • t :=
+  image_inter _ _ <| MulAction.injective₀ ha
+#align finset.smul_finset_inter₀ Finset.smul_finset_inter₀
+
+theorem smul_finset_sdiff₀ (ha : a ≠ 0) : a • (s \ t) = a • s \ a • t :=
+  image_sdiff _ _ <| MulAction.injective₀ ha
+#align finset.smul_finset_sdiff₀ Finset.smul_finset_sdiff₀
+
+theorem smul_finset_symm_diff₀ (ha : a ≠ 0) : a • s ∆ t = (a • s) ∆ (a • t) :=
+  image_symmDiff _ _ <| MulAction.injective₀ ha
+#align finset.smul_finset_symm_diff₀ Finset.smul_finset_symm_diff₀
+
 theorem smul_univ₀ [Fintype β] {s : Finset α} (hs : ¬s ⊆ 0) : s • (univ : Finset β) = univ :=
   coe_injective <| by
     rw [← coe_subset] at hs

Mathlib/Data/Set/Pointwise/SMul.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Floris van Doorn
 
 ! This file was ported from Lean 3 source module data.set.pointwise.smul
-! leanprover-community/mathlib commit c227d107bbada5d0d9d20287e3282c0a7f1651a0
+! leanprover-community/mathlib commit b685f506164f8d17a6404048bc4d696739c5d976
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -468,10 +468,12 @@ instance isScalarTower'' [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower 
 #align set.is_scalar_tower'' Set.isScalarTower''
 #align set.vadd_assoc_class'' Set.vAddAssocClass''
 
+@[to_additive]
 instance isCentralScalar [SMul α β] [SMul αᵐᵒᵖ β] [IsCentralScalar α β] :
     IsCentralScalar α (Set β) :=
   ⟨fun _ S ↦ (congr_arg fun f ↦ f '' S) <| funext fun _ ↦ op_smul_eq_smul _ _⟩
 #align set.is_central_scalar Set.isCentralScalar
+#align set.is_central_vadd Set.isCentralVAdd
 
 /-- A multiplicative action of a monoid `α` on a type `β` gives a multiplicative action of `Set α`
 on `Set β`. -/