α : Type ?u.300385
β : Type ?u.300388
γ : Type ?u.300391
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g : α → ℝ≥0∞
f : ℕ → ℝ≥0∞
hf : f 0 = ⊤ ∨ (∑' (b : ℕ), f (b + 1)) = ⊤
hf0 : f 0 ≠ ⊤
⊢ (∑' (n : ℕ), f (n + 1)) = ⊤
α : Type ?u.300385
β : Type ?u.300388
γ : Type ?u.300391
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g : α → ℝ≥0∞
f : ℕ → ℝ≥0∞
hf : (∑' (n : ℕ), f n) = ⊤
hf0 : f 0 ≠ ⊤
⊢ (∑' (n : ℕ), f (n + 1)) = ⊤
rw [tsum_eq_zero_add' ENNReal.summable, add_eq_top] at hf
no goals
α : Type ?u.300385
β : Type ?u.300388
γ : Type ?u.300391
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g : α → ℝ≥0∞
f : ℕ → ℝ≥0∞
hf : f 0 = ⊤ ∨ (∑' (b : ℕ), f (b + 1)) = ⊤
hf0 : f 0 ≠ ⊤
⊢ (∑' (n : ℕ), f (n + 1)) = ⊤
exact hf.resolve_left hf0