mathlib3

76c3f725 - chore(analysis/calculus/lhopital): use the new `nhds_within` notation (#17099)

chore(analysis/calculus/lhopital): use the new `nhds_within` notation (#17099) This slightly changes the definitional equality in the case of `univ \ {a}`, but the new spelling is easier to prove.