ι : Type u_2
κ : Type ?u.66748
α : Type u_1
inst✝³ : LinearOrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x => b
H : ∀ (s : Finset ι), card s • b ≤ ∑' (x : ι), b
⊢ Finite ι
ι : Type u_2
κ : Type ?u.66748
α : Type u_1
inst✝³ : LinearOrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x => b
⊢ Finite ι
have H : ∀ s : Finset ι, s.card • b ≤ ∑' _ : ι, b := fun s => by
  simpa using sum_le_hasSum s (fun a _ => hb.le) hf.hasSum
case intro
ι : Type u_2
κ : Type ?u.66748
α : Type u_1
inst✝³ : LinearOrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x => b
H : ∀ (s : Finset ι), card s • b ≤ ∑' (x : ι), b
n : ℕ
hn : (∑' (x : ι), b) ≤ n • b
⊢ Finite ι
ι : Type u_2
κ : Type ?u.66748
α : Type u_1
inst✝³ : LinearOrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x => b
H : ∀ (s : Finset ι), card s • b ≤ ∑' (x : ι), b
⊢ Finite ι
obtain ⟨n, hn⟩ := Archimedean.arch (∑' _ : ι, b) hb
case intro
ι : Type u_2
κ : Type ?u.66748
α : Type u_1
inst✝³ : LinearOrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x => b
H : ∀ (s : Finset ι), card s • b ≤ ∑' (x : ι), b
n : ℕ
hn : (∑' (x : ι), b) ≤ n • b
this : ∀ (s : Finset ι), card s ≤ n
⊢ Finite ι
case intro
ι : Type u_2
κ : Type ?u.66748
α : Type u_1
inst✝³ : LinearOrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x => b
H : ∀ (s : Finset ι), card s • b ≤ ∑' (x : ι), b
n : ℕ
hn : (∑' (x : ι), b) ≤ n • b
⊢ Finite ι
have : ∀ s : Finset ι, s.card ≤ n := fun s => by
  simpa [nsmul_le_nsmul_iff hb] using (H s).trans hn
case intro
ι : Type u_2
κ : Type ?u.66748
α : Type u_1
inst✝³ : LinearOrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x => b
H : ∀ (s : Finset ι), card s • b ≤ ∑' (x : ι), b
n : ℕ
hn : (∑' (x : ι), b) ≤ n • b
this✝ : ∀ (s : Finset ι), card s ≤ n
this : Fintype ι
⊢ Finite ι
case intro
ι : Type u_2
κ : Type ?u.66748
α : Type u_1
inst✝³ : LinearOrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x => b
H : ∀ (s : Finset ι), card s • b ≤ ∑' (x : ι), b
n : ℕ
hn : (∑' (x : ι), b) ≤ n • b
this : ∀ (s : Finset ι), card s ≤ n
⊢ Finite ι
have : Fintype ι := fintypeOfFinsetCardLe n this
no goals
case intro
ι : Type u_2
κ : Type ?u.66748
α : Type u_1
inst✝³ : LinearOrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x => b
H : ∀ (s : Finset ι), card s • b ≤ ∑' (x : ι), b
n : ℕ
hn : (∑' (x : ι), b) ≤ n • b
this✝ : ∀ (s : Finset ι), card s ≤ n
this : Fintype ι
⊢ Finite ι
infer_instance
no goals
ι : Type u_2
κ : Type ?u.66748
α : Type u_1
inst✝³ : LinearOrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x => b
s : Finset ι
⊢ card s • b ≤ ∑' (x : ι), b
simpa using sum_le_hasSum s (fun a _ => hb.le) hf.hasSum
no goals
ι : Type u_2
κ : Type ?u.66748
α : Type u_1
inst✝³ : LinearOrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x => b
H : ∀ (s : Finset ι), card s • b ≤ ∑' (x : ι), b
n : ℕ
hn : (∑' (x : ι), b) ≤ n • b
s : Finset ι
⊢ card s ≤ n
simpa [nsmul_le_nsmul_iff hb] using (H s).trans hn