mathlib3

e6322c6a - feat(analysis/convex): golf some proofs (#13451)