case intro
α : Type ?u.840754
β : Type ?u.840757
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_1
g : ι → ℝ≥0∞
f : ι → ℝ≥0
⊢ ENNReal.toNNReal (⨆ (i : ι), ↑(f i)) = ⨆ (i : ι), ENNReal.toNNReal ((fun i => ↑(f i)) i)
α : Type ?u.840754
β : Type ?u.840757
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_1
f g : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ⊤
⊢ ENNReal.toNNReal (iSup f) = ⨆ (i : ι), ENNReal.toNNReal (f i)
lift f to ι → ℝ≥0 using hf
case intro
α : Type ?u.840754
β : Type ?u.840757
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_1
g : ι → ℝ≥0∞
f : ι → ℝ≥0
⊢ ENNReal.toNNReal (⨆ (i : ι), ↑(f i)) = ⨆ (i : ι), f i
case intro
α : Type ?u.840754
β : Type ?u.840757
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_1
g : ι → ℝ≥0∞
f : ι → ℝ≥0
⊢ ENNReal.toNNReal (⨆ (i : ι), ↑(f i)) = ⨆ (i : ι), ENNReal.toNNReal ((fun i => ↑(f i)) i)
simp_rw [toNNReal_coe]
case pos
α : Type ?u.840754
β : Type ?u.840757
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_1
g : ι → ℝ≥0∞
f : ι → ℝ≥0
h : BddAbove (range f)
⊢ ENNReal.toNNReal (⨆ (i : ι), ↑(f i)) = ⨆ (i : ι), f i

case neg
α : Type ?u.840754
β : Type ?u.840757
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_1
g : ι → ℝ≥0∞
f : ι → ℝ≥0
h : ¬BddAbove (range f)
⊢ ENNReal.toNNReal (⨆ (i : ι), ↑(f i)) = ⨆ (i : ι), f i
case intro
α : Type ?u.840754
β : Type ?u.840757
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_1
g : ι → ℝ≥0∞
f : ι → ℝ≥0
⊢ ENNReal.toNNReal (⨆ (i : ι), ↑(f i)) = ⨆ (i : ι), f i
by_cases h : BddAbove (range f)
no goals
case pos
α : Type ?u.840754
β : Type ?u.840757
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_1
g : ι → ℝ≥0∞
f : ι → ℝ≥0
h : BddAbove (range f)
⊢ ENNReal.toNNReal (⨆ (i : ι), ↑(f i)) = ⨆ (i : ι), f i
rw [← coe_iSup h, toNNReal_coe]
no goals
case neg
α : Type ?u.840754
β : Type ?u.840757
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_1
g : ι → ℝ≥0∞
f : ι → ℝ≥0
h : ¬BddAbove (range f)
⊢ ENNReal.toNNReal (⨆ (i : ι), ↑(f i)) = ⨆ (i : ι), f i
erw [NNReal.iSup_of_not_bddAbove h, (WithTop.iSup_coe_eq_top f).mpr h, top_toNNReal]