Two submodules meeting in zero inside a third

Mathlib's Submodule.finrank_add_finrank_le_of_disjoint bounds the dimensions of two disjoint submodules by the dimension of the ambient module. TauCeti.finrank_add_finrank_le_of_inf_eq_bot is the relative form: the bound holds inside any submodule containing them both, which is what a counting argument that produces its two subspaces inside a third one needs.

theorem TauCeti.finrank_add_finrank_le_of_inf_eq_bot {K : Type u_1} {W : Type u_2} [DivisionRing K] [AddCommGroup W] [Module K W] [FiniteDimensional K W] {S T U : Submodule K W} (hS : S ≤ U) (hT : T ≤ U) (h : S ⊓ T = ⊥) : Module.finrank K ↥S + Module.finrank K ↥T ≤ Module.finrank K ↥U

Two submodules meeting only in 0 have dimensions adding to at most that of any submodule containing them both.