case intro
α : Type ?u.479540
β : Type ?u.479543
ι✝ : Type ?u.479546
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_1
inst✝ : Countable ι
w : ι → ℝ≥0
⊢ ∃ δ, (∀ (i : ι), 0 < δ i) ∧ (∑' (i : ι), (fun i => ↑(w i)) i * ↑(δ i)) < ε
α : Type ?u.479540
β : Type ?u.479543
ι✝ : Type ?u.479546
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_1
inst✝ : Countable ι
w : ι → ℝ≥0∞
hw : ∀ (i : ι), w i ≠ ⊤
⊢ ∃ δ, (∀ (i : ι), 0 < δ i) ∧ (∑' (i : ι), w i * ↑(δ i)) < ε
lift w to ι → ℝ≥0 using hw
case intro.intro.intro
α : Type ?u.479540
β : Type ?u.479543
ι✝ : Type ?u.479546
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_1
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : (∑' (i : ι), ↑(δ' i)) < ε
⊢ ∃ δ, (∀ (i : ι), 0 < δ i) ∧ (∑' (i : ι), (fun i => ↑(w i)) i * ↑(δ i)) < ε
case intro
α : Type ?u.479540
β : Type ?u.479543
ι✝ : Type ?u.479546
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_1
inst✝ : Countable ι
w : ι → ℝ≥0
⊢ ∃ δ, (∀ (i : ι), 0 < δ i) ∧ (∑' (i : ι), (fun i => ↑(w i)) i * ↑(δ i)) < ε
rcases exists_pos_sum_of_countable hε ι with ⟨δ', Hpos, Hsum⟩
case intro.intro.intro
α : Type ?u.479540
β : Type ?u.479543
ι✝ : Type ?u.479546
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_1
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : (∑' (i : ι), ↑(δ' i)) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
⊢ ∃ δ, (∀ (i : ι), 0 < δ i) ∧ (∑' (i : ι), (fun i => ↑(w i)) i * ↑(δ i)) < ε
case intro.intro.intro
α : Type ?u.479540
β : Type ?u.479543
ι✝ : Type ?u.479546
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_1
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : (∑' (i : ι), ↑(δ' i)) < ε
⊢ ∃ δ, (∀ (i : ι), 0 < δ i) ∧ (∑' (i : ι), (fun i => ↑(w i)) i * ↑(δ i)) < ε
have : ∀ i, 0 < max 1 (w i) := fun i => zero_lt_one.trans_le (le_max_left _ _)
case intro.intro.intro
α : Type ?u.479540
β : Type ?u.479543
ι✝ : Type ?u.479546
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_1
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : (∑' (i : ι), ↑(δ' i)) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
⊢ (∑' (i : ι), (fun i => ↑(w i)) i * ↑((fun i => δ' i / max 1 (w i)) i)) < ε
case intro.intro.intro
α : Type ?u.479540
β : Type ?u.479543
ι✝ : Type ?u.479546
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_1
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : (∑' (i : ι), ↑(δ' i)) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
⊢ ∃ δ, (∀ (i : ι), 0 < δ i) ∧ (∑' (i : ι), (fun i => ↑(w i)) i * ↑(δ i)) < ε
refine' ⟨fun i => δ' i / max 1 (w i), fun i => div_pos (Hpos _) (this i), _⟩
case intro.intro.intro
α : Type ?u.479540
β : Type ?u.479543
ι✝ : Type ?u.479546
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_1
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : (∑' (i : ι), ↑(δ' i)) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
i : ι
⊢ (fun i => ↑(w i)) i * ↑((fun i => δ' i / max 1 (w i)) i) ≤ ↑(δ' i)
case intro.intro.intro
α : Type ?u.479540
β : Type ?u.479543
ι✝ : Type ?u.479546
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_1
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : (∑' (i : ι), ↑(δ' i)) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
⊢ (∑' (i : ι), (fun i => ↑(w i)) i * ↑((fun i => δ' i / max 1 (w i)) i)) < ε
refine' lt_of_le_of_lt (ENNReal.tsum_le_tsum fun i => _) Hsum
case intro.intro.intro
α : Type ?u.479540
β : Type ?u.479543
ι✝ : Type ?u.479546
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_1
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : (∑' (i : ι), ↑(δ' i)) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
i : ι
⊢ (fun i => ↑(w i)) i * (↑(δ' i) / ↑(max 1 (w i))) ≤ ↑(δ' i)
case intro.intro.intro
α : Type ?u.479540
β : Type ?u.479543
ι✝ : Type ?u.479546
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_1
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : (∑' (i : ι), ↑(δ' i)) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
i : ι
⊢ (fun i => ↑(w i)) i * ↑((fun i => δ' i / max 1 (w i)) i) ≤ ↑(δ' i)
rw [coe_div (this i).ne']
case intro.intro.intro
α : Type ?u.479540
β : Type ?u.479543
ι✝ : Type ?u.479546
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_1
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : (∑' (i : ι), ↑(δ' i)) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
i : ι
⊢ (fun i => ↑(w i)) i ≤ ↑(max 1 (w i))
case intro.intro.intro
α : Type ?u.479540
β : Type ?u.479543
ι✝ : Type ?u.479546
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_1
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : (∑' (i : ι), ↑(δ' i)) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
i : ι
⊢ (fun i => ↑(w i)) i * (↑(δ' i) / ↑(max 1 (w i))) ≤ ↑(δ' i)
refine' mul_le_of_le_div' (mul_le_mul_left' (ENNReal.inv_le_inv.2 _) _)
no goals
case intro.intro.intro
α : Type ?u.479540
β : Type ?u.479543
ι✝ : Type ?u.479546
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_1
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : (∑' (i : ι), ↑(δ' i)) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
i : ι
⊢ (fun i => ↑(w i)) i ≤ ↑(max 1 (w i))
exact coe_le_coe.2 (le_max_right _ _)