diff --git a/Mathlib/Algebra/Module/Submodule/Map.lean b/Mathlib/Algebra/Module/Submodule/Map.lean
index 2e2f7d8ae98dc0..8ee3ab95cc8422 100644
--- a/Mathlib/Algebra/Module/Submodule/Map.lean
+++ b/Mathlib/Algebra/Module/Submodule/Map.lean
@@ -452,8 +452,7 @@ end OrderIso
 --TODO(Mario): is there a way to prove this from order properties?
 theorem map_inf_eq_map_inf_comap [RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂} {p : Submodule R M}
     {p' : Submodule R₂ M₂} : map f p ⊓ p' = map f (p ⊓ comap f p') :=
-  le_antisymm (by rintro _ ⟨⟨x, h₁, rfl⟩, h₂⟩; exact ⟨_, ⟨h₁, h₂⟩, rfl⟩)
-    (le_inf (map_mono inf_le_left) (map_le_iff_le_comap.2 inf_le_right))
+  .symm <| SetLike.coe_injective <| image_inter_preimage _ _ _
 
 @[simp]
 theorem map_comap_subtype : map p.subtype (comap p.subtype p') = p ⊓ p' :=
diff --git a/Mathlib/LinearAlgebra/Span/Basic.lean b/Mathlib/LinearAlgebra/Span/Basic.lean
index 2f16a8eb65657b..cd957fe7a6343d 100644
--- a/Mathlib/LinearAlgebra/Span/Basic.lean
+++ b/Mathlib/LinearAlgebra/Span/Basic.lean
@@ -561,6 +561,16 @@ theorem comap_map_sup_of_comap_le {f : M →ₛₗ[τ₁₂] M₂} {p : Submodul
   rw [add_comm, ← eq_sub_iff_add_eq, ← map_sub] at eq; subst eq
   simpa using p.add_mem (le hz) hy
 
+lemma disjoint_map_of_ker_le_right {f : M →ₛₗ[τ₁₂] M₂} {p q : Submodule R M}
+    (hpq : Disjoint p q) (hker : f.ker ≤ q) : Disjoint (p.map f) (q.map f) := by
+  rw [disjoint_iff, map_inf_eq_map_inf_comap, comap_map_eq, eq_bot_iff, map_le_iff_le_comap,
+    comap_bot, sup_eq_left.mpr hker, hpq.eq_bot]
+  exact bot_le
+
+lemma disjoint_map_of_ker_le_left {f : M →ₛₗ[τ₁₂] M₂} {p q : Submodule R M}
+    (hpq : Disjoint p q) (hker : f.ker ≤ p) : Disjoint (p.map f) (q.map f) :=
+  disjoint_map_of_ker_le_right hpq.symm hker |>.symm
+
 theorem isCoatom_comap_or_eq_top (f : M →ₛₗ[τ₁₂] M₂) {p : Submodule R₂ M₂} (hp : IsCoatom p) :
     IsCoatom (comap f p) ∨ comap f p = ⊤ :=
   or_iff_not_imp_right.mpr fun h ↦ ⟨h, fun q lt ↦ by