case intro.intro
α : Type ?u.477583
β : Type ?u.477586
ι✝ : Type ?u.477589
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_1
inst✝ : Countable ι
r : ℝ≥0∞
h0r : 0 < r
hrε : r < ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ (∑' (i : ι), ↑(ε' i)) < ε
α : Type ?u.477583
β : Type ?u.477586
ι✝ : Type ?u.477589
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_1
inst✝ : Countable ι
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ (∑' (i : ι), ↑(ε' i)) < ε
rcases exists_between (pos_iff_ne_zero.2 hε) with ⟨r, h0r, hrε⟩
case intro.intro.intro.intro
α : Type ?u.477583
β : Type ?u.477586
ι✝ : Type ?u.477589
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_1
inst✝ : Countable ι
x : ℝ≥0
right✝ : ↑x < ε
h0r : 0 < ↑x
hrε : ↑x < ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ (∑' (i : ι), ↑(ε' i)) < ε
case intro.intro
α : Type ?u.477583
β : Type ?u.477586
ι✝ : Type ?u.477589
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_1
inst✝ : Countable ι
r : ℝ≥0∞
h0r : 0 < r
hrε : r < ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ (∑' (i : ι), ↑(ε' i)) < ε
rcases lt_iff_exists_coe.1 hrε with ⟨x, rfl, _⟩
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type ?u.477583
β : Type ?u.477586
ι✝ : Type ?u.477589
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_1
inst✝ : Countable ι
x : ℝ≥0
right✝ : ↑x < ε
h0r : 0 < ↑x
hrε : ↑x < ε
ε' : ι → ℝ≥0
hp : ∀ (i : ι), 0 < ε' i
c : ℝ≥0
hc : HasSum ε' c
hcr : c < x
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ (∑' (i : ι), ↑(ε' i)) < ε
case intro.intro.intro.intro
α : Type ?u.477583
β : Type ?u.477586
ι✝ : Type ?u.477589
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_1
inst✝ : Countable ι
x : ℝ≥0
right✝ : ↑x < ε
h0r : 0 < ↑x
hrε : ↑x < ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ (∑' (i : ι), ↑(ε' i)) < ε
rcases NNReal.exists_pos_sum_of_countable (coe_pos.1 h0r).ne' ι with ⟨ε', hp, c, hc, hcr⟩
no goals
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type ?u.477583
β : Type ?u.477586
ι✝ : Type ?u.477589
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_1
inst✝ : Countable ι
x : ℝ≥0
right✝ : ↑x < ε
h0r : 0 < ↑x
hrε : ↑x < ε
ε' : ι → ℝ≥0
hp : ∀ (i : ι), 0 < ε' i
c : ℝ≥0
hc : HasSum ε' c
hcr : c < x
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ (∑' (i : ι), ↑(ε' i)) < ε
exact ⟨ε', hp, (ENNReal.tsum_coe_eq hc).symm ▸ lt_trans (coe_lt_coe.2 hcr) hrε⟩