mathlib

cdc56baf - feat(analysis/calculus/tangent_cone): prove that all intervals are `unique_diff_on` (#2108)

feat(analysis/calculus/tangent_cone): prove that all intervals are `unique_diff_on` (#2108) * feat(analysis/calculus/tangent_cone): prove that all intervals are `unique_diff_on` * Drop some unneeded assumptions Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>