[Merged by Bors] - feat(Data/Finsupp): add lemmas for Finsupp and Sum

Mathlib/Data/Finsupp/Antidiagonal.lean

@@ -89,4 +89,19 @@ theorem image_prodMap_embDomain_antidiagonal {β : Type*} [DecidableEq β] (f :
   · rw [embDomain_comapDomain ((mem_range_embDomain_iff ..).mp
       (isLowerSet_range_embDomain f (le_iff_exists_add'.mpr ⟨u, h.symm⟩) (by simp)))]
 
+open Finset in
+theorem image_sumElim_product_antidiagonal {β : Type*} [DecidableEq β]
+    {x : α →₀ ℕ} {y : β →₀ ℕ} : image (fun ((x, y), z, w) ↦
+      (x.sumElim z, y.sumElim w)) (antidiagonal x ×ˢ antidiagonal y) =
+    antidiagonal (x.sumElim y) := by
+  symm; ext ⟨u, v⟩
+  simp only [mem_antidiagonal, mem_image, mem_product, Prod.mk.injEq, Prod.exists]
+  refine ⟨fun h ↦ ⟨u.comapDomain Sum.inl Sum.inl_injective.injOn,
+    v.comapDomain Sum.inl Sum.inl_injective.injOn, u.comapDomain Sum.inr Sum.inr_injective.injOn,
+    v.comapDomain Sum.inr Sum.inr_injective.injOn, ⟨?_, ?_⟩, comapDomain_sumElim_comapDomain ..,
+    comapDomain_sumElim_comapDomain ..⟩, fun ⟨a, b, a', b', h1, h2, h3⟩ ↦ ?_⟩
+  · rw [← comapDomain_add_of_injective Sum.inl_injective, h, comapDomain_sumInl_sumElim]
+  · rw [← comapDomain_add_of_injective Sum.inr_injective, h, comapDomain_sumInr_sumElim]
+  rw [← h2, ← h3, sumElim_add, h1.left, h1.right]
+
 end Finsupp

Mathlib/Data/Finsupp/Basic.lean

@@ -1041,6 +1041,40 @@ lemma prod_sumElim {ι₁ ι₂ α M : Type*} [Zero α] [CommMonoid M]
     (f₁.sumElim f₂).prod g = f₁.prod (g ∘ Sum.inl) * f₂.prod (g ∘ Sum.inr) := by
   simp [Finsupp.prod, Finset.prod_disjSum]
 
+@[simp]
+lemma comapDomain_sumInl_sumElim (f : α →₀ γ) (g : β →₀ γ) :
+    comapDomain Sum.inl (f.sumElim g) Sum.inl_injective.injOn = f := by
+  ext; simp
+
+@[simp]
+lemma comapDomain_sumInr_sumElim (f : α →₀ γ) (g : β →₀ γ) :
+    comapDomain Sum.inr (f.sumElim g) Sum.inr_injective.injOn = g := by
+  ext; simp
+
+@[simp]
+lemma embDomain_embeddingInr (b : β →₀ γ) :
+    embDomain Function.Embedding.inr b = sumElim (0 : α →₀ γ) b := by
+  ext (_ | _)
+  · simp [embDomain_notin_range]
+  · rw [coe_sumElim, coe_zero, Sum.elim_inr, ← Function.Embedding.inr_apply, embDomain_apply_self]
+
+@[simp]
+lemma embDomain_embeddingInl (a : α →₀ γ) :
+    embDomain Function.Embedding.inl a = sumElim a (0 : β →₀ γ) := by
+  ext (_ | _)
+  · rw [coe_sumElim, coe_zero, Sum.elim_inl, ← Function.Embedding.inl_apply, embDomain_apply_self]
+  · simp [embDomain_notin_range]
+
+@[simp]
+lemma comapDomain_sumElim_comapDomain (c : α ⊕ β →₀ γ) :
+    (comapDomain Sum.inl c Sum.inl_injective.injOn).sumElim
+      (comapDomain Sum.inr c Sum.inr_injective.injOn) = c := by
+  ext (_ | _) <;> simp
+
+lemma sumElim_add [AddZeroClass M] (a b : α →₀ M) (c d : β →₀ M) :
+    a.sumElim c + b.sumElim d = (a + b).sumElim (c + d) := by
+  ext (_ | _) <;> simp
+
 /-- The equivalence between `(α ⊕ β) →₀ γ` and `(α →₀ γ) × (β →₀ γ)`.
 
 This is the `Finsupp` version of `Equiv.sum_arrow_equiv_prod_arrow`. -/

Mathlib/Data/Finsupp/Option.lean

@@ -211,6 +211,10 @@ theorem sum_option_index_smul [Semiring R] [AddCommMonoid M] [Module R M] (f : O
     (f.sum fun o r => r • b o) = f none • b none + f.some.sum fun a r => r • b (Option.some a) :=
   f.sum_option_index _ (fun _ => zero_smul _ _) fun _ _ _ => add_smul _ _ _
 
+lemma optionElim_add [AddZeroClass M] (a b : α →₀ M) (i j : M) :
+    a.optionElim i + b.optionElim j = (a + b).optionElim (i + j) := by
+  ext x; cases x <;> simp
+
 end Option
 
 end Finsupp