theorem Submodule.exists_equiv_fst_sndModFst {B : Type u_1} {F : Type u_2} {R : Type u_3} [DivisionRing R] [AddCommGroup B] [AddCommGroup F] [Module R B] [Module R F] (E : Submodule R (B × F)) : ∃ (B' : Submodule R B) (F' : Submodule R F) (f : ↥E ≃ₗ[R] ↥B' × ↥F') (φ : B →ₗ[R] F), (∀ (x : ↥E), ↑(f x).1 = (↑x).1 ∧ ↑(f x).2 = (↑x).2 - φ (↑x).1) ∧ ∀ (x₁ : ↥B') (x₂ : ↥F'), ↑(f.symm (x₁, x₂)) = (↑x₁, ↑x₂ + φ ↑x₁)

Given a submodule $E$ of $B\times F$, there is an equivalence $f:E\to B^{\prime }\times F^{\prime }$ given by the projections $E\to B$ and $E\to F$ "modulo" some $\phi :B\to F$.