diff --git a/Mathlib/Data/Finsupp/Antidiagonal.lean b/Mathlib/Data/Finsupp/Antidiagonal.lean
index 41fdc7fee17aab..be855b3c5530bd 100644
--- a/Mathlib/Data/Finsupp/Antidiagonal.lean
+++ b/Mathlib/Data/Finsupp/Antidiagonal.lean
@@ -89,4 +89,18 @@ 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
+  ext ⟨u, v⟩
+  simp only [mem_antidiagonal, mem_image, mem_product, Prod.mk.injEq, Prod.exists]
+  refine ⟨fun ⟨a, b, a', b', h1, h2, h3⟩ ↦ ?_, 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 ..⟩⟩
+  · rw [← h2, ← h3, ← sumElim_add, h1.left, h1.right]
+  · rw [← comapDomain_add_of_injective Sum.inl_injective, h, comapDomain_inl_sumElim]
+  · rw [← comapDomain_add_of_injective Sum.inr_injective, h, comapDomain_inr_sumElim]
+
 end Finsupp
diff --git a/Mathlib/Data/Finsupp/Basic.lean b/Mathlib/Data/Finsupp/Basic.lean
index 5a61c910e2c336..32d277098f2408 100644
--- a/Mathlib/Data/Finsupp/Basic.lean
+++ b/Mathlib/Data/Finsupp/Basic.lean
@@ -1045,6 +1045,37 @@ 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_inl_sumElim (f : α →₀ γ) (g : β →₀ γ) :
+    comapDomain Sum.inl (f.sumElim g) Sum.inl_injective.injOn = f := by
+  ext; simp
+
+@[simp]
+lemma comapDomain_inr_sumElim (f : α →₀ γ) (g : β →₀ γ) :
+    comapDomain Sum.inr (f.sumElim g) Sum.inr_injective.injOn = g := by
+  ext; simp
+
+@[simp]
+lemma embDomain_inl (a : α →₀ γ) :
+    embDomain Function.Embedding.inl a = sumElim a (0 : β →₀ γ) := by
+  ext (_ | _) <;> simp [embDomain_apply]
+
+@[simp]
+lemma embDomain_inr (b : β →₀ γ) :
+    embDomain Function.Embedding.inr b = sumElim (0 : α →₀ γ) b := by
+  ext (_ | _) <;> simp [embDomain_apply]
+
+@[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
+
+@[simp]
+lemma sumElim_add [AddZeroClass M] (a b : α →₀ M) (c d : β →₀ M) :
+    (a + b).sumElim (c + d) = a.sumElim c + b.sumElim d := by
+  ext (_ | _) <;> simp
+
 /-- The equivalence between `(α ⊕ β) →₀ γ` and `(α →₀ γ) × (β →₀ γ)`.
 
 This is the `Finsupp` version of `Equiv.sum_arrow_equiv_prod_arrow`. -/
diff --git a/Mathlib/Data/Finsupp/Option.lean b/Mathlib/Data/Finsupp/Option.lean
index e5952a6a4d3099..346d28f45ac970 100644
--- a/Mathlib/Data/Finsupp/Option.lean
+++ b/Mathlib/Data/Finsupp/Option.lean
@@ -211,6 +211,11 @@ 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 _ _ _
 
+@[simp]
+lemma optionElim_add [AddZeroClass M] (a b : α →₀ M) (i j : M) :
+    (a + b).optionElim (i + j) = a.optionElim i + b.optionElim j := by
+  ext x; cases x <;> simp
+
 end Option
 
 end Finsupp