mathlib3

7d754e06 - chore(analysis/calculus/mean_value): use `nnnorm` in a few lemmas (#8348)

chore(analysis/calculus/mean_value): use `nnnorm` in a few lemmas (#8348) Use `nnnorm` instead of `norm` and `C : nnreal` in lemmas about `lipschitz_on_with`. This way we can use them to prove any statement of the form `lipschitz_on_with C f s`, not only something of the form `lipschitz_on_with (real.to_nnreal C) f s`.