MeasureTheory.continuousWithinAt_distribution

lemma continuousWithinAt_distribution (t₀ : ℝ≥0∞) :    ContinuousWithinAt (distribution f · μ) (Ioi t₀) t₀ := by  rcases (eq_top_or_lt_top t₀) with rfl | t₀nottop  · exact continuousWithinAt_of_notMem_closure (by simp)  · rcases (eq_top_or_lt_top (distribution f t₀ μ)) with db_top | db_not_top    -- Case: distribution f t₀ μ = ⊤    · simp only [ContinuousWithinAt, db_top, ENNReal.tendsto_nhds_top_iff_nnreal]      intro b      have h₀ : ∃ n : ℕ, ↑b < distribution f (t₀ + (↑n)⁻¹) μ :=        select_neighborhood_distribution _ _ (db_top ▸ coe_lt_top)      rcases h₀ with ⟨n, wn⟩      refine eventually_mem_set.mpr (mem_inf_iff_superset.mpr ⟨Iio (t₀ + (↑n)⁻¹), ?_, ?_⟩)      · exact Iio_mem_nhds (lt_add_right t₀nottop.ne_top (ENNReal.inv_ne_zero.mpr (by finiteness)))      · exact ⟨Ioi t₀, by simp, fun z h₁ ↦ wn.trans_le (distribution_mono_right (le_of_lt h₁.1))⟩    -- Case: distribution f t₀ μ < ⊤    · refine (ENNReal.tendsto_nhds db_not_top.ne_top).mpr fun ε ε_gt_0 ↦ ?_      refine        eventually_mem_set.mpr (mem_inf_iff_superset.mpr ?_)      rcases eq_zero_or_pos (distribution f t₀ μ) with db_zero | db_not_zero      -- Case: distribution f t₀ μ = 0      · use Ico 0 (t₀ + 1)        constructor        · refine IsOpen.mem_nhds isOpen_Ico_zero ?_          simp [lt_add_right t₀nottop.ne_top one_ne_zero]        · use Ioi t₀          refine ⟨by simp, fun z hz ↦ ?_⟩          rw [db_zero]          simp only [zero_le, tsub_eq_zero_of_le, zero_add]          have h₂ : distribution f z μ ≤ distribution f t₀ μ :=            distribution_mono_right (le_of_lt hz.2)          rw [db_zero] at h₂          change Icc 0 ε (distribution f z μ)          rw [nonpos_iff_eq_zero.mp h₂]          exact ⟨zero_le, zero_le⟩      -- Case: 0 < distribution f t₀ μ      · obtain ⟨n, wn⟩ :=          select_neighborhood_distribution t₀ _            (ENNReal.sub_lt_self db_not_top.ne_top db_not_zero.ne' ε_gt_0.ne')        use Iio (t₀ + (↑n)⁻¹)        constructor        · exact Iio_mem_nhds (lt_add_right t₀nottop.ne_top (ENNReal.inv_ne_zero.mpr (by finiteness)))        · refine ⟨Ioi t₀, by simp, fun z h ↦ ⟨?_, ?_⟩⟩          · calc              distribution f t₀ μ - ε                ≤ distribution f (t₀ + (↑n)⁻¹) μ := le_of_lt wn              _ ≤ distribution f z μ             := distribution_mono_right (le_of_lt h.1)          · calc              distribution f z μ                ≤ distribution f t₀ μ := distribution_mono_right (le_of_lt h.2)              _ ≤ distribution f t₀ μ + ε := le_self_add