mathlib3

5585e3cb - chore(linear_algebra/basic): redefine le on submodule (#2766)

chore(linear_algebra/basic): redefine le on submodule (#2766) Previously, to prove an `S \le T`, there would be a coercion in the statement after `intro x`. This fixes that.