feat: Finsupp.mapRange of a surjective function is surjective (#17637)

From PFR

Author: YaelDillies

Mathlib/Data/Finsupp/Defs.lean

@@ -714,6 +714,10 @@ theorem mapRange_comp (f : N → P) (hf : f 0 = 0) (f₂ : M → N) (hf₂ : f
     (g : α →₀ M) : mapRange (f ∘ f₂) h g = mapRange f hf (mapRange f₂ hf₂ g) :=
   ext fun _ => rfl
 
+@[simp]
+lemma mapRange_mapRange (e₁ : N → P) (e₂ : M → N) (he₁ he₂) (f : α →₀ M) :
+    mapRange e₁ he₁ (mapRange e₂ he₂ f) = mapRange (e₁ ∘ e₂) (by simp [*]) f := ext fun _ ↦ rfl
+
 theorem support_mapRange {f : M → N} {hf : f 0 = 0} {g : α →₀ M} :
     (mapRange f hf g).support ⊆ g.support :=
   support_onFinset_subset
@@ -730,6 +734,14 @@ theorem support_mapRange_of_injective {e : M → N} (he0 : e 0 = 0) (f : ι →
   simp only [Finsupp.mem_support_iff, Ne, Finsupp.mapRange_apply]
   exact he.ne_iff' he0
 
+/-- `Finsupp.mapRange` of a surjective function is surjective. -/
+lemma mapRange_surjective (e : M → N) (he₀ : e 0 = 0) (he : Surjective e) :
+    Surjective (Finsupp.mapRange (α := α) e he₀) := by
+  classical
+  let d (n : N) : M := if n = 0 then 0 else surjInv he n
+  have : RightInverse d e := fun n ↦ by by_cases h : n = 0 <;> simp [d, h, he₀, surjInv_eq he n]
+  exact fun f ↦ ⟨mapRange d (by simp [d]) f, by simp [this.comp_eq_id]⟩
+
 end MapRange
 
 /-! ### Declarations about `embDomain` -/