MeasureTheory.SimpleFunc.iSup_nnapprox_apply

lemma iSup_nnapprox_apply (hf : Measurable f) (a : α) : ⨆ n, (nnapprox f n : SimpleFunc α ℝ≥0) a = f a := by  apply le_antisymm  · apply ciSup_le    intro n    exact nnapprox_le hf  · apply le_of_not_gt    intro h    rcases (NNReal.lt_iff_exists_rat_btwn _ _).1 h with ⟨q, _, lt_q, q_lt⟩    have :      (Real.toNNReal q : ℝ≥0) ≤ ⨆ (k : ℕ) (_ : nnrealRatEmbed k ≤ f a), nnrealRatEmbed k := by      apply le_ciSup_of_le _ (Encodable.encode q)      · rw [← nnrealRatEmbed_encode q] at *        apply le_csSup_of_le        · rw [BddAbove]          use nnrealRatEmbed (Encodable.encode q)          rw [mem_upperBounds]          simp        use le_of_lt q_lt        simp      · use f a        rw [mem_upperBounds]        simp only [Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff]        intro n        exact ciSup_le' fun i ↦ i    rw [nnapprox, iSup_approx_apply' _ _ _ hf (by simp)] at lt_q    apply lt_irrefl _ (lt_of_le_of_lt this lt_q)