case intro
α : Type ?u.476292
β : Type ?u.476295
ι✝ : Type ?u.476298
ε : ℝ≥0
hε : ε ≠ 0
ι : Type u_1
inst✝ : Countable ι
val✝ : Encodable ι
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε
α : Type ?u.476292
β : Type ?u.476295
ι✝ : Type ?u.476298
ε : ℝ≥0
hε : ε ≠ 0
ι : Type u_1
inst✝ : Countable ι
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε
cases nonempty_encodable ι
case intro.intro.intro
α : Type ?u.476292
β : Type ?u.476295
ι✝ : Type ?u.476298
ε : ℝ≥0
hε : ε ≠ 0
ι : Type u_1
inst✝ : Countable ι
val✝ : Encodable ι
a : ℝ≥0
a0 : 0 < a
aε : a < ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε
case intro
α : Type ?u.476292
β : Type ?u.476295
ι✝ : Type ?u.476298
ε : ℝ≥0
hε : ε ≠ 0
ι : Type u_1
inst✝ : Countable ι
val✝ : Encodable ι
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε
obtain ⟨a, a0, aε⟩ := exists_between (pos_iff_ne_zero.2 hε)
case intro.intro.intro.mk.intro.intro.intro
α : Type ?u.476292
β : Type ?u.476295
ι✝ : Type ?u.476298
ε : ℝ≥0
hε : ε ≠ 0
ι : Type u_1
inst✝ : Countable ι
val✝ : Encodable ι
a : ℝ≥0
a0 : 0 < a
aε : a < ε
ε' : ι → ℝ
hε' : ∀ (i : ι), 0 < ε' i
c : ℝ
hc : HasSum ε' c
hcε : c ≤ (fun a => ↑a) a
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε
case intro.intro.intro
α : Type ?u.476292
β : Type ?u.476295
ι✝ : Type ?u.476298
ε : ℝ≥0
hε : ε ≠ 0
ι : Type u_1
inst✝ : Countable ι
val✝ : Encodable ι
a : ℝ≥0
a0 : 0 < a
aε : a < ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε
obtain ⟨ε', hε', c, hc, hcε⟩ := posSumOfEncodable a0 ι
no goals
case intro.intro.intro.mk.intro.intro.intro
α : Type ?u.476292
β : Type ?u.476295
ι✝ : Type ?u.476298
ε : ℝ≥0
hε : ε ≠ 0
ι : Type u_1
inst✝ : Countable ι
val✝ : Encodable ι
a : ℝ≥0
a0 : 0 < a
aε : a < ε
ε' : ι → ℝ
hε' : ∀ (i : ι), 0 < ε' i
c : ℝ
hc : HasSum ε' c
hcε : c ≤ (fun a => ↑a) a
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε
exact
  ⟨fun i => ⟨ε' i, (hε' i).le⟩, fun i => NNReal.coe_lt_coe.1 <| hε' i,
    ⟨c, hasSum_le (fun i => (hε' i).le) hasSum_zero hc⟩, NNReal.hasSum_coe.1 hc,
    aε.trans_le' <| NNReal.coe_le_coe.1 hcε⟩