-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem exists_pos_tsum_mul_lt_of_countable {ε : ℝ≥0∞} (hε : ε ≠ 0) {ι} [Countable ι] (w : ι → ℝ≥0∞)
    (hw : ∀ i, w i ≠ ∞) : ∃ δ : ι → ℝ≥0, (∀ i, 0 < δ i) ∧ (∑' i, (w i * δ i : ℝ≥0∞)) < ε

Proof state:
case intro.intro.intro
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), ↑(δ' i) < ε
this : ∀ (i : ι), 0 < 1 ⊔ w i
i : ι
⊢ (fun i => ↑(w i)) i * ↑((fun i => δ' i / (1 ⊔ w i)) i) ≤ ↑(δ' i)

Tactic:
rw [coe_div (this i).ne']

Result:
case intro.intro.intro
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), ↑(δ' i) < ε
this : ∀ (i : ι), 0 < 1 ⊔ w i
i : ι
⊢ (fun i => ↑(w i)) i * (↑(δ' i) / ↑(1 ⊔ w i)) ≤ ↑(δ' i)

Proof state:
case intro.intro.intro
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), ↑(δ' i) < ε
⊢ ∃ δ, (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), (fun i => ↑(w i)) i * ↑(δ i) < ε

Tactic:
have : ∀ i, 0 < max 1 (w i) := fun i ↦ zero_lt_one.trans_le (le_max_left _ _)

Result:
case intro.intro.intro
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), ↑(δ' i) < ε
this : ∀ (i : ι), 0 < 1 ⊔ w i
⊢ ∃ δ, (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), (fun i => ↑(w i)) i * ↑(δ i) < ε

Proof state:
case intro.intro.intro
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), ↑(δ' i) < ε
this : ∀ (i : ι), 0 < 1 ⊔ w i
⊢ ∑' (i : ι), (fun i => ↑(w i)) i * ↑((fun i => δ' i / (1 ⊔ w i)) i) < ε

Tactic:
refine lt_of_le_of_lt (ENNReal.tsum_le_tsum fun i ↦ ?_) Hsum

Result:
case intro.intro.intro
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), ↑(δ' i) < ε
this : ∀ (i : ι), 0 < 1 ⊔ w i
i : ι
⊢ (fun i => ↑(w i)) i * ↑((fun i => δ' i / (1 ⊔ w i)) i) ≤ ↑(δ' i)

Proof state:
case intro
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w : ι → ℝ≥0
⊢ ∃ δ, (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), (fun i => ↑(w i)) i * ↑(δ i) < ε

Tactic:
rcases exists_pos_sum_of_countable hε ι with ⟨δ', Hpos, Hsum⟩

Result:
case intro.intro.intro
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), ↑(δ' i) < ε
⊢ ∃ δ, (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), (fun i => ↑(w i)) i * ↑(δ i) < ε

Proof state:
case intro.intro.intro
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), ↑(δ' i) < ε
this : ∀ (i : ι), 0 < 1 ⊔ w i
⊢ ∃ δ, (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), (fun i => ↑(w i)) i * ↑(δ i) < ε

Tactic:
refine ⟨fun i ↦ δ' i / max 1 (w i), fun i ↦ div_pos (Hpos _) (this i), ?_⟩

Result:
case intro.intro.intro
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), ↑(δ' i) < ε
this : ∀ (i : ι), 0 < 1 ⊔ w i
⊢ ∑' (i : ι), (fun i => ↑(w i)) i * ↑((fun i => δ' i / (1 ⊔ w i)) i) < ε

Proof state:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w : ι → ℝ≥0∞
hw : ∀ (i : ι), w i ≠ ⊤
⊢ ∃ δ, (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), w i * ↑(δ i) < ε

Tactic:
lift w to ι → ℝ≥0 using hw

Result:
case intro
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w : ι → ℝ≥0
⊢ ∃ δ, (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), (fun i => ↑(w i)) i * ↑(δ i) < ε

Proof state:
case intro.intro.intro
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), ↑(δ' i) < ε
this : ∀ (i : ι), 0 < 1 ⊔ w i
i : ι
⊢ (fun i => ↑(w i)) i * (↑(δ' i) / ↑(1 ⊔ w i)) ≤ ↑(δ' i)

Tactic:
refine mul_le_of_le_div' (mul_le_mul_left' (ENNReal.inv_le_inv.2 ?_) _)

Result:
case intro.intro.intro
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), ↑(δ' i) < ε
this : ∀ (i : ι), 0 < 1 ⊔ w i
i : ι
⊢ (fun i => ↑(w i)) i ≤ ↑(1 ⊔ w i)

Proof state:
case intro.intro.intro
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), ↑(δ' i) < ε
this : ∀ (i : ι), 0 < 1 ⊔ w i
i : ι
⊢ (fun i => ↑(w i)) i ≤ ↑(1 ⊔ w i)

Tactic:
exact coe_le_coe.2 (le_max_right _ _)

Result:
no goals