refactor(MeasureTheory): golf Mathlib/MeasureTheory/Function/Egorov (leanprover-community#38884)

- shortens `tendstoUniformlyOn_diff_iUnionNotConvergentSeq` by extracting the needed distance bound from `hx` with a single `not_lt.mp` argument, instead of unpacking `hx` via a long `simp`/`push Not` chain

Extracted from leanprover-community#38104

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

Author: yuanyi-350

Mathlib/MeasureTheory/Function/Egorov.lean

@@ -168,14 +168,10 @@ theorem tendstoUniformlyOn_diff_iUnionNotConvergentSeq (hε : 0 < ε)
   obtain ⟨N, hN⟩ := ENNReal.exists_inv_nat_lt hδ.ne'
   rw [eventually_atTop]
   refine ⟨Egorov.notConvergentSeqLTIndex (half_pos hε) hf hsm hs hfg N, fun n hn x hx => ?_⟩
-  simp only [Set.mem_diff, Egorov.iUnionNotConvergentSeq, not_exists, Set.mem_iUnion,
-    Set.mem_inter_iff, not_and, exists_and_left] at hx
-  obtain ⟨hxs, hx⟩ := hx
-  specialize hx hxs N
-  rw [Egorov.mem_notConvergentSeq_iff] at hx
-  push Not at hx
-  rw [edist_comm]
-  exact lt_of_le_of_lt (hx n hn) hN
+  refine lt_of_le_of_lt ?_ hN
+  have : edist (f n x) (g x) ≤ (N : ℝ≥0∞)⁻¹ :=
+    not_lt.mp fun h ↦ hx.2 <| Set.mem_iUnion.2 ⟨N, hx.1, mem_notConvergentSeq_iff.2 ⟨n, hn, h⟩⟩
+  simpa [edist_comm]
 
 end Egorov