feat(data/finset): add some lemmas about finset.disj_union (#14910)

Co-authored-by: YaelDillies <yael.dillies@gmail.com>

Author: eric-wieser

src/algebra/big_operators/basic.lean

@@ -254,6 +254,10 @@ lemma prod_congr (h : s₁ = s₂) : (∀ x ∈ s₂, f x = g x) → s₁.prod f
 by rw [h]; exact fold_congr
 attribute [congr] finset.sum_congr
 
+@[to_additive]
+lemma prod_disj_union (h) : ∏ x in s₁.disj_union s₂ h, f x = (∏ x in s₁, f x) * ∏ x in s₂, f x :=
+by { refine eq.trans _ (fold_disj_union h), rw one_mul, refl }
+
 @[to_additive]
 lemma prod_union_inter [decidable_eq α] :
   (∏ x in (s₁ ∪ s₂), f x) * (∏ x in (s₁ ∩ s₂), f x) = (∏ x in s₁, f x) * (∏ x in s₂, f x) :=

src/data/finset/basic.lean

@@ -1861,6 +1861,11 @@ lemma mem_map' (f : α ↪ β) {a} {s : finset α} : f a ∈ s.map f ↔ a ∈ s
 
 lemma mem_map_of_mem (f : α ↪ β) {a} {s : finset α} : a ∈ s → f a ∈ s.map f := (mem_map' _).2
 
+lemma forall_mem_map {f : α ↪ β} {s : finset α} {p : Π a, a ∈ s.map f → Prop} :
+  (∀ y ∈ s.map f, p y H) ↔ ∀ x ∈ s, p (f x) (mem_map_of_mem _ H) :=
+⟨λ h y hy, h (f y) (mem_map_of_mem _ hy), λ h x hx,
+  by { obtain ⟨y, hy, rfl⟩ := mem_map.1 hx, exact h _ hy }⟩
+
 lemma apply_coe_mem_map (f : α ↪ β) (s : finset α) (x : s) : f x ∈ s.map f :=
 mem_map_of_mem f x.prop
 
@@ -1910,6 +1915,20 @@ theorem map_filter {p : β → Prop} [decidable_pred p] :
   (s.map f).filter p = (s.filter (p ∘ f)).map f :=
 eq_of_veq (map_filter _ _ _)
 
+/-- A helper lemma to produce a default proof for `finset.map_disj_union`. -/
+theorem map_disj_union_aux {f : α ↪ β} {s₁ s₂ : finset α} :
+  (∀ a, a ∈ s₁ → a ∉ s₂) ↔ ∀ a, a ∈ map f s₁ → a ∉ map f s₂ :=
+by simp_rw [forall_mem_map, mem_map']
+
+theorem map_disj_union {f : α ↪ β} (s₁ s₂ : finset α) (h) (h' := map_disj_union_aux.1 h) :
+  (s₁.disj_union s₂ h).map f = (s₁.map f).disj_union (s₂.map f) h' :=
+eq_of_veq $ multiset.map_add _ _ _
+
+/-- A version of `finset.map_disj_union` for writing in the other direction. -/
+theorem map_disj_union' {f : α ↪ β} (s₁ s₂ : finset α) (h') (h := map_disj_union_aux.2 h') :
+  (s₁.disj_union s₂ h).map f = (s₁.map f).disj_union (s₂.map f) h' :=
+map_disj_union _ _ _
+
 theorem map_union [decidable_eq α] [decidable_eq β]
   {f : α ↪ β} (s₁ s₂ : finset α) : (s₁ ∪ s₂).map f = s₁.map f ∪ s₂.map f :=
 coe_injective $ by simp only [coe_map, coe_union, set.image_union]

src/data/finset/fold.lean

@@ -70,6 +70,10 @@ theorem fold_hom {op' : γ → γ → γ} [is_commutative γ op'] [is_associativ
   s.fold op' (m b) (λx, m (f x)) = m (s.fold op b f) :=
 by rw [fold, fold, ← fold_hom op hm, multiset.map_map]
 
+theorem fold_disj_union {s₁ s₂ : finset α} {b₁ b₂ : β} (h) :
+  (s₁.disj_union s₂ h).fold op (b₁ * b₂) f = s₁.fold op b₁ f * s₂.fold op b₂ f :=
+(congr_arg _ $ multiset.map_add _ _ _).trans (multiset.fold_add _ _ _ _ _)
+
 theorem fold_union_inter [decidable_eq α] {s₁ s₂ : finset α} {b₁ b₂ : β} :
   (s₁ ∪ s₂).fold op b₁ f * (s₁ ∩ s₂).fold op b₂ f = s₁.fold op b₂ f * s₂.fold op b₁ f :=
 by unfold fold; rw [← fold_add op, ← multiset.map_add, union_val,