case pos
α : Type ?u.115719
β : Type ?u.115722
γ : Type ?u.115725
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
h : a = ⊤ → (⨅ (i : ι), f i) = 0 → ∃ i, f i = 0
h0 : a = 0 → Nonempty ι
H : a = ⊤ ∧ (⨅ (i : ι), f i) = 0
⊢ (⨅ (i : ι), a * f i) = a * ⨅ (i : ι), f i

case neg
α : Type ?u.115719
β : Type ?u.115722
γ : Type ?u.115725
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
h : a = ⊤ → (⨅ (i : ι), f i) = 0 → ∃ i, f i = 0
h0 : a = 0 → Nonempty ι
H : ¬(a = ⊤ ∧ (⨅ (i : ι), f i) = 0)
⊢ (⨅ (i : ι), a * f i) = a * ⨅ (i : ι), f i
α : Type ?u.115719
β : Type ?u.115722
γ : Type ?u.115725
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
h : a = ⊤ → (⨅ (i : ι), f i) = 0 → ∃ i, f i = 0
h0 : a = 0 → Nonempty ι
⊢ (⨅ (i : ι), a * f i) = a * ⨅ (i : ι), f i
by_cases H : a = ⊤ ∧ (⨅ i, f i) = 0
case pos.intro
α : Type ?u.115719
β : Type ?u.115722
γ : Type ?u.115725
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
h : a = ⊤ → (⨅ (i : ι), f i) = 0 → ∃ i, f i = 0
h0 : a = 0 → Nonempty ι
H : a = ⊤ ∧ (⨅ (i : ι), f i) = 0
i : ι
hi : f i = 0
⊢ (⨅ (i : ι), a * f i) = a * ⨅ (i : ι), f i
case pos
α : Type ?u.115719
β : Type ?u.115722
γ : Type ?u.115725
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
h : a = ⊤ → (⨅ (i : ι), f i) = 0 → ∃ i, f i = 0
h0 : a = 0 → Nonempty ι
H : a = ⊤ ∧ (⨅ (i : ι), f i) = 0
⊢ (⨅ (i : ι), a * f i) = a * ⨅ (i : ι), f i
rcases h H.1 H.2 with ⟨i, hi⟩
case pos.intro
α : Type ?u.115719
β : Type ?u.115722
γ : Type ?u.115725
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
h : a = ⊤ → (⨅ (i : ι), f i) = 0 → ∃ i, f i = 0
h0 : a = 0 → Nonempty ι
H : a = ⊤ ∧ (⨅ (i : ι), f i) = 0
i : ι
hi : f i = 0
⊢ ∀ (b : ℝ≥0∞), b > ⊥ → ∃ i, a * f i < b
case pos.intro
α : Type ?u.115719
β : Type ?u.115722
γ : Type ?u.115725
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
h : a = ⊤ → (⨅ (i : ι), f i) = 0 → ∃ i, f i = 0
h0 : a = 0 → Nonempty ι
H : a = ⊤ ∧ (⨅ (i : ι), f i) = 0
i : ι
hi : f i = 0
⊢ (⨅ (i : ι), a * f i) = a * ⨅ (i : ι), f i
rw [H.2, mul_zero, ← bot_eq_zero, iInf_eq_bot]
no goals
case pos.intro
α : Type ?u.115719
β : Type ?u.115722
γ : Type ?u.115725
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
h : a = ⊤ → (⨅ (i : ι), f i) = 0 → ∃ i, f i = 0
h0 : a = 0 → Nonempty ι
H : a = ⊤ ∧ (⨅ (i : ι), f i) = 0
i : ι
hi : f i = 0
⊢ ∀ (b : ℝ≥0∞), b > ⊥ → ∃ i, a * f i < b
exact fun b hb => ⟨i, by rwa [hi, mul_zero, ← bot_eq_zero]⟩
no goals
α : Type ?u.115719
β : Type ?u.115722
γ : Type ?u.115725
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
h : a = ⊤ → (⨅ (i : ι), f i) = 0 → ∃ i, f i = 0
h0 : a = 0 → Nonempty ι
H : a = ⊤ ∧ (⨅ (i : ι), f i) = 0
i : ι
hi : f i = 0
b : ℝ≥0∞
hb : b > ⊥
⊢ a * f i < b
rwa [hi, mul_zero, ← bot_eq_zero]
case neg
α : Type ?u.115719
β : Type ?u.115722
γ : Type ?u.115725
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
h : a = ⊤ → (⨅ (i : ι), f i) = 0 → ∃ i, f i = 0
h0 : a = 0 → Nonempty ι
H : ¬a = ⊤ ∨ ¬(⨅ (i : ι), f i) = 0
⊢ (⨅ (i : ι), a * f i) = a * ⨅ (i : ι), f i
case neg
α : Type ?u.115719
β : Type ?u.115722
γ : Type ?u.115725
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
h : a = ⊤ → (⨅ (i : ι), f i) = 0 → ∃ i, f i = 0
h0 : a = 0 → Nonempty ι
H : ¬(a = ⊤ ∧ (⨅ (i : ι), f i) = 0)
⊢ (⨅ (i : ι), a * f i) = a * ⨅ (i : ι), f i
rw [not_and_or] at H
case neg.inl
α : Type ?u.115719
β : Type ?u.115722
γ : Type ?u.115725
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
h : a = ⊤ → (⨅ (i : ι), f i) = 0 → ∃ i, f i = 0
h0 : a = 0 → Nonempty ι
H : ¬a = ⊤ ∨ ¬(⨅ (i : ι), f i) = 0
h✝ : IsEmpty ι
⊢ (⨅ (i : ι), a * f i) = a * ⨅ (i : ι), f i

case neg.inr
α : Type ?u.115719
β : Type ?u.115722
γ : Type ?u.115725
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
h : a = ⊤ → (⨅ (i : ι), f i) = 0 → ∃ i, f i = 0
h0 : a = 0 → Nonempty ι
H : ¬a = ⊤ ∨ ¬(⨅ (i : ι), f i) = 0
h✝ : Nonempty ι
⊢ (⨅ (i : ι), a * f i) = a * ⨅ (i : ι), f i
case neg
α : Type ?u.115719
β : Type ?u.115722
γ : Type ?u.115725
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
h : a = ⊤ → (⨅ (i : ι), f i) = 0 → ∃ i, f i = 0
h0 : a = 0 → Nonempty ι
H : ¬a = ⊤ ∨ ¬(⨅ (i : ι), f i) = 0
⊢ (⨅ (i : ι), a * f i) = a * ⨅ (i : ι), f i
cases isEmpty_or_nonempty ι
case neg.inl
α : Type ?u.115719
β : Type ?u.115722
γ : Type ?u.115725
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
h : a = ⊤ → (⨅ (i : ι), f i) = 0 → ∃ i, f i = 0
h0 : a = 0 → Nonempty ι
H : ¬a = ⊤ ∨ ¬(⨅ (i : ι), f i) = 0
h✝ : IsEmpty ι
⊢ a ≠ 0
case neg.inl
α : Type ?u.115719
β : Type ?u.115722
γ : Type ?u.115725
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
h : a = ⊤ → (⨅ (i : ι), f i) = 0 → ∃ i, f i = 0
h0 : a = 0 → Nonempty ι
H : ¬a = ⊤ ∨ ¬(⨅ (i : ι), f i) = 0
h✝ : IsEmpty ι
⊢ (⨅ (i : ι), a * f i) = a * ⨅ (i : ι), f i
rw [iInf_of_empty, iInf_of_empty, mul_top]
no goals
case neg.inl
α : Type ?u.115719
β : Type ?u.115722
γ : Type ?u.115725
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
h : a = ⊤ → (⨅ (i : ι), f i) = 0 → ∃ i, f i = 0
h0 : a = 0 → Nonempty ι
H : ¬a = ⊤ ∨ ¬(⨅ (i : ι), f i) = 0
h✝ : IsEmpty ι
⊢ a ≠ 0
exact mt h0 (not_nonempty_iff.2 ‹_›)
no goals
case neg.inr
α : Type ?u.115719
β : Type ?u.115722
γ : Type ?u.115725
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
h : a = ⊤ → (⨅ (i : ι), f i) = 0 → ∃ i, f i = 0
h0 : a = 0 → Nonempty ι
H : ¬a = ⊤ ∨ ¬(⨅ (i : ι), f i) = 0
h✝ : Nonempty ι
⊢ (⨅ (i : ι), a * f i) = a * ⨅ (i : ι), f i
exact (ENNReal.mul_left_mono.map_iInf_of_continuousAt'
  (ENNReal.continuousAt_const_mul H)).symm