ENNReal.coe_biSup

lemma coe_biSup {f : ι → ℝ≥0} (hf : BddAbove (range f)) :    ⨆ x ∈ s, f x = ⨆ x ∈ s, (f x : ℝ≥0∞) := by  simp_rw [bddAbove_def, mem_range, forall_exists_index, forall_apply_eq_imp_iff] at hf  rw [ENNReal.coe_iSup]  · congr with x    rw [ENNReal.coe_iSup]    apply IsBounded.bddAbove    simp only [Metric.isBounded_iff, mem_range, exists_prop, and_imp, forall_apply_eq_imp_iff,      dist_self, forall_self_imp]    aesop  · simp_rw [bddAbove_def, mem_range, forall_exists_index, forall_apply_eq_imp_iff]    obtain ⟨K, hK⟩ := hf    exact ⟨K, fun c ↦ ciSup_le' fun _ ↦ hK c⟩