α✝ : Type ?u.246869
β : Type ?u.246872
γ : Type ?u.246875
a b c✝ d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f g : α✝ → ℝ≥0∞
α : Type u_1
inst✝ : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
A : Tendsto (fun n => ↑n * c) atTop (𝓝 (⊤ * c))
⊢ (∑' (x : α), c) = ⊤
α✝ : Type ?u.246869
β : Type ?u.246872
γ : Type ?u.246875
a b c✝ d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f g : α✝ → ℝ≥0∞
α : Type u_1
inst✝ : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
⊢ (∑' (x : α), c) = ⊤
have A : Tendsto (fun n : ℕ => (n : ℝ≥0∞) * c) atTop (𝓝 (∞ * c)) := by
  apply ENNReal.Tendsto.mul_const tendsto_nat_nhds_top
  simp only [true_or_iff, top_ne_zero, Ne.def, not_false_iff]
α✝ : Type ?u.246869
β : Type ?u.246872
γ : Type ?u.246875
a b c✝ d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f g : α✝ → ℝ≥0∞
α : Type u_1
inst✝ : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
A : Tendsto (fun n => ↑n * c) atTop (𝓝 (⊤ * c))
B : ∀ (n : ℕ), ↑n * c ≤ ∑' (x : α), c
⊢ (∑' (x : α), c) = ⊤
α✝ : Type ?u.246869
β : Type ?u.246872
γ : Type ?u.246875
a b c✝ d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f g : α✝ → ℝ≥0∞
α : Type u_1
inst✝ : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
A : Tendsto (fun n => ↑n * c) atTop (𝓝 (⊤ * c))
⊢ (∑' (x : α), c) = ⊤
have B : ∀ n : ℕ, (n : ℝ≥0∞) * c ≤ ∑' _ : α, c := fun n => by
  rcases Infinite.exists_subset_card_eq α n with ⟨s, hs⟩
  simpa [hs] using @ENNReal.sum_le_tsum α (fun _ => c) s
no goals
α✝ : Type ?u.246869
β : Type ?u.246872
γ : Type ?u.246875
a b c✝ d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f g : α✝ → ℝ≥0∞
α : Type u_1
inst✝ : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
A : Tendsto (fun n => ↑n * c) atTop (𝓝 (⊤ * c))
B : ∀ (n : ℕ), ↑n * c ≤ ∑' (x : α), c
⊢ (∑' (x : α), c) = ⊤
simpa [hc] using le_of_tendsto' A B
α✝ : Type ?u.246869
β : Type ?u.246872
γ : Type ?u.246875
a b c✝ d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f g : α✝ → ℝ≥0∞
α : Type u_1
inst✝ : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
⊢ ⊤ ≠ 0 ∨ c ≠ ⊤
α✝ : Type ?u.246869
β : Type ?u.246872
γ : Type ?u.246875
a b c✝ d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f g : α✝ → ℝ≥0∞
α : Type u_1
inst✝ : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
⊢ Tendsto (fun n => ↑n * c) atTop (𝓝 (⊤ * c))
apply ENNReal.Tendsto.mul_const tendsto_nat_nhds_top
no goals
α✝ : Type ?u.246869
β : Type ?u.246872
γ : Type ?u.246875
a b c✝ d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f g : α✝ → ℝ≥0∞
α : Type u_1
inst✝ : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
⊢ ⊤ ≠ 0 ∨ c ≠ ⊤
simp only [true_or_iff, top_ne_zero, Ne.def, not_false_iff]
case intro
α✝ : Type ?u.246869
β : Type ?u.246872
γ : Type ?u.246875
a b c✝ d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s✝ : Set ℝ≥0∞
f g : α✝ → ℝ≥0∞
α : Type u_1
inst✝ : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
A : Tendsto (fun n => ↑n * c) atTop (𝓝 (⊤ * c))
n : ℕ
s : Finset α
hs : Finset.card s = n
⊢ ↑n * c ≤ ∑' (x : α), c
α✝ : Type ?u.246869
β : Type ?u.246872
γ : Type ?u.246875
a b c✝ d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f g : α✝ → ℝ≥0∞
α : Type u_1
inst✝ : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
A : Tendsto (fun n => ↑n * c) atTop (𝓝 (⊤ * c))
n : ℕ
⊢ ↑n * c ≤ ∑' (x : α), c
rcases Infinite.exists_subset_card_eq α n with ⟨s, hs⟩
no goals
case intro
α✝ : Type ?u.246869
β : Type ?u.246872
γ : Type ?u.246875
a b c✝ d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s✝ : Set ℝ≥0∞
f g : α✝ → ℝ≥0∞
α : Type u_1
inst✝ : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
A : Tendsto (fun n => ↑n * c) atTop (𝓝 (⊤ * c))
n : ℕ
s : Finset α
hs : Finset.card s = n
⊢ ↑n * c ≤ ∑' (x : α), c
simpa [hs] using @ENNReal.sum_le_tsum α (fun _ => c) s