case intro.intro.intro.intro
α : Type ?u.475376
β : Type ?u.475379
ι✝ : Type ?u.475382
ι : Type u_1
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
ε' : ι → ℝ
hpos : ∀ (i : ι), 0 < ε' i
c : ℝ
hε'c : HasSum (fun i => ε' ↑i) c
hcε : c ≤ ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∀ (t : Finset ι), ↑t ⊆ s → ∑ i in t, ε' i ≤ ε
α : Type ?u.475376
β : Type ?u.475379
ι✝ : Type ?u.475382
ι : Type u_1
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∀ (t : Finset ι), ↑t ⊆ s → ∑ i in t, ε' i ≤ ε
rcases hs.exists_pos_hasSum_le hε with ⟨ε', hpos, c, hε'c, hcε⟩
case intro.intro.intro.intro
α : Type ?u.475376
β : Type ?u.475379
ι✝ : Type ?u.475382
ι : Type u_1
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
ε' : ι → ℝ
hpos : ∀ (i : ι), 0 < ε' i
c : ℝ
hε'c : HasSum (fun i => ε' ↑i) c
hcε : c ≤ ε
t : Finset ι
ht : ↑t ⊆ s
⊢ ∑ i in t, ε' i ≤ ε
case intro.intro.intro.intro
α : Type ?u.475376
β : Type ?u.475379
ι✝ : Type ?u.475382
ι : Type u_1
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
ε' : ι → ℝ
hpos : ∀ (i : ι), 0 < ε' i
c : ℝ
hε'c : HasSum (fun i => ε' ↑i) c
hcε : c ≤ ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∀ (t : Finset ι), ↑t ⊆ s → ∑ i in t, ε' i ≤ ε
refine' ⟨ε', hpos, fun t ht => _⟩
case intro.intro.intro.intro
α : Type ?u.475376
β : Type ?u.475379
ι✝ : Type ?u.475382
ι : Type u_1
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
ε' : ι → ℝ
hpos : ∀ (i : ι), 0 < ε' i
c : ℝ
hε'c : HasSum (fun i => ε' ↑i) c
hcε : c ≤ ε
t : Finset ι
ht : ↑t ⊆ s
⊢ ∑ x in Finset.subtype (fun x => x ∈ s) t, ε' ↑x ≤ ε
case intro.intro.intro.intro
α : Type ?u.475376
β : Type ?u.475379
ι✝ : Type ?u.475382
ι : Type u_1
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
ε' : ι → ℝ
hpos : ∀ (i : ι), 0 < ε' i
c : ℝ
hε'c : HasSum (fun i => ε' ↑i) c
hcε : c ≤ ε
t : Finset ι
ht : ↑t ⊆ s
⊢ ∑ i in t, ε' i ≤ ε
rw [← sum_subtype_of_mem _ ht]
case intro.intro.intro.intro
α : Type ?u.475376
β : Type ?u.475379
ι✝ : Type ?u.475382
ι : Type u_1
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
ε' : ι → ℝ
hpos : ∀ (i : ι), 0 < ε' i
c : ℝ
hε'c : HasSum (fun i => ε' ↑i) c
hcε : c ≤ ε
t : Finset ι
ht : ↑t ⊆ s
⊢ ∀ (i : ↑s), ¬i ∈ Finset.subtype (fun x => x ∈ s) t → 0 ≤ ε' ↑i
case intro.intro.intro.intro
α : Type ?u.475376
β : Type ?u.475379
ι✝ : Type ?u.475382
ι : Type u_1
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
ε' : ι → ℝ
hpos : ∀ (i : ι), 0 < ε' i
c : ℝ
hε'c : HasSum (fun i => ε' ↑i) c
hcε : c ≤ ε
t : Finset ι
ht : ↑t ⊆ s
⊢ ∑ x in Finset.subtype (fun x => x ∈ s) t, ε' ↑x ≤ ε
refine' (sum_le_hasSum _ _ hε'c).trans hcε
no goals
case intro.intro.intro.intro
α : Type ?u.475376
β : Type ?u.475379
ι✝ : Type ?u.475382
ι : Type u_1
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
ε' : ι → ℝ
hpos : ∀ (i : ι), 0 < ε' i
c : ℝ
hε'c : HasSum (fun i => ε' ↑i) c
hcε : c ≤ ε
t : Finset ι
ht : ↑t ⊆ s
⊢ ∀ (i : ↑s), ¬i ∈ Finset.subtype (fun x => x ∈ s) t → 0 ≤ ε' ↑i
exact fun _ _ => (hpos _).le