no goals
α : Type ?u.843793
β : Type ?u.843796
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_1
f g : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ⊤
⊢ ENNReal.toReal (iSup f) = ⨆ (i : ι), ENNReal.toReal (f i)
simp only [ENNReal.toReal, toNNReal_iSup hf, NNReal.coe_iSup]