mathlib

6a0801a6 - `finish` from `exists_subset_affine_independent_span_eq_top_of_open`