mathlib

c59720b4 - chore(analysis/convex/cone): add trivial coercion lemmas (#15713)

chore(analysis/convex/cone): add trivial coercion lemmas (#15713) This also changes `le` to unfold in terms of `coe` rather than `carrier`, since that's the form we have lemmas about.