feat: s ∩ t * s ∪ t ⊆ s * t (#1619)

Match leanprover-community/mathlib#17961



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>

Mathlib/Data/Finset/NAry.lean

@@ -4,11 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 
 ! This file was ported from Lean 3 source module data.finset.n_ary
-! leanprover-community/mathlib commit 20715f4ac6819ef2453d9e5106ecd086a5dc2a5e
+! leanprover-community/mathlib commit 517cc149e0b515d2893baa376226ed10feb319c7
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathlib.Data.Finset.Prod
+import Mathlib.Data.Set.Finite
 
 /-!
 # N-ary images of finsets
@@ -28,12 +29,13 @@ and `Set.image2` already fulfills this task.
 
 open Function Set
 
+variable {α α' β β' γ γ' δ δ' ε ε' ζ ζ' ν : Type _}
+
 namespace Finset
 
-variable {α α' β β' γ γ' δ δ' ε ε' ζ ζ' ν : Type _} [DecidableEq α'] [DecidableEq β']
-  [DecidableEq γ] [DecidableEq γ'] [DecidableEq δ] [DecidableEq δ'] [DecidableEq ε] [DecidableEq ε']
-  {f f' : α → β → γ} {g g' : α → β → γ → δ} {s s' : Finset α} {t t' : Finset β} {u u' : Finset γ}
-  {a a' : α} {b b' : β} {c : γ}
+variable [DecidableEq α'] [DecidableEq β'] [DecidableEq γ] [DecidableEq γ'] [DecidableEq δ]
+  [DecidableEq δ'] [DecidableEq ε] [DecidableEq ε'] {f f' : α → β → γ} {g g' : α → β → γ → δ}
+  {s s' : Finset α} {t t' : Finset β} {u u' : Finset γ} {a a' : α} {b b' : β} {c : γ}
 
 /-- The image of a binary function `f : α → β → γ` as a function `Finset α → Finset β → Finset γ`.
 Mathematically this should be thought of as the image of the corresponding function `α × β → γ`. -/
@@ -498,4 +500,37 @@ theorem image₂_right_identity {f : γ → β → γ} {b : β} (h : ∀ a, f a
     image₂ f s {b} = s := by rw [image₂_singleton_right, funext h, image_id']
 #align finset.image₂_right_identity Finset.image₂_right_identity
 
+variable [DecidableEq α] [DecidableEq β]
+
+theorem image₂_inter_union_subset {f : α → α → β} {s t : Finset α} (hf : ∀ a b, f a b = f b a) :
+    image₂ f (s ∩ t) (s ∪ t) ⊆ image₂ f s t :=
+  coe_subset.1 <| by
+    push_cast
+    exact image2_inter_union_subset hf
+#align finset.image₂_inter_union_subset Finset.image₂_inter_union_subset
+
+theorem image₂_union_inter_subset {f : α → α → β} {s t : Finset α} (hf : ∀ a b, f a b = f b a) :
+    image₂ f (s ∪ t) (s ∩ t) ⊆ image₂ f s t :=
+  coe_subset.1 <| by
+    push_cast
+    exact image2_union_inter_subset hf
+#align finset.image₂_union_inter_subset Finset.image₂_union_inter_subset
+
 end Finset
+
+namespace Set
+
+variable [DecidableEq γ] {s : Set α} {t : Set β}
+
+@[simp]
+theorem toFinset_image2 (f : α → β → γ) (s : Set α) (t : Set β) [Fintype s] [Fintype t]
+    [Fintype (image2 f s t)] : (image2 f s t).toFinset = Finset.image₂ f s.toFinset t.toFinset :=
+  Finset.coe_injective <| by simp
+#align set.to_finset_image2 Set.toFinset_image2
+
+theorem Finite.toFinset_image2 (f : α → β → γ) (hs : s.Finite) (ht : t.Finite)
+    (hf := hs.image2 f ht) : hf.toFinset = Finset.image₂ f hs.toFinset ht.toFinset :=
+  Finset.coe_injective <| by simp
+#align set.finite.to_finset_image2 Set.Finite.toFinset_image2
+
+end Set

Mathlib/Data/Finset/Pointwise.lean

@@ -4,12 +4,13 @@ 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 f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
+! leanprover-community/mathlib commit 517cc149e0b515d2893baa376226ed10feb319c7
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathlib.Data.Finset.NAry
 import Mathlib.Data.Finset.Preimage
+import Mathlib.Data.Set.Pointwise.Finite
 import Mathlib.Data.Set.Pointwise.SMul
 import Mathlib.Data.Set.Pointwise.ListOfFn
 
@@ -140,6 +141,12 @@ theorem Nonempty.subset_one_iff (h : s.Nonempty) : s ⊆ 1 ↔ s = 1 :=
 #align finset.nonempty.subset_one_iff Finset.Nonempty.subset_one_iff
 #align finset.nonempty.subset_zero_iff Finset.Nonempty.subset_zero_iff
 
+@[to_additive (attr := simp)]
+theorem card_one : (1 : Finset α).card = 1 :=
+  card_singleton _
+#align finset.card_one Finset.card_one
+#align finset.card_zero Finset.card_zero
+
 /-- The singleton operation as a `OneHom`. -/
 @[to_additive "The singleton operation as a `ZeroHom`."]
 def singletonOneHom : OneHom α (Finset α) :=
@@ -719,13 +726,31 @@ protected def semigroup [Semigroup α] : Semigroup (Finset α) :=
 #align finset.semigroup Finset.semigroup
 #align finset.add_semigroup Finset.addSemigroup
 
+section CommSemigroup
+
+variable [CommSemigroup α] {s t : Finset α}
+
 /-- `Finset α` is a `CommSemigroup` under pointwise operations if `α` is. -/
 @[to_additive "`Finset α` is an `AddCommSemigroup` under pointwise operations if `α` is. "]
-protected def commSemigroup [CommSemigroup α] : CommSemigroup (Finset α) :=
+protected def commSemigroup : CommSemigroup (Finset α) :=
   coe_injective.commSemigroup _ coe_mul
 #align finset.comm_semigroup Finset.commSemigroup
 #align finset.add_comm_semigroup Finset.addCommSemigroup
 
+@[to_additive]
+theorem inter_mul_union_subset : s ∩ t * (s ∪ t) ⊆ s * t :=
+  image₂_inter_union_subset mul_comm
+#align finset.inter_mul_union_subset Finset.inter_mul_union_subset
+#align finset.inter_add_union_subset Finset.inter_add_union_subset
+
+@[to_additive]
+theorem union_mul_inter_subset : (s ∪ t) * (s ∩ t) ⊆ s * t :=
+  image₂_union_inter_subset mul_comm
+#align finset.union_mul_inter_subset Finset.union_mul_inter_subset
+#align finset.union_add_inter_subset Finset.union_add_inter_subset
+
+end CommSemigroup
+
 section MulOneClass
 
 variable [MulOneClass α]
@@ -1799,6 +1824,20 @@ end
 
 open Pointwise
 
+@[to_additive]
+theorem image_smul_comm [DecidableEq β] [DecidableEq γ] [SMul α β] [SMul α γ] (f : β → γ) (a : α)
+    (s : Finset β) : (∀ b, f (a • b) = a • f b) → (a • s).image f = a • s.image f :=
+  image_comm
+#align finset.image_smul_comm Finset.image_smul_comm
+#align finset.image_vadd_comm Finset.image_vadd_comm
+
+@[to_additive]
+theorem image_smul_distrib [DecidableEq α] [DecidableEq β] [Monoid α] [Monoid β]
+    [MonoidHomClass F α β] (f : F) (a : α) (s : Finset α) : (a • s).image f = f a • s.image f :=
+  image_comm <| map_mul _ _
+#align finset.image_smul_distrib Finset.image_smul_distrib
+#align finset.image_vadd_distrib Finset.image_vadd_distrib
+
 section Group
 
 variable [DecidableEq β] [Group α] [MulAction α β] {s t : Finset β} {a : α} {b : β}
@@ -1843,6 +1882,12 @@ 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 (attr := simp)]
+theorem card_smul_finset (a : α) (s : Finset β) : (a • s).card = s.card :=
+  card_image_of_injective _ <| MulAction.injective _
+#align finset.card_smul_finset Finset.card_smul_finset
+#align finset.card_vadd_finset Finset.card_vadd_finset
+
 end Group
 
 section GroupWithZero
@@ -1978,3 +2023,105 @@ protected theorem neg_smul [DecidableEq α] : -s • t = -(s • t) := by
 end Ring
 
 end Finset
+
+open Pointwise
+
+namespace Set
+
+section One
+
+variable [One α]
+
+@[to_additive (attr := simp)]
+theorem toFinset_one : (1 : Set α).toFinset = 1 :=
+  rfl
+#align set.to_finset_one Set.toFinset_one
+#align set.to_finset_zero Set.toFinset_zero
+
+-- Porting note: should take priority over `Finite.toFinset_singleton`
+@[to_additive (attr := simp high)]
+theorem Finite.toFinset_one (h : (1 : Set α).Finite := finite_one) : h.toFinset = 1 :=
+  Finite.toFinset_singleton _
+#align set.finite.to_finset_one Set.Finite.toFinset_one
+#align set.finite.to_finset_zero Set.Finite.toFinset_zero
+
+end One
+
+section Mul
+
+variable [DecidableEq α] [Mul α] {s t : Set α}
+
+@[to_additive (attr := simp)]
+theorem toFinset_mul (s t : Set α) [Fintype s] [Fintype t] [Fintype ↑(s * t)] :
+    (s * t).toFinset = s.toFinset * t.toFinset :=
+  toFinset_image2 _ _ _
+#align set.to_finset_mul Set.toFinset_mul
+#align set.to_finset_add Set.toFinset_add
+
+@[to_additive]
+theorem Finite.toFinset_mul (hs : s.Finite) (ht : t.Finite) (hf := hs.mul ht) :
+    hf.toFinset = hs.toFinset * ht.toFinset :=
+  Finite.toFinset_image2 _ _ _
+#align set.finite.to_finset_mul Set.Finite.toFinset_mul
+#align set.finite.to_finset_add Set.Finite.toFinset_add
+
+end Mul
+
+section SMul
+
+variable [SMul α β] [DecidableEq β] {a : α} {s : Set α} {t : Set β}
+
+@[to_additive (attr := simp)]
+theorem toFinset_smul (s : Set α) (t : Set β) [Fintype s] [Fintype t] [Fintype ↑(s • t)] :
+    (s • t).toFinset = s.toFinset • t.toFinset :=
+  toFinset_image2 _ _ _
+#align set.to_finset_smul Set.toFinset_smul
+#align set.to_finset_vadd Set.toFinset_vadd
+
+@[to_additive]
+theorem Finite.toFinset_smul (hs : s.Finite) (ht : t.Finite) (hf := hs.smul ht) :
+    hf.toFinset = hs.toFinset • ht.toFinset :=
+  Finite.toFinset_image2 _ _ _
+#align set.finite.to_finset_smul Set.Finite.toFinset_smul
+#align set.finite.to_finset_vadd Set.Finite.toFinset_vadd
+
+end SMul
+
+section SMul
+
+variable [DecidableEq β] [SMul α β] {a : α} {s : Set β}
+
+@[to_additive (attr := simp)]
+theorem toFinset_smul_set (a : α) (s : Set β) [Fintype s] [Fintype ↑(a • s)] :
+    (a • s).toFinset = a • s.toFinset :=
+  toFinset_image _ _
+#align set.to_finset_smul_set Set.toFinset_smul_set
+#align set.to_finset_vadd_set Set.toFinset_vadd_set
+
+@[to_additive]
+theorem Finite.toFinset_smul_set (hs : s.Finite) (hf : (a • s).Finite := hs.smul_set) :
+    hf.toFinset = a • hs.toFinset :=
+  Finite.toFinset_image _ _ _
+#align set.finite.to_finset_smul_set Set.Finite.toFinset_smul_set
+#align set.finite.to_finset_vadd_set Set.Finite.toFinset_vadd_set
+
+end SMul
+
+section VSub
+
+variable [DecidableEq α] [VSub α β] {s t : Set β}
+
+@[simp]
+theorem toFinset_vsub (s t : Set β) [Fintype s] [Fintype t] [Fintype ↑(s -ᵥ t)] :
+    (s -ᵥ t : Set α).toFinset = s.toFinset -ᵥ t.toFinset :=
+  toFinset_image2 _ _ _
+#align set.to_finset_vsub Set.toFinset_vsub
+
+theorem Finite.toFinset_vsub (hs : s.Finite) (ht : t.Finite) (hf := hs.vsub ht) :
+    hf.toFinset = hs.toFinset -ᵥ ht.toFinset :=
+  Finite.toFinset_image2 _ _ _
+#align set.finite.to_finset_vsub Set.Finite.toFinset_vsub
+
+end VSub
+
+end Set

Mathlib/Data/Polynomial/RingDivision.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker, Johan Commelin
 
 ! This file was ported from Lean 3 source module data.polynomial.ring_division
-! leanprover-community/mathlib commit cbdf7b565832144d024caa5a550117c6df0204a5
+! leanprover-community/mathlib commit 517cc149e0b515d2893baa376226ed10feb319c7
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -792,7 +792,7 @@ theorem nthRoots_zero (r : R) : nthRoots 0 r = 0 := by
 theorem card_nthRoots (n : ℕ) (a : R) : Multiset.card (nthRoots n a) ≤ n :=
   if hn : n = 0 then
     if h : (X : R[X]) ^ n - C a = 0 then by
-      simp [Nat.zero_le, nthRoots, roots, h, dif_pos rfl, empty_eq_zero, card_zero]
+      simp [Nat.zero_le, nthRoots, roots, h, dif_pos rfl, empty_eq_zero, Multiset.card_zero]
     else
       WithBot.coe_le_coe.1
         (le_trans (card_roots h)

Mathlib/Data/Set/Finite.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Kyle Miller
 
 ! This file was ported from Lean 3 source module data.set.finite
-! leanprover-community/mathlib commit 1f0096e6caa61e9c849ec2adbd227e960e9dff58
+! leanprover-community/mathlib commit 517cc149e0b515d2893baa376226ed10feb319c7
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -263,7 +263,6 @@ protected theorem toFinset_empty (h : (∅ : Set α).Finite) : h.toFinset = ∅
   simp
 #align set.finite.to_finset_empty Set.Finite.toFinset_empty
 
--- Note: Not `simp` because `Set.Finite.toFinset_setOf` already proves it
 protected theorem toFinset_univ [Fintype α] (h : (Set.univ : Set α).Finite) :
     h.toFinset = Finset.univ := by
   simp

Mathlib/Data/Set/NAry.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 
 ! This file was ported from Lean 3 source module data.set.n_ary
-! leanprover-community/mathlib commit 20715f4ac6819ef2453d9e5106ecd086a5dc2a5e
+! leanprover-community/mathlib commit 517cc149e0b515d2893baa376226ed10feb319c7
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -430,4 +430,18 @@ lemma image2_right_identity {f : α → β → α} {b : β} (h : ∀ a, f a b =
   rw [image2_singleton_right, funext h, image_id']
 #align set.image2_right_identity Set.image2_right_identity
 
+theorem image2_inter_union_subset {f : α → α → β} {s t : Set α} (hf : ∀ a b, f a b = f b a) :
+    image2 f (s ∩ t) (s ∪ t) ⊆ image2 f s t := by
+  rintro _ ⟨a, b, ha, hb | hb, rfl⟩
+  · rw [hf]
+    exact mem_image2_of_mem hb ha.2
+  · exact mem_image2_of_mem ha.1 hb
+#align set.image2_inter_union_subset Set.image2_inter_union_subset
+
+theorem image2_union_inter_subset {f : α → α → β} {s t : Set α} (hf : ∀ a b, f a b = f b a) :
+    image2 f (s ∪ t) (s ∩ t) ⊆ image2 f s t := by
+  rw [image2_comm hf]
+  exact image2_inter_union_subset hf
+#align set.image2_union_inter_subset Set.image2_union_inter_subset
+
 end Set

Mathlib/Data/Set/Pointwise/Basic.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.basic
-! leanprover-community/mathlib commit 207cfac9fcd06138865b5d04f7091e46d9320432
+! leanprover-community/mathlib commit 517cc149e0b515d2893baa376226ed10feb319c7
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -827,13 +827,31 @@ protected noncomputable def semigroup [Semigroup α] : Semigroup (Set α) :=
 #align set.semigroup Set.semigroup
 #align set.add_semigroup Set.addSemigroup
 
+section CommSemigroup
+
+variable [CommSemigroup α] {s t : Set α}
+
 /-- `Set α` is a `CommSemigroup` under pointwise operations if `α` is. -/
 @[to_additive "`Set α` is an `AddCommSemigroup` under pointwise operations if `α` is."]
-protected noncomputable def commSemigroup [CommSemigroup α] : CommSemigroup (Set α) :=
+protected noncomputable def commSemigroup : CommSemigroup (Set α) :=
   { Set.semigroup with mul_comm := fun _ _ => image2_comm mul_comm }
 #align set.comm_semigroup Set.commSemigroup
 #align set.add_comm_semigroup Set.addCommSemigroup
 
+@[to_additive]
+theorem inter_mul_union_subset : s ∩ t * (s ∪ t) ⊆ s * t :=
+  image2_inter_union_subset mul_comm
+#align set.inter_mul_union_subset Set.inter_mul_union_subset
+#align set.inter_add_union_subset Set.inter_add_union_subset
+
+@[to_additive]
+theorem union_mul_inter_subset : (s ∪ t) * (s ∩ t) ⊆ s * t :=
+  image2_union_inter_subset mul_comm
+#align set.union_mul_inter_subset Set.union_mul_inter_subset
+#align set.union_add_inter_subset Set.union_add_inter_subset
+
+end CommSemigroup
+
 section MulOneClass
 
 variable [MulOneClass α]