feat(data/finset/pointwise): |s| ∣ |s * t| (#18663)

Author: YaelDillies

src/data/finset/basic.lean

@@ -570,6 +570,10 @@ lemma forall_mem_cons (h : a ∉ s) (p : α → Prop) :
   (∀ x, x ∈ cons a s h → p x) ↔ p a ∧ ∀ x, x ∈ s → p x :=
 by simp only [mem_cons, or_imp_distrib, forall_and_distrib, forall_eq]
 
+/-- Useful in proofs by induction. -/
+lemma forall_of_forall_cons {p : α → Prop} {h : a ∉ s} (H : ∀ x, x ∈ cons a s h → p x) (x)
+  (h : x ∈ s) : p x := H _ $ mem_cons.2 $ or.inr h
+
 @[simp] lemma mk_cons {s : multiset α} (h : (a ::ₘ s).nodup) :
   (⟨a ::ₘ s, h⟩ : finset α) = cons a ⟨s, (nodup_cons.1 h).2⟩ (nodup_cons.1 h).1 := rfl
 
@@ -2084,6 +2088,10 @@ lemma forall_mem_insert [decidable_eq α] (a : α) (s : finset α) (p : α → P
   (∀ x, x ∈ insert a s → p x) ↔ p a ∧ ∀ x, x ∈ s → p x :=
 by simp only [mem_insert, or_imp_distrib, forall_and_distrib, forall_eq]
 
+/-- Useful in proofs by induction. -/
+lemma forall_of_forall_insert [decidable_eq α] {p : α → Prop} {a : α} {s : finset α}
+  (H : ∀ x, x ∈ insert a s → p x) (x) (h : x ∈ s) : p x := H _ $ mem_insert_of_mem h
+
 end finset
 
 /-- Equivalence between the set of natural numbers which are `≥ k` and `ℕ`, given by `n → n - k`. -/

src/data/finset/n_ary.lean

@@ -358,6 +358,37 @@ lemma image₂_right_identity {f : γ → β → γ} {b : β} (h : ∀ a, f a b
   image₂ f s {b} = s :=
 by rw [image₂_singleton_right, funext h, image_id']
 
+/-- If each partial application of `f` is injective, and images of `s` under those partial
+applications are disjoint (but not necessarily distinct!), then the size of `t` divides the size of
+`finset.image₂ f s t`. -/
+lemma card_dvd_card_image₂_right (hf : ∀ a ∈ s, injective (f a))
+  (hs : ((λ a, t.image $ f a) '' s).pairwise_disjoint id) :
+  t.card ∣ (image₂ f s t).card :=
+begin
+  classical,
+  induction s using finset.induction with a s ha ih,
+  { simp },
+  specialize ih (forall_of_forall_insert hf)
+    (hs.subset $ set.image_subset _ $ coe_subset.2 $ subset_insert _ _),
+  rw image₂_insert_left,
+  by_cases h : disjoint (image (f a) t) (image₂ f s t),
+  { rw card_union_eq h,
+    exact (card_image_of_injective _ $ hf _ $ mem_insert_self _ _).symm.dvd.add ih },
+  simp_rw [←bUnion_image_left, disjoint_bUnion_right, not_forall] at h,
+  obtain ⟨b, hb, h⟩ := h,
+  rwa union_eq_right_iff_subset.2,
+  exact (hs.eq (set.mem_image_of_mem _ $ mem_insert_self _ _)
+    (set.mem_image_of_mem _ $ mem_insert_of_mem hb) h).trans_subset (image_subset_image₂_right hb),
+end
+
+/-- If each partial application of `f` is injective, and images of `t` under those partial
+applications are disjoint (but not necessarily distinct!), then the size of `s` divides the size of
+`finset.image₂ f s t`. -/
+lemma card_dvd_card_image₂_left (hf : ∀ b ∈ t, injective (λ a, f a b))
+  (ht : ((λ b, s.image $ λ a, f a b) '' t).pairwise_disjoint id) :
+  s.card ∣ (image₂ f s t).card :=
+by { rw ←image₂_swap, exact card_dvd_card_image₂_right hf ht }
+
 variables [decidable_eq α] [decidable_eq β]
 
 lemma image₂_inter_union_subset_union :

src/data/finset/pointwise.lean

@@ -1078,6 +1078,24 @@ coe_injective $ by { push_cast, exact set.smul_univ hs }
 @[simp, to_additive] lemma card_smul_finset (a : α) (s : finset β) : (a • s).card = s.card :=
 card_image_of_injective _ $ mul_action.injective _
 
+/-- If the left cosets of `t` by elements of `s` are disjoint (but not necessarily distinct!), then
+the size of `t` divides the size of `s * t`. -/
+@[to_additive "If the left cosets of `t` by elements of `s` are disjoint (but not necessarily
+distinct!), then the size of `t` divides the size of `s + t`."]
+lemma card_dvd_card_smul_right {s : finset α} :
+  ((• t) '' (s : set α)).pairwise_disjoint id → t.card ∣ (s • t).card :=
+card_dvd_card_image₂_right (λ _ _, mul_action.injective _)
+
+variables [decidable_eq α]
+
+/-- If the right cosets of `s` by elements of `t` are disjoint (but not necessarily distinct!), then
+the size of `s` divides the size of `s * t`. -/
+@[to_additive "If the right cosets of `s` by elements of `t` are disjoint (but not necessarily
+distinct!), then the size of `s` divides the size of `s + t`."]
+lemma card_dvd_card_mul_left {s t : finset α} :
+  ((λ b, s.image $ λ a, a * b) '' (t : set α)).pairwise_disjoint id → s.card ∣ (s * t).card :=
+card_dvd_card_image₂_left (λ _ _, mul_left_injective _)
+
 end group
 
 section group_with_zero