MeasureTheory.truncCut_sup

lemma truncCut_sup {μ : Measure α} [SigmaFinite μ] {f : α → ℝ≥0∞} (x : α) :    ⨆ n : ℕ, truncCut f μ n x = f x := by  refine iSup_eq_of_forall_le_of_forall_lt_exists_gt ?h₁ ?h₂  · intro n; unfold truncCut indicator    split_ifs    · exact min_le_left (f x) ↑n    · exact zero_le  · intro w hw    have : ∃ m : ℕ, x ∈ spanningSets μ m := by      have obs := iUnion_spanningSets μ      refine mem_iUnion.mp ?_      rw [obs]      exact trivial    rcases this with ⟨m, wm⟩    rcases ENNReal.exists_nat_gt hw.ne_top with ⟨n, wn⟩    use (m + n)    simp only [truncCut, indicator]    split_ifs with is_x_in_Ampn    · refine lt_min hw ?_      calc      w < n := wn      _ ≤ m + n := le_add_self      _ = _ := (Nat.cast_add m n).symm    · contrapose! is_x_in_Ampn      exact monotone_spanningSets _ (by simp) wm