feat(LinearAlgebra/Span/Defs): replace Submodule.exists_add_eq_of_codisjoint with an iff (#26796)

Instead of introducing another theorem to go the other way, I have upgraded this one to an iff. The changed order of terms is preferable in my application (and probably others) because to prove the existential it is enough to provide the two witnesses first and leave everything else to simp.

Author: agjftucker

Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean

@@ -288,7 +288,7 @@ lemma ker_restrict_eq_of_codisjoint {p q : Submodule R M} (hpq : Codisjoint p q)
   simp only [LinearMap.mem_ker, Submodule.mem_comap, Submodule.coe_subtype]
   refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
   · ext w
-    obtain ⟨x, hx, y, hy, rfl⟩ := Submodule.exists_add_eq_of_codisjoint hpq w
+    obtain ⟨x, y, hx, hy, rfl⟩ := Submodule.codisjoint_iff_exists_add_eq.mp hpq w
     simpa [hB z hz y hy] using LinearMap.congr_fun h ⟨x, hx⟩
   · ext ⟨x, hx⟩
     simpa using LinearMap.congr_fun h x

Mathlib/LinearAlgebra/PerfectPairing/Restrict.lean

@@ -54,8 +54,8 @@ private lemma restrict_aux : Bijective (p.toLinearMap.compl₁₂ i j) := by
   · set F : Module.Dual R N := f ∘ₗ j.linearProjOfIsCompl _ hj hij.isCompl_right with hF
     have hF (n : N') : F (j n) = f n := by simp [hF]
     set m : M := p.toDualLeft.symm F with hm
-    obtain ⟨-, ⟨m₀, rfl⟩, y, hy, hm'⟩ :=
-      Submodule.exists_add_eq_of_codisjoint hij.isCompl_left.codisjoint m
+    obtain ⟨-, y, ⟨m₀, rfl⟩, hy, hm'⟩ :=
+      Submodule.codisjoint_iff_exists_add_eq.mp hij.isCompl_left.codisjoint m
     refine ⟨m₀, LinearMap.ext fun n ↦ ?_⟩
     replace hy : (p y) (j n) = 0 := by
       simp only [Submodule.mem_map, Submodule.mem_dualAnnihilator] at hy

Mathlib/LinearAlgebra/Span/Defs.lean

@@ -349,10 +349,13 @@ theorem mem_sup : x ∈ p ⊔ p' ↔ ∃ y ∈ p, ∃ z ∈ p', y + z = x :=
 theorem mem_sup' : x ∈ p ⊔ p' ↔ ∃ (y : p) (z : p'), (y : M) + z = x :=
   mem_sup.trans <| by simp only [Subtype.exists, exists_prop]
 
-lemma exists_add_eq_of_codisjoint (h : Codisjoint p p') (x : M) :
-    ∃ y ∈ p, ∃ z ∈ p', y + z = x := by
-  suffices x ∈ p ⊔ p' by exact Submodule.mem_sup.mp this
-  simpa only [h.eq_top] using Submodule.mem_top
+theorem codisjoint_iff_exists_add_eq :
+    Codisjoint p p' ↔ ∀ z, ∃ x y, x ∈ p ∧ y ∈ p' ∧ x + y = z := by
+  rw [codisjoint_iff, eq_top_iff']
+  exact forall_congr' (fun z => mem_sup.trans <| by simp)
+
+@[deprecated (since := "2025-07-05")]
+alias ⟨exists_add_eq_of_codisjoint, _⟩ := codisjoint_iff_exists_add_eq
 
 variable (p p')