Countable not right Lim Within ae eq

lemma countable_not_rightLimWithin_ae_eq [SecondCountableTopology ι] [IsFiniteMeasure μ]    (hX : IsRealQuasimartingale 𝓕 X μ)    {T : Set ι} (hTc : T.Countable) (hTd : Dense T) :    {t | ¬ (fun ω ↦ rightLimWithin (X · ω) T t) =ᵐ[μ] X t}.Countable := by  -- every dense set is cofinal  have hcof : ∀ T : Set ι, Dense T → ∀ x : ι, ∃ d ∈ T, x < d := fun T hTd x ↦ hTd.exists_gt x  -- the right-limit value along `T`, by choice  let R T' x ω : ℝ := Function.rightLimWithin (X · ω) T' x  have hRspec T' x ω (h : ∃ l, Tendsto (X · ω) (𝓝[T' ∩ Set.Ioi x] x) (𝓝 l)) :      Tendsto (X · ω) (𝓝[T' ∩ Set.Ioi x] x) (𝓝 (R T' x ω)) := by    rw [Set.inter_comm] at h ⊢    exact tendsto_rightLimWithin_of_tendsto h  -- Stage 1: a.e. one-sided limits along D₀  have hae₀ := ae_right_limit hX hTc (hcof T hTd)  -- Stage 2: measurable versions of `R D₀ x`  have hRm : ∀ x : ι, ∃ g : Ω → ℝ, Measurable g ∧ g =ᵐ[μ] R T x := by    intro x    have hne : (𝓝[T ∩ Set.Ioi x] x).NeBot := by      rw [Set.inter_comm]; exact nhdsWithin_Ioi_inter_neBot hTd x    obtain ⟨v, hv⟩ := exists_seq_tendsto (𝓝[T ∩ Set.Ioi x] x)    have haet : ∀ᵐ ω ∂μ, Tendsto (fun j ↦ X (v j) ω) atTop (𝓝 (R T x ω)) := by      filter_upwards [hae₀] with ω hω      exact (hRspec T x ω (hω x)).comp hv    obtain ⟨g, hgmeas, hgae⟩ := measurable_limit_of_tendsto_metrizable_ae      (f := fun j ↦ X (v j)) (L := atTop) (fun j ↦ (hX.measurable (v j)).aemeasurable)      (by filter_upwards [haet] with ω hω using ⟨_, hω⟩)    refine ⟨g, hgmeas, ?_⟩    filter_upwards [haet, hgae] with ω h1 h2    exact tendsto_nhds_unique h2 h1  choose Rm hRmMeas hRmae using hRm  -- Stage 3: the set of points where `R D₀ x` and `X x` disagree is countable  let Sset : Set ι := {x | ¬ R T x =ᵐ[μ] X x}  change Sset.Countable  by_contra hSunc  set Sn : ℕ → Set ι := fun n ↦    {x | ENNReal.ofReal (1 / (n + 1)) < μ {ω | 1 / (n + 1 : ℝ) < |Rm x ω - X x ω|}} with hSn  have hSsub : Sset ⊆ ⋃ n, Sn n := by    intro x hx    have hxm : ¬ Rm x =ᵐ[μ] X x := fun hcon ↦ hx ((hRmae x).symm.trans hcon)    have hpos : μ {ω | Rm x ω ≠ X x ω} ≠ 0 := hxm    have hBmono : Monotone (fun n : ℕ ↦ {ω | 1 / (n + 1 : ℝ) < |Rm x ω - X x ω|}) := by      intro n n' hnn' ω hω      simp only [Set.mem_ofPred_eq] at hω ⊢      refine lt_of_le_of_lt (one_div_le_one_div_of_le (by positivity) ?_) hω      have : (n : ℝ) ≤ (n' : ℝ) := mod_cast hnn'      gcongr    have hBunion : {ω | Rm x ω ≠ X x ω} = ⋃ n : ℕ, {ω | 1 / (n + 1 : ℝ) < |Rm x ω - X x ω|} := by      ext ω      simp only [Set.mem_ofPred_eq, Set.mem_iUnion]      constructor      · intro hne        have habs : 0 < |Rm x ω - X x ω| := abs_pos.2 (sub_ne_zero.2 hne)        exact exists_nat_one_div_lt habs      · rintro ⟨n, hn⟩ hcon        rw [hcon, sub_self, abs_zero] at hn        exact absurd hn (not_lt.2 (by positivity))    have hexn : ∃ n₀ : ℕ, 0 < μ {ω | 1 / ((n₀ : ℝ) + 1) < |Rm x ω - X x ω|} := by      by_contra! hcon      simp only [nonpos_iff_eq_zero] at hcon      refine hpos ?_      rw [hBunion]      refine le_antisymm ((measure_iUnion_le _).trans ?_) zero_le      simp only [hcon, tsum_zero, Std.le_refl]    obtain ⟨n₀, hn₀⟩ := hexn    have hfin : μ {ω | 1 / ((n₀ : ℝ) + 1) < |Rm x ω - X x ω|} ≠ ⊤ := measure_ne_top μ _    let ε : ℝ := (μ {ω | 1 / ((n₀ : ℝ) + 1) < |Rm x ω - X x ω|}).toReal    have hεpos : 0 < ε := ENNReal.toReal_pos hn₀.ne' hfin    obtain ⟨n₁, hn₁⟩ := exists_nat_one_div_lt hεpos    let n := max n₀ n₁    refine Set.mem_iUnion.2 ⟨n, ?_⟩    rw [hSn]    have hsub2 : {ω | 1 / ((n₀ : ℝ) + 1) < |Rm x ω - X x ω|}        ⊆ {ω | 1 / ((n : ℝ) + 1) < |Rm x ω - X x ω|} :=      hBmono (le_max_left n₀ n₁)    calc ENNReal.ofReal (1 / (n + 1))        ≤ ENNReal.ofReal (1 / (n₁ + 1)) := by          refine ENNReal.ofReal_le_ofReal (one_div_le_one_div_of_le (by positivity) ?_)          gcongr          exact mod_cast le_max_right n₀ n₁      _ < ENNReal.ofReal ε := ENNReal.ofReal_lt_ofReal_iff_of_nonneg (by positivity) |>.2 hn₁      _ = μ {ω | 1 / ((n₀ : ℝ) + 1) < |Rm x ω - X x ω|} := by rw [ENNReal.ofReal_toReal hfin]      _ ≤ μ {ω | 1 / ((n : ℝ) + 1) < |Rm x ω - X x ω|} := measure_mono hsub2  have hexSn : ∃ n, ¬ (Sn n).Countable := by    by_contra! hcon    exact hSunc ((Set.countable_iUnion hcon).mono hSsub)  obtain ⟨n, hSnunc⟩ := hexSn  obtain ⟨p, u, huSn, hup, hutend⟩ := exists_seq_gt_tendsto_of_not_countable hSnunc  set T' : Set ι := T ∪ (Set.range u ∪ {p}) with hT'  have hT'c : T'.Countable :=    hTc.union ((Set.countable_range u).union (Set.countable_singleton p))  have hT'd : Dense T' := hTd.mono Set.subset_union_left  have haediff : ∀ᵐ ω ∂μ, Tendsto (fun k ↦ Rm (u k) ω - X (u k) ω) atTop (𝓝 0) := by    have hcnt : ∀ᵐ ω ∂μ, ∀ k, Rm (u k) ω = R T (u k) ω := ae_all_iff.2 fun k ↦ hRmae (u k)    filter_upwards [hae₀, ae_right_limit hX hT'c (hcof T' hT'd), hcnt] with ω hω₀ hω' hkeq    have hL' := hRspec T' p ω (hω' p)    have hXu : Tendsto (fun k ↦ X (u k) ω) atTop (𝓝 (R T' p ω)) := by      refine hL'.comp ?_      rw [tendsto_nhdsWithin_iff]      exact ⟨hutend, Filter.Eventually.of_forall fun k ↦ by grind⟩    have hRu : Tendsto (fun k ↦ R T (u k) ω) atTop (𝓝 (R T' p ω)) :=      tendsto_rightLim_comp_of_gt hTd Set.subset_union_left        (fun y ↦ hRspec T y ω (hω₀ y)) hup hutend hL'    have hsub := hRu.sub hXu    rw [sub_self] at hsub    refine Tendsto.congr (fun k ↦ ?_) hsub    rw [hkeq k]  have htim : TendstoInMeasure μ (fun k ω ↦ Rm (u k) ω - X (u k) ω) atTop      (fun _ ↦ (0 : ℝ)) := by    refine tendstoInMeasure_of_tendsto_ae      (fun k ↦ ((hRmMeas (u k)).sub (hX.measurable (u k))).aestronglyMeasurable) ?_    filter_upwards [haediff] with ω hω using hω  have hcontra := htim (ENNReal.ofReal (1 / (n + 1 : ℝ)))    (by rw [ENNReal.ofReal_pos]; positivity)  have hev : ∀ᶠ k in atTop,      μ {ω | ENNReal.ofReal (1 / (n + 1 : ℝ)) ≤ edist (Rm (u k) ω - X (u k) ω) 0}        < ENNReal.ofReal (1 / (n + 1)) := by    refine hcontra.eventually_lt_const ?_    positivity  obtain ⟨k, hk⟩ := hev.exists  have hmem := huSn k  rw [hSn, Set.mem_ofPred_eq] at hmem  have hsub3 : {ω | 1 / (n + 1 : ℝ) < |Rm (u k) ω - X (u k) ω|}      ⊆ {ω | ENNReal.ofReal (1 / (n + 1 : ℝ)) ≤ edist (Rm (u k) ω - X (u k) ω) 0} := by    intro ω hω    rw [Set.mem_ofPred_eq] at hω ⊢    rw [edist_dist, dist_zero_right, Real.norm_eq_abs]    exact ENNReal.ofReal_le_ofReal hω.le  exact lt_irrefl _ ((hmem.trans_le (measure_mono hsub3)).trans hk)