Golfing an `ENNReal` coercion push lemma

Stream: mathlib4

[Jeremy Tan]

While working on Carleson I had to prove the following lemma:

import Mathlib.Topology.Instances.NNReal.Defs

open Set

lemma ENNReal.coe_iSup_NNReal {X : Type*} {s : Set X} {f : X → NNReal}
    (hf : Bornology.IsBounded (range f)) :
    ENNReal.ofNNReal (⨆ x ∈ s, f x) = ⨆ x ∈ s, ENNReal.ofNNReal (f x) := by
  rw [ENNReal.coe_iSup]
  · congr with x; rw [ENNReal.coe_iSup]
    apply Bornology.IsBounded.bddAbove
    simp_rw [Metric.isBounded_iff, mem_range, exists_prop, and_imp, forall_apply_eq_imp_iff,
      dist_self, forall_self_imp]
    use 0; simp
  · simp_rw [bddAbove_def, mem_range, forall_exists_index, forall_apply_eq_imp_iff]
    suffices ∃ x, ∀ a, f a ≤ x by
      obtain ⟨K, hK⟩ := this; use K; intro c
      exact ciSup_le' fun _ ↦ hK c
    replace hf := (isBounded_iff_bddBelow_bddAbove.mp hf).2
    rw [bddAbove_def] at hf; simpa using hf

Can this be proved in a more straightforward manner?