no goals
α : Type ?u.843276
β : Type ?u.843279
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort ?u.843296
f g : ι → ℝ≥0∞
s : Set ℝ≥0∞
hf : ∀ (r : ℝ≥0∞), r ∈ s → r ≠ ⊤
⊢ ENNReal.toReal (sInf s) = sInf (ENNReal.toReal '' s)
simp only [ENNReal.toReal, toNNReal_sInf s hf, NNReal.coe_sInf, Set.image_image]