Note: some results should go to LinearAlgebra.Span.

theorem Submodule.sup_eq_span_union {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (s t : Submodule R M) : s ⊔ t = span R (↑s ∪ ↑t)

theorem LinearMap.injective_iff_of_direct_sum {R : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [Ring R] [Ring R₂] [AddCommGroup M] [AddCommGroup M₂] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {p q : Submodule R M} [RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (hpq : p ⊓ q = ⊥) (hpq' : p ⊔ q = ⊤) : Function.Injective ⇑f ↔ Disjoint p (ker f) ∧ Disjoint q (ker f) ∧ Disjoint (Submodule.map f p) (Submodule.map f q)