mathlib3

1a51c706 - feat(analysis/convex/cone): lemmas about `inner_dual_cone` of unions (#15836)

feat(analysis/convex/cone): lemmas about `inner_dual_cone` of unions (#15836) This discards the proof in #15639 and replaces it with a more general strategy and some auxiliary lemmas. This includes an `insert` lemma for consistency with `submodule.span_insert`, even though it follows trivially from the union lemma.