mathlib3

223f6590 - chore(linear_algebra/basic): remove a duplicate proof, generalize map_span_le (#10219)