structure GLnBuilding.SimultaneousRefinementHyp (k : Type u_1) [Field k] (n : ℕ) : Prop

Hypothesis: any finite list of proper non-zero subspaces is simultaneously compatible with some frame $F$ — i.e.\ admits a common adapted basis.

• refine_list (subs : List (Submodule k (Vec k n))) : (∀ V ∈ subs, V ≠ ⊥ ∧ V ≠ ⊤) → ∃ (F : Frame k n), ∀ V ∈ subs, Frame.IsCompatible k n F V

noncomputable def GLnBuilding.commonApartmentHyp (k : Type u_1) [Field k] (n : ℕ) (h : SimultaneousRefinementHyp k n) : CommonApartmentHyp k n

From simultaneous refinement of arbitrary lists, deduce that any two flags lie in a common apartment: apply the hypothesis to $\sigma.\mathrm{chain} \mathbin{+\!\!+} \tau.\mathrm{chain}$.