-- Mathlib/Data/ENNReal/Real.lean
@[simp] lemma ofReal_iInf [Nonempty ι] (f : ι → ℝ) :
    ENNReal.ofReal (⨅ i, f i) = ⨅ i, ENNReal.ofReal (f i)

Proof state:
case inr.inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ⊤
⊢ (∀ (i : ι), a.toReal ≤ f i) ↔ ∀ (i : ι), a ≤ ENNReal.ofReal (f i)

Tactic:
exact forall_congr' fun i ↦ (le_ofReal_iff_toReal_le ha (h _)).symm

Result:
no goals

Proof state:
case inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ¬∃ i, f i ≤ 0
⊢ ENNReal.ofReal (⨅ i, f i) = ⨅ i, ENNReal.ofReal (f i)

Tactic:
replace h i : 0 ≤ f i := le_of_not_le fun hi ↦ h ⟨i, hi⟩

Result:
case inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
⊢ ENNReal.ofReal (⨅ i, f i) = ⨅ i, ENNReal.ofReal (f i)

Proof state:
case inr.inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ⊤
⊢ 0 ≤ ⨅ i, f i

Tactic:
exact Real.iInf_nonneg h

Result:
no goals

Proof state:
case inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
⊢ ENNReal.ofReal (⨅ i, f i) = ⨅ i, ENNReal.ofReal (f i)

Tactic:
refine eq_of_forall_le_iff fun a ↦ ?_

Result:
case inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
⊢ a ≤ ENNReal.ofReal (⨅ i, f i) ↔ a ≤ ⨅ i, ENNReal.ofReal (f i)

Proof state:
case inr.inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ⊤
⊢ a ≤ ENNReal.ofReal (⨅ i, f i) ↔ a ≤ ⨅ i, ENNReal.ofReal (f i)

Tactic:
rw [le_iInf_iff, le_ofReal_iff_toReal_le ha, le_ciInf_iff ⟨0, by simpa [mem_lowerBounds]⟩]

Result:
case inr.inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ⊤
⊢ (∀ (i : ι), a.toReal ≤ f i) ↔ ∀ (i : ι), a ≤ ENNReal.ofReal (f i)

case inr.inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ⊤
⊢ 0 ≤ ⨅ i, f i

Proof state:
case inr.inl
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
⊢ ⊤ ≤ ENNReal.ofReal (⨅ i, f i) ↔ ⊤ ≤ ⨅ i, ENNReal.ofReal (f i)

Tactic:
simp

Result:
no goals

Proof state:
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
i : ι
hi : f i ≤ 0
x✝¹ : ℝ≥0∞
x✝ : x✝¹ > ⊥
⊢ ENNReal.ofReal (f i) < x✝¹

Tactic:
simpa [ofReal_of_nonpos hi]

Result:
no goals

Proof state:
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ⊤
⊢ 0 ∈ lowerBounds (range fun i => f i)

Tactic:
simpa [mem_lowerBounds]

Result:
no goals

Proof state:
case inl.intro
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
i : ι
hi : f i ≤ 0
⊢ ENNReal.ofReal (⨅ i, f i) = ⊥

Tactic:
simp [Real.iInf_nonpos' ⟨i, hi⟩]

Result:
no goals

Proof state:
case inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
⊢ a ≤ ENNReal.ofReal (⨅ i, f i) ↔ a ≤ ⨅ i, ENNReal.ofReal (f i)

Tactic:
obtain rfl | ha := eq_or_ne a ∞

Result:
case inr.inl
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
⊢ ⊤ ≤ ENNReal.ofReal (⨅ i, f i) ↔ ⊤ ≤ ⨅ i, ENNReal.ofReal (f i)

case inr.inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ⊤
⊢ a ≤ ENNReal.ofReal (⨅ i, f i) ↔ a ≤ ⨅ i, ENNReal.ofReal (f i)

Proof state:
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
⊢ ENNReal.ofReal (⨅ i, f i) = ⨅ i, ENNReal.ofReal (f i)

Tactic:
obtain ⟨i, hi⟩ | h := em (∃ i, f i ≤ 0)

Result:
case inl.intro
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
i : ι
hi : f i ≤ 0
⊢ ENNReal.ofReal (⨅ i, f i) = ⨅ i, ENNReal.ofReal (f i)

case inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ¬∃ i, f i ≤ 0
⊢ ENNReal.ofReal (⨅ i, f i) = ⨅ i, ENNReal.ofReal (f i)

Proof state:
case inl.intro
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
i : ι
hi : f i ≤ 0
⊢ ENNReal.ofReal (⨅ i, f i) = ⨅ i, ENNReal.ofReal (f i)

Tactic:
rw [(iInf_eq_bot _).2 fun _ _ ↦ ⟨i, by simpa [ofReal_of_nonpos hi]⟩]

Result:
case inl.intro
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
i : ι
hi : f i ≤ 0
⊢ ENNReal.ofReal (⨅ i, f i) = ⊥