case inl
α : Type ?u.838531
β : Type ?u.838534
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_1
f g : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ⊤
h✝ : IsEmpty ι
⊢ ENNReal.toNNReal (iInf f) = ⨅ (i : ι), ENNReal.toNNReal (f i)

case inr
α : Type ?u.838531
β : Type ?u.838534
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_1
f g : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ⊤
h✝ : Nonempty ι
⊢ ENNReal.toNNReal (iInf f) = ⨅ (i : ι), ENNReal.toNNReal (f i)
α : Type ?u.838531
β : Type ?u.838534
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_1
f g : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ⊤
⊢ ENNReal.toNNReal (iInf f) = ⨅ (i : ι), ENNReal.toNNReal (f i)
cases isEmpty_or_nonempty ι
no goals
case inl
α : Type ?u.838531
β : Type ?u.838534
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_1
f g : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ⊤
h✝ : IsEmpty ι
⊢ ENNReal.toNNReal (iInf f) = ⨅ (i : ι), ENNReal.toNNReal (f i)
rw [iInf_of_empty, top_toNNReal, NNReal.iInf_empty]
case inr.intro
α : Type ?u.838531
β : Type ?u.838534
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_1
g : ι → ℝ≥0∞
h✝ : Nonempty ι
f : ι → ℝ≥0
⊢ ENNReal.toNNReal (⨅ (i : ι), ↑(f i)) = ⨅ (i : ι), ENNReal.toNNReal ((fun i => ↑(f i)) i)
case inr
α : Type ?u.838531
β : Type ?u.838534
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_1
f g : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ⊤
h✝ : Nonempty ι
⊢ ENNReal.toNNReal (iInf f) = ⨅ (i : ι), ENNReal.toNNReal (f i)
lift f to ι → ℝ≥0 using hf
no goals
case inr.intro
α : Type ?u.838531
β : Type ?u.838534
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_1
g : ι → ℝ≥0∞
h✝ : Nonempty ι
f : ι → ℝ≥0
⊢ ENNReal.toNNReal (⨅ (i : ι), ↑(f i)) = ⨅ (i : ι), ENNReal.toNNReal ((fun i => ↑(f i)) i)
simp_rw [← coe_iInf, toNNReal_coe]