α : Type ?u.301039
β : Type ?u.301042
γ : Type ?u.301045
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε✝ ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f g : α → ℝ≥0∞
ι : Type u_1
a : ι → ℝ≥0∞
tsum_ne_top : (∑' (i : ι), a i) ≠ ⊤
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
h : ¬Set.Finite {i | ε ≤ a i}
⊢ False
α : Type ?u.301039
β : Type ?u.301042
γ : Type ?u.301045
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε✝ ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f g : α → ℝ≥0∞
ι : Type u_1
a : ι → ℝ≥0∞
tsum_ne_top : (∑' (i : ι), a i) ≠ ⊤
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
⊢ Set.Finite {i | ε ≤ a i}
by_contra h
α : Type ?u.301039
β : Type ?u.301042
γ : Type ?u.301045
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε✝ ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f g : α → ℝ≥0∞
ι : Type u_1
a : ι → ℝ≥0∞
tsum_ne_top : (∑' (i : ι), a i) ≠ ⊤
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
h : ¬Set.Finite {i | ε ≤ a i}
this : Infinite ↑{i | ε ≤ a i}
⊢ False
α : Type ?u.301039
β : Type ?u.301042
γ : Type ?u.301045
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε✝ ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f g : α → ℝ≥0∞
ι : Type u_1
a : ι → ℝ≥0∞
tsum_ne_top : (∑' (i : ι), a i) ≠ ⊤
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
h : ¬Set.Finite {i | ε ≤ a i}
⊢ False
have := Infinite.to_subtype h
α : Type ?u.301039
β : Type ?u.301042
γ : Type ?u.301045
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε✝ ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f g : α → ℝ≥0∞
ι : Type u_1
a : ι → ℝ≥0∞
tsum_ne_top : (∑' (i : ι), a i) ≠ ⊤
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
h : ¬Set.Finite {i | ε ≤ a i}
this : Infinite ↑{i | ε ≤ a i}
⊢ ⊤ ≤ ∑' (i : ι), a i
α : Type ?u.301039
β : Type ?u.301042
γ : Type ?u.301045
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε✝ ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f g : α → ℝ≥0∞
ι : Type u_1
a : ι → ℝ≥0∞
tsum_ne_top : (∑' (i : ι), a i) ≠ ⊤
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
h : ¬Set.Finite {i | ε ≤ a i}
this : Infinite ↑{i | ε ≤ a i}
⊢ False
refine tsum_ne_top (top_unique ?_)
no goals
α : Type ?u.301039
β : Type ?u.301042
γ : Type ?u.301045
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε✝ ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f g : α → ℝ≥0∞
ι : Type u_1
a : ι → ℝ≥0∞
tsum_ne_top : (∑' (i : ι), a i) ≠ ⊤
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
h : ¬Set.Finite {i | ε ≤ a i}
this : Infinite ↑{i | ε ≤ a i}
⊢ ⊤ ≤ ∑' (i : ι), a i
calc ⊤ = ∑' _ : { i | ε ≤ a i }, ε := (tsum_const_eq_top_of_ne_zero ε_ne_zero).symm
_ ≤ ∑' i, a i := tsum_le_tsum_of_inj (↑) Subtype.val_injective (fun _ _ => zero_le _)
  (fun i => i.2) ENNReal.summable ENNReal.summable