awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_4
f : (i : α) → ℝ≥0
hf : Ne (α := ℝ≥0∞) (∑' (x : α), (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) x) ∞
⊢ Tendsto (β := ℝ≥0∞) (fun (s : Finset α) ↦ ∑' (b : { x : α // x ∉ s }), (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) (↑b : α)) atTop
    (𝓝 0)
have h : ∀ (x : Finset α),
  ∑' (b : { x_1 : α // x_1 ∉ x }), (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) (↑b : α) =
    (↑(∑' (b : { x_1 : α // x_1 ∉ x }), f (↑b : α)) : ℝ≥0∞)
Tactic: convert! ENNReal.tendsto_coe.2 (NNReal.tendsto_tsum_compl_atTop_zero f)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_4
f : (i : α) → ℝ≥0
hf : Ne (α := ℝ≥0∞) (∑' (x : α), (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) x) ∞
x : Finset α
⊢ ∑' (b : { x_1 : α // x_1 ∉ x }), (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) (↑b : α) =
    (↑(∑' (b : { x_1 : α // x_1 ∉ x }), f (↑b : α)) : ℝ≥0∞)
have h : Summable (α := ℝ≥0) fun (b : { x_1 : α // x_1 ∉ x }) ↦ f (↑b : α)
Tactic: rw [ENNReal.coe_tsum]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
ι : Type u_4
inst : Fintype ι
f : α → ℝ≥0∞
t : ι → Set α
⊢ LE.le (α := ℝ≥0∞) (∑' (x : (↑(⋃ (i : ι), t i) : Type u_1)), f (↑x : α))
    (∑ i : ι, ∑' (x : (↑(t i) : Type u_1)), f (↑x : α))
have rw : LE.le (α := ℝ≥0∞) (∑' (x : (↑(⋃ (i : ι), t i) : Type u_1)), f (↑x : α))
  (∑' (b : ι) (x : (↑(t b) : Type u_1)), f (↑x : α))
Tactic: rw [← tsum_fintype (L := SummationFilter.unconditional _)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (hypothesis)
Goal:
f : ℕ → ℝ≥0∞
hf : Eq (α := ℝ≥0∞) (∑' (n : ℕ), f n) ∞
hf0 : f 0 ≠ ∞
⊢ Eq (α := ℝ≥0∞) (∑' (n : ℕ), f (n + 1)) ∞
have hf₁ : f 0 = ∞ ∨ Eq (α := ℝ≥0∞) (∑' (b : ℕ), f (b + 1)) ∞
Tactic: rw [tsum_eq_zero_add' ENNReal.summable, add_eq_top] at hf
Cleared hypotheses: hf, hf0
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
ι : Type u_4
a : ι → ℝ≥0∞
tsum_ne_top : Ne (α := ℝ≥0∞) (∑' (i : ι), a i) ∞
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
⊢ Set.Finite.{u_4} (α := ι) {i : ι | ε ≤ a i}
have by_contra : ∀ (h : ¬Set.Finite.{u_4} (α := ι) {i : ι | ε ≤ a i}), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (hypothesis)
Goal:
ι : Type u_4
a : ι → ℝ≥0∞
tsum_ne_top : Ne (α := ℝ≥0∞) (∑' (i : ι), a i) ∞
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
h : ¬Set.Finite.{u_4} (α := ι) {i : ι | ε ≤ a i}
⊢ False
have this : Infinite.{u_4 + 1} (↑{i : ι | ε ≤ a i} : Type u_4)
Tactic: have := Infinite.to_subtype h
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
ι : Type u_4
a : ι → ℝ≥0∞
tsum_ne_top : Ne (α := ℝ≥0∞) (∑' (i : ι), a i) ∞
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
h : ¬Set.Finite.{u_4} (α := ι) {i : ι | ε ≤ a i}
this : Infinite.{u_4 + 1} (↑{i : ι | ε ≤ a i} : Type u_4)
⊢ False
have refine : LE.le (α := ℝ≥0∞) ∞ (∑' (i : ι), a i)
Tactic: refine tsum_ne_top (top_unique ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (hypothesis)
Goal:
ι : Type u_4
a : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ∞
tsum_le_c : ∑' (i : ι), a i ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
⊢ ∃ (hf : Set.Finite.{u_4} (α := ι) {i : ι | ε ≤ a i}), (↑(#(hf.toFinset (s := {i : ι | ε ≤ a i}))) : ℝ≥0∞) ≤ c / ε
have hf : Set.Finite.{u_4} (α := ι) {i : ι | ε ≤ a i}
Tactic: have hf : { i : ι | ε ≤ a i }.Finite :=
    finite_const_le_of_tsum_ne_top (ne_top_of_le_ne_top c_ne_top tsum_le_c) ε_ne_zero
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
ι : Type u_4
a : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ∞
tsum_le_c : ∑' (i : ι), a i ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
hf : Set.Finite.{u_4} (α := ι) {i : ι | ε ≤ a i}
⊢ ∃ (hf : Set.Finite.{u_4} (α := ι) {i : ι | ε ≤ a i}), (↑(#(hf.toFinset (s := {i : ι | ε ≤ a i}))) : ℝ≥0∞) ≤ c / ε
have refine : (↑(#(hf.toFinset (s := {i : ι | ε ≤ a i}))) : ℝ≥0∞) * ε ≤ c
Tactic: refine ⟨hf, (ENNReal.le_div_iff_mul_le (.inl ε_ne_zero) (.inr c_ne_top)).2 ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
ι : Type u_4
a : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ∞
tsum_le_c : ∑' (i : ι), a i ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
hf : Set.Finite.{u_4} (α := ι) {i : ι | ε ≤ a i}
⊢ (↑(#(hf.toFinset (s := {i : ι | ε ≤ a i}))) : ℝ≥0∞) * ε = ∑ _i ∈ hf.toFinset (s := {i : ι | ε ≤ a i}), ε
have rw : (↑(#(hf.toFinset (s := {i : ι | ε ≤ a i}))) : ℝ≥0∞) * ε = #(hf.toFinset (s := {i : ι | ε ≤ a i})) • ε
Tactic: rw [Finset.sum_const, nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
ι : Type u_4
a : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ∞
tsum_le_c : ∑' (i : ι), a i ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
hf : Set.Finite.{u_4} (α := ι) {i : ι | ε ≤ a i}
rw : (↑(#(hf.toFinset (s := {i : ι | ε ≤ a i}))) : ℝ≥0∞) * ε = #(hf.toFinset (s := {i : ι | ε ≤ a i})) • ε
⊢ (↑(#(hf.toFinset (s := {i : ι | ε ≤ a i}))) : ℝ≥0∞) * ε = ∑ _i ∈ hf.toFinset (s := {i : ι | ε ≤ a i}), ε
have rw₁ : (↑(#(hf.toFinset (s := {i : ι | ε ≤ a i}))) : ℝ≥0∞) * ε = (↑(#(hf.toFinset (s := {i : ι | ε ≤ a i}))) : ℝ≥0∞) * ε
Tactic: rw [Finset.sum_const, nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
ι : Type u_4
a : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ∞
tsum_le_c : ∑' (i : ι), a i ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
hf : Set.Finite.{u_4} (α := ι) {i : ι | ε ≤ a i}
⊢ (↑(#(hf.toFinset (s := {i : ι | ε ≤ a i}))) : ℝ≥0∞) * ε ≤ c
have calc : (↑(#(hf.toFinset (s := {i : ι | ε ≤ a i}))) : ℝ≥0∞) * ε = ∑ _i ∈ hf.toFinset (s := {i : ι | ε ≤ a i}), ε
Tactic: calc #hf.toFinset * ε = ∑ _i ∈ hf.toFinset, ε := by rw [Finset.sum_const, nsmul_eq_mul]
    _ ≤ ∑ i ∈ hf.toFinset, a i := Finset.sum_le_sum fun i => hf.mem_toFinset.1
    _ ≤ ∑' i, a i := ENNReal.sum_le_tsum _
    _ ≤ c := tsum_le_c
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
β : Type u_2
γ : Type u_3
f : β → ℝ≥0∞
g : β → γ
⊢ Eq (α := ℝ≥0∞) (∑' (x : γ) (b : (↑(g ⁻¹' {x}) : Type u_2)), f (↑b : β)) (∑' (i : β), f i)
have ha : HasSum (α := ℝ≥0∞) (fun (b : γ) ↦ ∑' (b_1 : (↑(g ⁻¹' {b}) : Type u_2)), f (↑b_1 : β)) (∑' (i : β), f i)
Tactic: apply HasSum.tsum_eq
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
β : Type u_2
γ : Type u_3
f : β → ℝ≥0∞
g : β → γ
equiv : (y : γ) × { x : β // g x = y } ≃ β := Equiv.sigmaFiberEquiv g
⊢ HasSum (α := ℝ≥0∞) (fun (b : γ) ↦ ∑' (b_1 : (↑(g ⁻¹' {b}) : Type u_2)), f (↑b_1 : β)) (∑' (i : β), f i)
have ha : ∀ (b : γ),
  HasSum (α := ℝ≥0∞)
    (fun (c : { x : β // g x = b }) ↦
      comp (α := (y : γ) × { x : β // g x = y }) f (⇑equiv : (a : (y : γ) × { x : β // g x = y }) → β)
        (Sigma.mk (β := fun (b : γ) ↦ { x : β // g x = b }) b c))
    (∑' (b_1 : (↑(g ⁻¹' {b}) : Type u_2)), f (↑b_1 : β))
Tactic: apply (equiv.hasSum_iff.mpr ENNReal.summable.hasSum).sigma
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
f : α → ℝ≥0
⊢ Ne (α := ℝ≥0∞) (∑' (a : α), (↑(f a) : ℝ≥0∞)) ∞ ↔ Summable (α := ℝ) fun (a : α) ↦ (↑(f a) : ℝ)
have rw : Ne (α := ℝ≥0∞) (∑' (a : α), (↑(f a) : ℝ≥0∞)) ∞ ↔ Summable f
Tactic: rw [NNReal.summable_coe]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
f : α → ℝ≥0∞
hsum : Ne (α := ℝ≥0∞) (∑' (x : α), f x) ∞
⊢ HasSum (α := ℝ) (fun (x : α) ↦ (f x).toReal) (∑' (x : α), (f x).toReal)
have lift : ∀ (f : (i : α) → ℝ≥0) (hsum : Ne (α := ℝ≥0∞) (∑' (x : α), (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) x) ∞),
  HasSum (α := ℝ) (fun (x : α) ↦ ENNReal.toReal ((fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) x))
    (∑' (x : α), ENNReal.toReal ((fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) x))
Tactic: lift f to α → ℝ≥0 using ENNReal.ne_top_of_tsum_ne_top hsum
Cleared hypotheses: f, hsum
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
f : (i : α) → ℝ≥0
hsum : Ne (α := ℝ≥0∞) (∑' (x : α), (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) x) ∞
⊢ HasSum (α := ℝ) (fun (x : α) ↦ ENNReal.toReal ((fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) x))
    (∑' (x : α), ENNReal.toReal ((fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) x))
have simp : HasSum f (∑' (a : α), f a)
Tactic: simp only [coe_toReal, ← NNReal.coe_tsum, NNReal.hasSum_coe]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
β : Type u_2
f : β → ℝ≥0
⊢ ∑' (b : β), f b = ENNReal.toNNReal (∑' (b : β), (↑(f b) : ℝ≥0∞))
have pos : ∀ (h : Summable f), ∑' (b : β), f b = ENNReal.toNNReal (∑' (b : β), (↑(f b) : ℝ≥0∞))
Tactic: by_cases h : Summable f
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
β : Type u_2
f : β → ℝ≥0
pos : ∀ (h : Summable f), ∑' (b : β), f b = ENNReal.toNNReal (∑' (b : β), (↑(f b) : ℝ≥0∞))
⊢ ∑' (b : β), f b = ENNReal.toNNReal (∑' (b : β), (↑(f b) : ℝ≥0∞))
have neg : ∀ (h : ¬Summable f), ∑' (b : β), f b = ENNReal.toNNReal (∑' (b : β), (↑(f b) : ℝ≥0∞))
Tactic: by_cases h : Summable f
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
β : Type u_2
f : β → ℝ≥0
h : Summable f
⊢ ∑' (b : β), f b = ENNReal.toNNReal (∑' (b : β), (↑(f b) : ℝ≥0∞))
have pos : ∑' (b : β), f b = (↑(tsum f) : ℝ≥0∞).toNNReal
Tactic: rw [← ENNReal.coe_tsum h, ENNReal.toNNReal_coe]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
β : Type u_2
f : β → ℝ≥0
h : Summable f
pos : ∑' (b : β), f b = (↑(tsum f) : ℝ≥0∞).toNNReal
⊢ ∑' (b : β), f b = ENNReal.toNNReal (∑' (b : β), (↑(f b) : ℝ≥0∞))
have pos₁ : ∑' (b : β), f b = tsum f
Tactic: rw [← ENNReal.coe_tsum h, ENNReal.toNNReal_coe]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (hypothesis)
Goal:
β : Type u_2
f : β → ℝ≥0
h : ¬Summable f
⊢ ∑' (b : β), f b = ENNReal.toNNReal (∑' (b : β), (↑(f b) : ℝ≥0∞))
have A : Eq (α := ℝ≥0) (∑' (b : β), f b) 0
Tactic: have A := tsum_eq_zero_of_not_summable h
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (hypothesis)
Goal:
β : Type u_2
f : β → ℝ≥0
h : ¬Summable f
A : Eq (α := ℝ≥0) (∑' (b : β), f b) 0
⊢ ∑' (b : β), f b = ENNReal.toNNReal (∑' (b : β), (↑(f b) : ℝ≥0∞))
have h₁ : Eq (α := ℝ≥0∞) (∑' (b : β), (↑(f b) : ℝ≥0∞)) ∞
Tactic: simp only [← ENNReal.tsum_coe_ne_top_iff_summable, Classical.not_not] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
β : Type u_2
f g : β → ℝ≥0
r : ℝ≥0
hgf : ∀ (b : β), g b ≤ f b
hfr : HasSum f r
⊢ ∑' (b : β), (↑(g b) : ℝ≥0∞) ≤ (↑r : ℝ≥0∞)
have refine : ∀ (b : β), (↑(g b) : ℝ≥0∞) ≤ (↑(f b) : ℝ≥0∞)
Tactic: refine hasSum_le (fun b => ?_) ENNReal.summable.hasSum (ENNReal.hasSum_coe.2 hfr)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (hypothesis)
Goal:
α : Type u_1
f : α → ℝ≥0
h : Summable f
⊢ (support f).Countable
have h₁ : Summable (α := ℝ) fun (a : α) ↦ (↑(f a) : ℝ)
Tactic: rw [← NNReal.summable_coe] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
f : ℕ → ℝ≥0
r : ℝ≥0
⊢ HasSum f r ↔ Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
have rw : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, (↑(f i) : ℝ≥0∞)) atTop (𝓝 (↑r : ℝ≥0∞)) ↔
  Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
Tactic: rw [← ENNReal.hasSum_coe, ENNReal.hasSum_iff_tendsto_nat]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
f : ℕ → ℝ≥0
r : ℝ≥0
⊢ Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, (↑(f i) : ℝ≥0∞)) atTop (𝓝 (↑r : ℝ≥0∞)) ↔
    Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
have simp : Tendsto (fun (n : ℕ) ↦ (↑(∑ a ∈ Finset.range n, f a) : ℝ≥0∞)) atTop (𝓝 (↑r : ℝ≥0∞)) ↔
  Tendsto (fun (n : ℕ) ↦ ∑ a ∈ Finset.range n, f a) atTop (𝓝 r)
Tactic: simp only [← ENNReal.coe_finsetSum]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
f : ℕ → ℝ≥0
⊢ ¬Summable f ↔ Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop atTop
have mp : ¬Summable f → Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop atTop
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
f : ℕ → ℝ≥0
mp : ¬Summable f → Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop atTop
⊢ ¬Summable f ↔ Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop atTop
have mpr : Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop atTop → ¬Summable f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
f : ℕ → ℝ≥0
h : ¬Summable f
⊢ Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop atTop
have mp : Monotone (β := ℝ≥0) fun (s : Finset ℕ) ↦ ∑ b ∈ s, f b
Tactic: refine ((tendsto_atTop_of_monotone ?_).resolve_right h).comp ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
f : ℕ → ℝ≥0
h : ¬Summable f
mp : Monotone (β := ℝ≥0) fun (s : Finset ℕ) ↦ ∑ b ∈ s, f b
⊢ Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop atTop
have mp₁ : Tendsto Finset.range atTop atTop
Tactic: refine ((tendsto_atTop_of_monotone ?_).resolve_right h).comp ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
f : ℕ → ℝ≥0
⊢ Summable f ↔ ¬Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop atTop
have rw : ¬Summable f ↔ ¬¬Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop atTop
Tactic: rw [← not_iff_not, Classical.not_not, not_summable_iff_tendsto_nat_atTop]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
f : ℕ → ℝ≥0
rw : ¬Summable f ↔ ¬¬Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop atTop
⊢ Summable f ↔ ¬Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop atTop
have rw₁ : ¬Summable f ↔ Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop atTop
Tactic: rw [← not_iff_not, Classical.not_not, not_summable_iff_tendsto_nat_atTop]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
f : ℕ → ℝ≥0
rw : ¬Summable f ↔ ¬¬Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop atTop
rw₁ : ¬Summable f ↔ Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop atTop
⊢ Summable f ↔ ¬Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop atTop
have rw₂ : Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop atTop ↔
  Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop atTop
Tactic: rw [← not_iff_not, Classical.not_not, not_summable_iff_tendsto_nat_atTop]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
f : ℕ → ℝ≥0
c : ℝ≥0
h : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c
⊢ Summable f
have refine : ∀ (H : Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop atTop), False
Tactic: refine summable_iff_not_tendsto_nat_atTop.2 fun H => ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
f : ℕ → ℝ≥0
c : ℝ≥0
h : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c
H : Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop atTop
⊢ False
have rcases : ∀ (n : ℕ) (hn : c < ∑ i ∈ Finset.range n, f i), False
Tactic: rcases exists_lt_of_tendsto_atTop H 0 c with ⟨n, -, hn⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
β : α → Type u_4
f : (x : α) × β x → ℝ≥0
⊢ Summable f ↔
    (∀ (x : α), Summable (α := ℝ≥0) fun (y : β x) ↦ f (Sigma.mk (β := fun (x : α) ↦ β x) x y)) ∧
      Summable (α := ℝ≥0) fun (x : α) ↦ ∑' (y : β x), f (Sigma.mk (β := fun (x : α) ↦ β x) x y)
have mp : Summable f →
  (∀ (x : α), Summable (α := ℝ≥0) fun (y : β x) ↦ f (Sigma.mk (β := fun (x : α) ↦ β x) x y)) ∧
    Summable (α := ℝ≥0) fun (x : α) ↦ ∑' (y : β x), f (Sigma.mk (β := fun (x : α) ↦ β x) x y)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
β : α → Type u_4
f : (x : α) × β x → ℝ≥0
mp :
  Summable f →
    (∀ (x : α), Summable (α := ℝ≥0) fun (y : β x) ↦ f (Sigma.mk (β := fun (x : α) ↦ β x) x y)) ∧
      Summable (α := ℝ≥0) fun (x : α) ↦ ∑' (y : β x), f (Sigma.mk (β := fun (x : α) ↦ β x) x y)
⊢ Summable f ↔
    (∀ (x : α), Summable (α := ℝ≥0) fun (y : β x) ↦ f (Sigma.mk (β := fun (x : α) ↦ β x) x y)) ∧
      Summable (α := ℝ≥0) fun (x : α) ↦ ∑' (y : β x), f (Sigma.mk (β := fun (x : α) ↦ β x) x y)
have mpr : ((∀ (x : α), Summable (α := ℝ≥0) fun (y : β x) ↦ f (Sigma.mk (β := fun (x : α) ↦ β x) x y)) ∧
    Summable (α := ℝ≥0) fun (x : α) ↦ ∑' (y : β x), f (Sigma.mk (β := fun (x : α) ↦ β x) x y)) →
  Summable f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
β : α → Type u_4
f : (x : α) × β x → ℝ≥0
⊢ Summable f →
    (∀ (x : α), Summable (α := ℝ≥0) fun (y : β x) ↦ f (Sigma.mk (β := fun (x : α) ↦ β x) x y)) ∧
      Summable (α := ℝ≥0) fun (x : α) ↦ ∑' (y : β x), f (Sigma.mk (β := fun (x : α) ↦ β x) x y)
have mp : (Summable (α := ℝ) fun (a : (x : α) × β x) ↦ (↑(f a) : ℝ)) →
  (∀ (x : α), Summable (α := ℝ) fun (a : β x) ↦ (↑(f (Sigma.mk (β := fun (x : α) ↦ β x) x a)) : ℝ)) ∧
    Summable (α := ℝ) fun (a : α) ↦ ∑' (a_1 : β a), (↑(f (Sigma.mk (β := fun (x : α) ↦ β x) a a_1)) : ℝ)
Tactic: simp only [← NNReal.summable_coe, NNReal.coe_tsum]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
s : Set α
⊢ Summable (s.indicator f)
have refine : ∀ (a : α), (if a ∈ s then f a else 0) ≤ f a
Tactic: refine NNReal.summable_of_le (fun a => le_trans (le_of_eq (s.indicator_apply f a)) ?_) hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
s : Set α
a : α
⊢ (if a ∈ s then f a else 0) ≤ f a
have pos : a ∈ s → f a ≤ f a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
s : Set α
a : α
pos : a ∈ s → f a ≤ f a
⊢ (if a ∈ s then f a else 0) ≤ f a
have neg : a ∉ s → 0 ≤ f a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
s : Set α
⊢ Summable (s.indicator f)
have refine : ∀ (a : α), (if a ∈ s then f a else 0) ≤ f a
Tactic: classical
  refine NNReal.summable_of_le (fun a => le_trans (le_of_eq (s.indicator_apply f a)) ?_) hf
  split_ifs
  · exact le_refl (f a)
  · exact zero_le_coe
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
s : Set α
refine : ∀ (a : α), (if a ∈ s then f a else 0) ≤ f a
⊢ Summable (s.indicator f)
have pos : ∀ a ∈ s, f a ≤ f a
Tactic: classical
  refine NNReal.summable_of_le (fun a => le_trans (le_of_eq (s.indicator_apply f a)) ?_) hf
  split_ifs
  · exact le_refl (f a)
  · exact zero_le_coe
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
s : Set α
refine : ∀ (a : α), (if a ∈ s then f a else 0) ≤ f a
pos : ∀ a ∈ s, f a ≤ f a
⊢ Summable (s.indicator f)
have neg : ∀ a ∉ s, 0 ≤ f a
Tactic: classical
  refine NNReal.summable_of_le (fun a => le_trans (le_of_eq (s.indicator_apply f a)) ?_) hf
  split_ifs
  · exact le_refl (f a)
  · exact zero_le_coe
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
f : ℕ → ℝ≥0
⊢ Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ∑' (k : ℕ), f (k + i)) atTop (𝓝 0)
have rw : Tendsto (fun (a : ℕ) ↦ (↑(∑' (k : ℕ), f (k + a)) : ℝ)) atTop (𝓝 (↑0 : ℝ))
Tactic: rw [← tendsto_coe]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
f : ℕ → ℝ≥0
⊢ Tendsto (fun (a : ℕ) ↦ (↑(∑' (k : ℕ), f (k + a)) : ℝ)) atTop (𝓝 (↑0 : ℝ))
have h : ∀ (x : ℕ), (↑(∑' (k : ℕ), f (k + x)) : ℝ) = ∑' (k : ℕ), (↑(f (k + x)) : ℝ)
Tactic: convert! _root_.tendsto_sum_nat_add fun i => (f i : ℝ)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
f : ℕ → ℝ≥0
x : ℕ
⊢ (↑(∑' (k : ℕ), f (k + x)) : ℝ) = ∑' (k : ℕ), (↑(f (k + x)) : ℝ)
have h : Eq (α := ℝ≥0) (∑' (k : ℕ), f (k + x)) (∑' (k : ℕ), f (k + x))
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (hypothesis)
Goal:
α : Type u_1
f g : α → ℝ≥0
sf sg : ℝ≥0
i : α
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
hf : HasSum f sf
hg : HasSum g sg
⊢ sf < sg
have A : ∀ (a : α), (↑(f a) : ℝ) ≤ (↑(g a) : ℝ)
Tactic: have A : ∀ a : α, (f a : ℝ) ≤ g a := fun a => NNReal.coe_le_coe.2 (h a)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (hypothesis)
Goal:
α : Type u_1
f g : α → ℝ≥0
sf sg : ℝ≥0
i : α
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
hf : HasSum f sf
hg : HasSum g sg
A : ∀ (a : α), (↑(f a) : ℝ) ≤ (↑(g a) : ℝ)
⊢ sf < sg
have this : (↑sf : ℝ) < (↑sg : ℝ)
Tactic: have : (sf : ℝ) < sg := hasSum_lt A (NNReal.coe_lt_coe.2 hi) (hasSum_coe.2 hf) (hasSum_coe.2 hg)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
i : α
⊢ ∑' (x : α), f x = f i + ∑' (x : α), if x = i then 0 else f x
have refine : ∀ (i' : α), update (β := fun (a : α) ↦ ℝ≥0) f i (0 : ℝ≥0) i' ≤ f i'
Tactic: refine (NNReal.summable_of_le (fun i' => ?_) hf).tsum_eq_add_tsum_ite' i
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
i i' : α
⊢ update (β := fun (a : α) ↦ ℝ≥0) f i (0 : ℝ≥0) i' ≤ f i'
have rw : (if i' = i then 0 else f i') ≤ f i'
Tactic: rw [Function.update_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
i i' : α
⊢ (if i' = i then 0 else f i') ≤ f i'
have pos : i' = i → 0 ≤ f i'
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
i i' : α
pos : i' = i → 0 ≤ f i'
⊢ (if i' = i then 0 else f i') ≤ f i'
have neg : ¬i' = i → f i' ≤ f i'
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
f : ℕ → ℝ≥0∞
hf : Ne (α := ℝ≥0∞) (∑' (i : ℕ), f i) ∞
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ ∑' (k : ℕ), f (k + i)) atTop (𝓝 0)
have lift : ∀ (f : (i : ℕ) → ℝ≥0) (hf : Ne (α := ℝ≥0∞) (∑' (i : ℕ), (fun (i : ℕ) ↦ (↑(f i) : ℝ≥0∞)) i) ∞),
  Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ ∑' (k : ℕ), (fun (i : ℕ) ↦ (↑(f i) : ℝ≥0∞)) (k + i)) atTop (𝓝 0)
Tactic: lift f to ℕ → ℝ≥0 using ENNReal.ne_top_of_tsum_ne_top hf
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (hypothesis)
Goal:
f : (i : ℕ) → ℝ≥0
hf : Ne (α := ℝ≥0∞) (∑' (i : ℕ), (fun (i : ℕ) ↦ (↑(f i) : ℝ≥0∞)) i) ∞
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ ∑' (k : ℕ), (fun (i : ℕ) ↦ (↑(f i) : ℝ≥0∞)) (k + i)) atTop (𝓝 0)
have hf₁ : Summable f
Tactic: replace hf : Summable f := tsum_coe_ne_top_iff_summable.1 hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
f : (i : ℕ) → ℝ≥0
hf : Summable f
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ ∑' (k : ℕ), (fun (i : ℕ) ↦ (↑(f i) : ℝ≥0∞)) (k + i)) atTop (𝓝 0)
have simp : Tendsto (fun (i : ℕ) ↦ (↑(∑' (a : ℕ), f (a + i)) : ℝ≥0∞)) atTop (𝓝 (↑0 : ℝ≥0∞))
Tactic: simp only [← ENNReal.coe_tsum, NNReal.summable_nat_add _ hf, ← ENNReal.coe_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
f g : α → ℝ≥0∞
sf sg : ℝ≥0∞
i : α
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
hsf : sf ≠ ∞
hf : HasSum f sf
hg : HasSum g sg
⊢ sf < sg
have pos : ∀ (hsg : sg = ∞), sf < sg
Tactic: by_cases hsg : sg = ∞
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
f g : α → ℝ≥0∞
sf sg : ℝ≥0∞
i : α
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
hsf : sf ≠ ∞
hf : HasSum f sf
hg : HasSum g sg
pos : ∀ (hsg : sg = ∞), sf < sg
⊢ sf < sg
have neg : ∀ (hsg : ¬sg = ∞), sf < sg
Tactic: by_cases hsg : sg = ∞
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (hypothesis)
Goal:
α : Type u_1
f g : α → ℝ≥0∞
sf sg : ℝ≥0∞
i : α
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
hsf : sf ≠ ∞
hf : HasSum f sf
hg : HasSum g sg
hsg : ¬sg = ∞
⊢ sf < sg
have hg' : ∀ (x : α), g x ≠ ∞
Tactic: have hg' : ∀ x, g x ≠ ∞ := ENNReal.ne_top_of_tsum_ne_top (hg.tsum_eq.symm ▸ hsg)