mathlib3

af27ee33 - chore(analysis): two more -T50000 challenges (#2393)

chore(analysis): two more -T50000 challenges (#2393) Refactor two proofs to bring them under `-T50000`, in the hope that we can later add this requirement to CI, per #2276.