ContinuousWithinAt.measure_lt_ne_zero

lemma ContinuousWithinAt.measure_lt_ne_zero {α : Type*} {m : MeasurableSpace α} {μ : Measure α}    [TopologicalSpace α] [LinearOrder α] [DenselyOrdered α]    [OrderTopology α] [ClosedIicTopology α] [μ.IsOpenPosMeasure] {f : α → ℝ≥0∞} {x : α}    (hx : ¬IsMax x) (hf : ContinuousWithinAt f (Set.Ioi x) x)    {a : ℝ≥0∞} (ha : a < f x) :    μ {y | a < f y} ≠ 0 := by  unfold ContinuousWithinAt at hf  set s := Set.Ioi a  have := hf (isOpen_Ioi.mem_nhds (by simpa))  simp only [Filter.mem_map] at this  rw [← ENNReal.bot_eq_zero, ← bot_lt_iff_ne_bot]  obtain ⟨u, u_open, x_in_u, u_inter_subset⟩ := mem_nhdsWithin.mp this  calc _    _ < μ (u ∩ Set.Ioi x) := by      rw [bot_lt_iff_ne_bot]      apply (u_open.inter isOpen_Ioi).measure_ne_zero _      exact nonempty_nhds_inter_Ioi (u_open.mem_nhds x_in_u) hx    _ ≤ μ (f ⁻¹' s) := by      apply measure_mono u_inter_subset    _ ≤ μ {y | a < f y} := by      apply measure_mono      unfold s Set.preimage      simp only [Set.mem_Ioi, Set.setOf_subset_setOf]      intro y h      exact h