α : Type ?u.472618
β : Type ?u.472621
ι✝ : Type ?u.472624
ι : Type u_1
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum (fun i => ε' ↑i) c ∧ c ≤ ε
α : Type ?u.472618
β : Type ?u.472621
ι✝ : Type ?u.472624
ι : Type u_1
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum (fun i => ε' ↑i) c ∧ c ≤ ε
haveI := hs.toEncodable
case mk.intro.intro.intro
α : Type ?u.472618
β : Type ?u.472621
ι✝ : Type ?u.472624
ι : Type u_1
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
f : ↑s → ℝ
hf0 : ∀ (i : ↑s), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum (fun i => ε' ↑i) c ∧ c ≤ ε
α : Type ?u.472618
β : Type ?u.472621
ι✝ : Type ?u.472624
ι : Type u_1
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum (fun i => ε' ↑i) c ∧ c ≤ ε
rcases posSumOfEncodable hε s with ⟨f, hf0, ⟨c, hfc, hcε⟩⟩
case mk.intro.intro.intro.refine'_1
α : Type ?u.472618
β : Type ?u.472621
ι✝ : Type ?u.472624
ι : Type u_1
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
f : ↑s → ℝ
hf0 : ∀ (i : ↑s), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
i : ι
⊢ 0 < (fun i => if h : i ∈ s then f { val := i, property := h } else 1) i

case mk.intro.intro.intro.refine'_2
α : Type ?u.472618
β : Type ?u.472621
ι✝ : Type ?u.472624
ι : Type u_1
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
f : ↑s → ℝ
hf0 : ∀ (i : ↑s), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
⊢ HasSum (fun i => (fun i => if h : i ∈ s then f { val := i, property := h } else 1) ↑i) c
case mk.intro.intro.intro
α : Type ?u.472618
β : Type ?u.472621
ι✝ : Type ?u.472624
ι : Type u_1
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
f : ↑s → ℝ
hf0 : ∀ (i : ↑s), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum (fun i => ε' ↑i) c ∧ c ≤ ε
refine' ⟨fun i => if h : i ∈ s then f ⟨i, h⟩ else 1, fun i => _, ⟨c, _, hcε⟩⟩
case mk.intro.intro.intro.refine'_1
α : Type ?u.472618
β : Type ?u.472621
ι✝ : Type ?u.472624
ι : Type u_1
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
f : ↑s → ℝ
hf0 : ∀ (i : ↑s), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
i : ι
⊢ 0 < if h : i ∈ s then f { val := i, property := h } else 1
case mk.intro.intro.intro.refine'_1
α : Type ?u.472618
β : Type ?u.472621
ι✝ : Type ?u.472624
ι : Type u_1
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
f : ↑s → ℝ
hf0 : ∀ (i : ↑s), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
i : ι
⊢ 0 < (fun i => if h : i ∈ s then f { val := i, property := h } else 1) i
conv_rhs => simp
case mk.intro.intro.intro.refine'_1.inl
α : Type ?u.472618
β : Type ?u.472621
ι✝ : Type ?u.472624
ι : Type u_1
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
f : ↑s → ℝ
hf0 : ∀ (i : ↑s), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
i : ι
h✝ : i ∈ s
⊢ 0 < f { val := i, property := h✝ }

case mk.intro.intro.intro.refine'_1.inr
α : Type ?u.472618
β : Type ?u.472621
ι✝ : Type ?u.472624
ι : Type u_1
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
f : ↑s → ℝ
hf0 : ∀ (i : ↑s), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
i : ι
h✝ : ¬i ∈ s
⊢ 0 < 1
case mk.intro.intro.intro.refine'_1
α : Type ?u.472618
β : Type ?u.472621
ι✝ : Type ?u.472624
ι : Type u_1
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
f : ↑s → ℝ
hf0 : ∀ (i : ↑s), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
i : ι
⊢ 0 < if h : i ∈ s then f { val := i, property := h } else 1
split_ifs
no goals
case mk.intro.intro.intro.refine'_1.inl
α : Type ?u.472618
β : Type ?u.472621
ι✝ : Type ?u.472624
ι : Type u_1
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
f : ↑s → ℝ
hf0 : ∀ (i : ↑s), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
i : ι
h✝ : i ∈ s
⊢ 0 < f { val := i, property := h✝ }

case mk.intro.intro.intro.refine'_1.inr
α : Type ?u.472618
β : Type ?u.472621
ι✝ : Type ?u.472624
ι : Type u_1
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
f : ↑s → ℝ
hf0 : ∀ (i : ↑s), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
i : ι
h✝ : ¬i ∈ s
⊢ 0 < 1
exacts [hf0 _, zero_lt_one]
no goals
case mk.intro.intro.intro.refine'_2
α : Type ?u.472618
β : Type ?u.472621
ι✝ : Type ?u.472624
ι : Type u_1
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
f : ↑s → ℝ
hf0 : ∀ (i : ↑s), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
⊢ HasSum (fun i => (fun i => if h : i ∈ s then f { val := i, property := h } else 1) ↑i) c
simpa only [Subtype.coe_prop, dif_pos, Subtype.coe_eta]