chore: cleanup API around LinearMap.surjective_domRestrict_iff (leanprover-community#41235)

- semilinearize [LinearMap.range_domRestrict](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Module/Submodule/Range.html#LinearMap.range_domRestrict)
- add `map_eq_range_iff` as a replacement for [LinearMap.range_domRestrict_eq_range_iff](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Span/Basic.html#LinearMap.range_domRestrict_eq_range_iff), with a golfed proof.
- use `Codisjoint` in [LinearMap.surjective_domRestrict_iff](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Span/Basic.html#LinearMap.surjective_domRestrict_iff)

Author: ADedecker

Mathlib/Algebra/Module/Submodule/Range.lean

@@ -114,7 +114,7 @@ theorem range_neg {R : Type*} {R₂ : Type*} {M : Type*} {M₂ : Type*} [Semirin
   change range ((-LinearMap.id : M₂ →ₗ[R₂] M₂).comp f) = _
   rw [range_comp, Submodule.map_neg, Submodule.map_id]
 
-@[simp] lemma range_domRestrict [Module R M₂] (K : Submodule R M) (f : M →ₗ[R] M₂) :
+@[simp] lemma range_domRestrict [RingHomSurjective τ₁₂] (K : Submodule R M) (f : M →ₛₗ[τ₁₂] M₂) :
     range (domRestrict f K) = K.map f := by ext; simp
 
 lemma range_domRestrict_le_range [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) (S : Submodule R M) :
@@ -303,6 +303,7 @@ open LinearMap
 @[simp]
 theorem map_top [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) : map f ⊤ = range f :=
   (range_eq_map f).symm
+
 @[simp]
 theorem range_subtype : range p.subtype = p := by simpa using map_comap_subtype p ⊤
 

Mathlib/LinearAlgebra/Span/Basic.lean

@@ -529,6 +529,8 @@ end AddCommGroup
 
 section AddCommGroup
 
+-- TODO: Multiple lemmas in this section should be in earlier files
+
 variable [Semiring R] [Semiring R₂]
 variable [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂]
 variable {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂]
@@ -539,6 +541,11 @@ theorem comap_map_eq (f : M →ₛₗ[τ₁₂] M₂) (p : Submodule R M) :
   rintro x ⟨y, hy, e⟩
   exact mem_sup.2 ⟨y, hy, x - y, by simpa using sub_eq_zero.2 e.symm, by simp⟩
 
+theorem map_eq_range_iff {f : M →ₛₗ[τ₁₂] M₂} {p : Submodule R M} :
+    map f p = f.range ↔ Codisjoint p f.ker := by
+  simp_rw [le_antisymm_iff, LinearMap.map_le_range, true_and, ← map_top, map_le_iff_le_comap,
+    comap_map_eq, codisjoint_iff_le_sup]
+
 theorem map_lt_map_of_le_of_sup_lt_sup {p p' : Submodule R M} {f : M →ₛₗ[τ₁₂] M₂} (hab : p ≤ p')
     (h : p ⊔ LinearMap.ker f < p' ⊔ LinearMap.ker f) : Submodule.map f p < Submodule.map f p' := by
   simp_rw [← comap_map_eq] at h
@@ -587,28 +594,16 @@ lemma comap_covBy_of_surjective {f : M →ₛₗ[τ₁₂] M₂} (hf : Surjectiv
   rwa [← comap_lt_comap_iff_of_surjective hf, comap_map_eq, sup_eq_left.mpr]
   refine (LinearMap.ker_le_comap (f : M →ₛₗ[τ₁₂] M₂)).trans h₁.le
 
+@[deprecated map_eq_range_iff (since := "2026-07-01")]
 lemma _root_.LinearMap.range_domRestrict_eq_range_iff {f : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M} :
-    LinearMap.range (f.domRestrict S) = LinearMap.range f ↔ S ⊔ (LinearMap.ker f) = ⊤ := by
-  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-  · rw [eq_top_iff]
-    intro x _
-    have : f x ∈ LinearMap.range f := LinearMap.mem_range_self f x
-    rw [← h] at this
-    obtain ⟨y, hy⟩ : ∃ y : S, f.domRestrict S y = f x := this
-    have : (y : M) + (x - y) ∈ S ⊔ (LinearMap.ker f) := Submodule.add_mem_sup y.2 (by simp [← hy])
-    simpa using this
-  · refine le_antisymm (LinearMap.range_domRestrict_le_range f S) ?_
-    rintro x ⟨y, rfl⟩
-    obtain ⟨s, hs, t, ht, rfl⟩ : ∃ s, s ∈ S ∧ ∃ t, t ∈ LinearMap.ker f ∧ s + t = y :=
-      Submodule.mem_sup.1 (by simp [h])
-    exact ⟨⟨s, hs⟩, by simp [LinearMap.mem_ker.1 ht]⟩
+    LinearMap.range (f.domRestrict S) = LinearMap.range f ↔ Codisjoint S f.ker := by
+  simp [map_eq_range_iff]
 
 @[simp] lemma _root_.LinearMap.surjective_domRestrict_iff
     {f : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M} (hf : Surjective f) :
-    Surjective (f.domRestrict S) ↔ S ⊔ LinearMap.ker f = ⊤ := by
+    Surjective (f.domRestrict S) ↔ Codisjoint S f.ker := by
   rw [← LinearMap.range_eq_top] at hf ⊢
-  rw [← hf]
-  exact LinearMap.range_domRestrict_eq_range_iff
+  rw [← hf, LinearMap.range_domRestrict, map_eq_range_iff]
 
 lemma biSup_comap_eq_top_of_surjective {ι : Type*} (s : Set ι) (hs : s.Nonempty)
     (p : ι → Submodule R₂ M₂) (hp : ⨆ i ∈ s, p i = ⊤)

Mathlib/MeasureTheory/Measure/Haar/Disintegration.lean

@@ -64,7 +64,7 @@ theorem LinearMap.exists_map_addHaar_eq_smul_addHaar' (h : Function.Surjective L
   have P_cont : Continuous P := LinearMap.continuous_of_finiteDimensional _
   have I : Function.Bijective (LinearMap.domRestrict L T) :=
     ⟨LinearMap.injective_domRestrict_iff.2 (IsCompl.inf_eq_bot hT.symm),
-    (LinearMap.surjective_domRestrict_iff h).2 hT.symm.sup_eq_top⟩
+    (LinearMap.surjective_domRestrict_iff h).2 hT.symm.codisjoint⟩
   let L' : T ≃ₗ[𝕜] F := LinearEquiv.ofBijective (LinearMap.domRestrict L T) I
   have L'_cont : Continuous L' := LinearMap.continuous_of_finiteDimensional _
   have A : L = (L' : T →ₗ[𝕜] F).comp (P.comp (M.symm : E →ₗ[𝕜] (S × T))) := by