From 1406534bcd66081dd9610a3891355c9e411ca0ea Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Fri, 29 Jul 2022 12:50:09 +0000
Subject: [PATCH] feat(data/finset/pointwise): Singleton arithmetic (#15435)

Lemmas about pointwise operations with a singleton. Also make `s` explicit in `finset.card_inv`.
---
 src/data/finset/n_ary.lean     | 35 ++++++++++++++++++++++++
 src/data/finset/pointwise.lean | 49 ++++++++++++++++++++++++++--------
 2 files changed, 73 insertions(+), 11 deletions(-)

diff --git a/src/data/finset/n_ary.lean b/src/data/finset/n_ary.lean
index 43dc62905ad72..174012d5c2e35 100644
--- a/src/data/finset/n_ary.lean
+++ b/src/data/finset/n_ary.lean
@@ -140,6 +140,41 @@ begin
     mem_insert_self _ _, ha⟩, h.trans $ image₂_subset (subset_insert _ _) $ subset_insert _ _⟩⟩,
 end
 
+variables (s t)
+
+lemma card_image₂_singleton_left (hf : injective (f a)) : (image₂ f {a} t).card = t.card :=
+by rw [image₂_singleton_left, card_image_of_injective _ hf]
+
+lemma card_image₂_singleton_right (hf : injective (λ a, f a b)) : (image₂ f s {b}).card = s.card :=
+by rw [image₂_singleton_right, card_image_of_injective _ hf]
+
+lemma image₂_singleton_inter [decidable_eq β] (t₁ t₂ : finset β) (hf : injective (f a)) :
+  image₂ f {a} (t₁ ∩ t₂) = image₂ f {a} t₁ ∩ image₂ f {a} t₂ :=
+by simp_rw [image₂_singleton_left, image_inter _ _ hf]
+
+lemma image₂_inter_singleton [decidable_eq α] (s₁ s₂ : finset α) (hf : injective (λ a, f a b)) :
+  image₂ f (s₁ ∩ s₂) {b} = image₂ f s₁ {b} ∩ image₂ f s₂ {b} :=
+by simp_rw [image₂_singleton_right, image_inter _ _ hf]
+
+lemma card_le_card_image₂_left {s : finset α} (hs : s.nonempty) (hf : ∀ a, injective (f a)) :
+  t.card ≤ (image₂ f s t).card :=
+begin
+  obtain ⟨a, ha⟩ := hs,
+  rw ←card_image₂_singleton_left _ (hf a),
+  exact card_le_of_subset (image₂_subset_right $ singleton_subset_iff.2 ha),
+end
+
+lemma card_le_card_image₂_right {t : finset β} (ht : t.nonempty)
+  (hf : ∀ b, injective (λ a, f a b)) :
+  s.card ≤ (image₂ f s t).card :=
+begin
+  obtain ⟨b, hb⟩ := ht,
+  rw ←card_image₂_singleton_right _ (hf b),
+  exact card_le_of_subset (image₂_subset_left $ singleton_subset_iff.2 hb),
+end
+
+variables {s t}
+
 lemma bUnion_image_left : s.bUnion (λ a, t.image $ f a) = image₂ f s t :=
 coe_injective $ by { push_cast, exact set.Union_image_left _ }
 
diff --git a/src/data/finset/pointwise.lean b/src/data/finset/pointwise.lean
index 1e7b4eee1df73..cd6fed1ef1145 100644
--- a/src/data/finset/pointwise.lean
+++ b/src/data/finset/pointwise.lean
@@ -124,10 +124,10 @@ end has_inv
 open_locale pointwise
 
 section has_involutive_inv
-variables [decidable_eq α] [has_involutive_inv α] {s t : finset α}
+variables [decidable_eq α] [has_involutive_inv α] (s : finset α)
 
 @[simp, norm_cast, to_additive]
-lemma coe_inv (s : finset α) : ↑(s⁻¹) = (s : set α)⁻¹ := coe_image.trans set.image_inv
+lemma coe_inv : ↑(s⁻¹) = (s : set α)⁻¹ := coe_image.trans set.image_inv
 
 @[simp, to_additive] lemma card_inv : s⁻¹.card = s.card := card_image_of_injective _ inv_injective
 
@@ -178,9 +178,8 @@ image₂_nonempty_iff
 @[to_additive] lemma nonempty.of_mul_left : (s * t).nonempty → s.nonempty := nonempty.of_image₂_left
 @[to_additive] lemma nonempty.of_mul_right : (s * t).nonempty → t.nonempty :=
 nonempty.of_image₂_right
-@[simp, to_additive] lemma mul_singleton (a : α) : s * {a} = s.image (* a) := image₂_singleton_right
-@[simp, to_additive] lemma singleton_mul (a : α) : {a} * s = s.image ((*) a) :=
-image₂_singleton_left
+@[to_additive] lemma mul_singleton (a : α) : s * {a} = s.image (* a) := image₂_singleton_right
+@[to_additive] lemma singleton_mul (a : α) : {a} * s = s.image ((*) a) := image₂_singleton_left
 @[simp, to_additive] lemma singleton_mul_singleton (a b : α) : ({a} : finset α) * {b} = {a * b} :=
 image₂_singleton
 
@@ -643,9 +642,9 @@ image₂_nonempty_iff
 nonempty.of_image₂_left
 @[to_additive] lemma nonempty.of_smul_right : (s • t).nonempty → t.nonempty :=
 nonempty.of_image₂_right
-@[simp, to_additive] lemma smul_singleton (b : β) : s • ({b} : finset β) = s.image (• b) :=
+@[to_additive] lemma smul_singleton (b : β) : s • ({b} : finset β) = s.image (• b) :=
 image₂_singleton_right
-@[simp, to_additive] lemma singleton_smul (a : α) : ({a} : finset α) • t = t.image ((•) a) :=
+@[to_additive] lemma singleton_smul (a : α) : ({a} : finset α) • t = t.image ((•) a) :=
 image₂_singleton_left
 @[simp, to_additive] lemma singleton_smul_singleton (a : α) (b : β) :
   ({a} : finset α) • ({b} : finset β) = {a • b} :=
@@ -709,8 +708,7 @@ lemma nonempty.of_vsub_left : (s -ᵥ t : finset α).nonempty → s.nonempty :=
 lemma nonempty.of_vsub_right : (s -ᵥ t : finset α).nonempty → t.nonempty := nonempty.of_image₂_right
 @[simp] lemma vsub_singleton (b : β) : s -ᵥ ({b} : finset β) = s.image (-ᵥ b) :=
 image₂_singleton_right
-@[simp] lemma singleton_vsub (a : β) : ({a} : finset β) -ᵥ t = t.image ((-ᵥ) a) :=
-image₂_singleton_left
+lemma singleton_vsub (a : β) : ({a} : finset β) -ᵥ t = t.image ((-ᵥ) a) := image₂_singleton_left
 @[simp] lemma singleton_vsub_singleton (a b : β) : ({a} : finset β) -ᵥ {b} = {a -ᵥ b} :=
 image₂_singleton
 
@@ -888,11 +886,40 @@ coe_injective.no_zero_smul_divisors _ coe_zero coe_smul_finset
 
 end instances
 
-@[to_additive] lemma pairwise_disjoint_smul_iff [decidable_eq α] [left_cancel_semigroup α]
-  {s : set α} {t : finset α} :
+section left_cancel_semigroup
+variables [left_cancel_semigroup α] [decidable_eq α] (s t : finset α) (a : α)
+
+@[to_additive] lemma pairwise_disjoint_smul_iff {s : set α} {t : finset α} :
   s.pairwise_disjoint (• t) ↔ ((s : set α) ×ˢ (t : set α) : set (α × α)).inj_on (λ p, p.1 * p.2) :=
 by simp_rw [←pairwise_disjoint_coe, coe_smul_finset, set.pairwise_disjoint_smul_iff]
 
+@[simp, to_additive] lemma card_singleton_mul : ({a} * t).card = t.card :=
+card_image₂_singleton_left _ $ mul_right_injective _
+
+@[to_additive] lemma singleton_mul_inter : {a} * (s ∩ t) = ({a} * s) ∩ ({a} * t) :=
+image₂_singleton_inter _ _ $ mul_right_injective _
+
+@[to_additive] lemma card_le_card_mul_left {s : finset α} (hs : s.nonempty) :
+  t.card ≤ (s * t).card :=
+card_le_card_image₂_left _ hs mul_right_injective
+
+end left_cancel_semigroup
+
+section
+variables [right_cancel_semigroup α] [decidable_eq α] (s t : finset α) (a : α)
+
+@[simp, to_additive] lemma card_mul_singleton : (s * {a}).card = s.card :=
+card_image₂_singleton_right _ $ mul_left_injective _
+
+@[to_additive] lemma inter_mul_singleton : (s ∩ t) * {a} = (s * {a}) ∩ (t * {a}) :=
+image₂_inter_singleton _ _ $ mul_left_injective _
+
+@[to_additive] lemma card_le_card_mul_right {t : finset α} (ht : t.nonempty) :
+  s.card ≤ (s * t).card :=
+card_le_card_image₂_right _ ht mul_left_injective
+
+end
+
 open_locale pointwise
 
 section group