mathlib3

1263906f - chore(data/nat/pairing): add `pp_nodot`, fix some non-finalizing `simp`s (#8705)