awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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}
calc : (↑(#(hf.toFinset (s := {i : ι | ε ≤ a i}))) : ℝ≥0∞) * ε = ∑ _i ∈ hf.toFinset (s := {i : ι | ε ≤ a i}), ε
⊢ (↑(#(hf.toFinset (s := {i : ι | ε ≤ a i}))) : ℝ≥0∞) * ε ≤ c

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

Premises used: ENNReal.sum_le_tsum, Set.Finite.toFinset, Finset.sum_le_sum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
β : Type u_2
γ : Type u_3
f : β → ℝ≥0∞
g : β → γ
ha : HasSum (α := ℝ≥0∞) (fun (b : γ) ↦ ∑' (b_1 : (↑(g ⁻¹' {b}) : Type u_2)), f (↑b_1 : β)) (∑' (i : β), f i)
⊢ Eq (α := ℝ≥0∞) (∑' (x : γ) (b : (↑(g ⁻¹' {x}) : Type u_2)), f (↑b : β)) (∑' (i : β), f i)

Tactic:
apply HasSum.tsum_eq

Premises used: HasSum.tsum_eq
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
β : Type u_2
γ : Type u_3
f : β → ℝ≥0∞
g : β → γ
equiv : (y : γ) × { x : β // g x = y } ≃ β := Equiv.sigmaFiberEquiv g
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 : β))
⊢ HasSum (α := ℝ≥0∞) (fun (b : γ) ↦ ∑' (b_1 : (↑(g ⁻¹' {b}) : Type u_2)), f (↑b_1 : β)) (∑' (i : β), f i)

Tactic:
apply (equiv.hasSum_iff.mpr ENNReal.summable.hasSum).sigma

Premises used: Iff.mpr, Equiv.hasSum_iff, ENNReal.summable, HasSum.sigma, Summable.hasSum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
β : Type u_2
γ : Type u_3
f : β → ℝ≥0∞
g : β → γ
equiv : (y : γ) × { x : β // g x = y } ≃ β := Equiv.sigmaFiberEquiv g
⊢ ∀ (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:
fun _ ↦ ENNReal.summable.hasSum_iff.mpr rfl

Premises used: Iff.mpr, ENNReal.summable, Summable.hasSum_iff, rfl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
β : Type u_2
γ : Type u_3
f : β → ℝ≥0∞
g : β → γ
equiv : (y : γ) × { x : β // g x = y } ≃ β := Equiv.sigmaFiberEquiv g
⊢ ∀ (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:
exact fun _ ↦ ENNReal.summable.hasSum_iff.mpr rfl

Premises used: Iff.mpr, ENNReal.summable, Summable.hasSum_iff, rfl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0
rw : Ne (α := ℝ≥0∞) (∑' (a : α), (↑(f a) : ℝ≥0∞)) ∞ ↔ Summable f
⊢ Ne (α := ℝ≥0∞) (∑' (a : α), (↑(f a) : ℝ≥0∞)) ∞ ↔ Summable (α := ℝ) fun (a : α) ↦ (↑(f a) : ℝ)

Tactic:
rw [NNReal.summable_coe]

Premises used: NNReal.summable_coe
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0
⊢ Ne (α := ℝ≥0∞) (∑' (a : α), (↑(f a) : ℝ≥0∞)) ∞ ↔ Summable f

Tactic:
tsum_coe_ne_top_iff_summable

Premises used: ENNReal.tsum_coe_ne_top_iff_summable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0
⊢ Ne (α := ℝ≥0∞) (∑' (a : α), (↑(f a) : ℝ≥0∞)) ∞ ↔ Summable f

Tactic:
exact tsum_coe_ne_top_iff_summable

Premises used: ENNReal.tsum_coe_ne_top_iff_summable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0
⊢ Eq (α := ℝ≥0∞) (∑' (a : α), (↑(f a) : ℝ≥0∞)) ∞ ↔ ¬Summable (α := ℝ) fun (a : α) ↦ (↑(f a) : ℝ)

Tactic:
tsum_coe_ne_top_iff_summable_coe.not_right

Premises used: ENNReal.tsum_coe_ne_top_iff_summable_coe, Iff.not_right
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0∞
hsum : Ne (α := ℝ≥0∞) (∑' (x : α), f x) ∞
⊢ ∀ (i : α), f i ≠ ∞

Tactic:
ENNReal.ne_top_of_tsum_ne_top hsum

Premises used: ENNReal.ne_top_of_tsum_ne_top
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0∞
hsum : Ne (α := ℝ≥0∞) (∑' (x : α), f x) ∞
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))
⊢ HasSum (α := ℝ) (fun (x : α) ↦ (f x).toReal) (∑' (x : α), (f x).toReal)

Tactic:
lift f to α → ℝ≥0 using ENNReal.ne_top_of_tsum_ne_top hsum

Premises used: ENNReal.ne_top_of_tsum_ne_top
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : (i : α) → ℝ≥0
hsum : Ne (α := ℝ≥0∞) (∑' (x : α), (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) x) ∞
simp : HasSum f (∑' (a : α), f a)
⊢ HasSum (α := ℝ) (fun (x : α) ↦ ENNReal.toReal ((fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) x))
    (∑' (x : α), ENNReal.toReal ((fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) x))

Tactic:
simp only [coe_toReal, ← NNReal.coe_tsum, NNReal.hasSum_coe]

Premises used: ENNReal.coe_toReal, NNReal.hasSum_coe, NNReal.coe_tsum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : (i : α) → ℝ≥0
hsum : Ne (α := ℝ≥0∞) (∑' (x : α), (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) x) ∞
⊢ HasSum f (∑' (a : α), f a)

Tactic:
(tsum_coe_ne_top_iff_summable.1 hsum).hasSum

Premises used: Summable.hasSum, ENNReal.tsum_coe_ne_top_iff_summable, Iff.mp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : (i : α) → ℝ≥0
hsum : Ne (α := ℝ≥0∞) (∑' (x : α), (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) x) ∞
⊢ HasSum f (∑' (a : α), f a)

Tactic:
exact (tsum_coe_ne_top_iff_summable.1 hsum).hasSum

Premises used: Summable.hasSum, ENNReal.tsum_coe_ne_top_iff_summable, Iff.mp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0∞
hsum : Ne (α := ℝ≥0∞) (∑' (x : α), f x) ∞
⊢ Summable (α := ℝ) fun (x : α) ↦ (f x).toReal

Tactic:
(hasSum_toReal hsum).summable

Premises used: ENNReal.hasSum_toReal, HasSum.summable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
β : Type u_2
f : β → ℝ≥0
pos : ∀ (h : Summable f), ∑' (b : β), f b = ENNReal.toNNReal (∑' (b : β), (↑(f b) : ℝ≥0∞))
neg : ∀ (h : ¬Summable f), ∑' (b : β), f b = ENNReal.toNNReal (∑' (b : β), (↑(f b) : ℝ≥0∞))
⊢ ∑' (b : β), f b = ENNReal.toNNReal (∑' (b : β), (↑(f b) : ℝ≥0∞))

Tactic:
by_cases h : Summable f

Premises used: Summable, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
β : Type u_2
f : β → ℝ≥0
h : Summable f
pos : ∑' (b : β), f b = (↑(tsum f) : ℝ≥0∞).toNNReal
pos₁ pos₂ : ∑' (b : β), f b = tsum f
⊢ ∑' (b : β), f b = ENNReal.toNNReal (∑' (b : β), (↑(f b) : ℝ≥0∞))

Tactic:
rw [← ENNReal.coe_tsum h, ENNReal.toNNReal_coe]

Premises used: ENNReal.toNNReal_coe, ENNReal.coe_tsum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
β : Type u_2
f : β → ℝ≥0
h : ¬Summable f
⊢ Eq (α := ℝ≥0) (∑' (b : β), f b) 0

Tactic:
have A := tsum_eq_zero_of_not_summable h
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
β : Type u_2
f : β → ℝ≥0
h : ¬Summable f
A : Eq (α := ℝ≥0) (∑' (b : β), f b) 0
⊢ Eq (α := ℝ≥0∞) (∑' (b : β), (↑(f b) : ℝ≥0∞)) ∞

Tactic:
simp only [← ENNReal.tsum_coe_ne_top_iff_summable, Classical.not_not] at h

Premises used: Classical.not_not, ENNReal.tsum_coe_ne_top_iff_summable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
β : Type u_2
f : β → ℝ≥0
A : Eq (α := ℝ≥0) (∑' (b : β), f b) 0
h : Eq (α := ℝ≥0∞) (∑' (b : β), (↑(f b) : ℝ≥0∞)) ∞
⊢ ∑' (b : β), f b = ENNReal.toNNReal (∑' (b : β), (↑(f b) : ℝ≥0∞))

Tactic:
simp only [h, ENNReal.toNNReal_top, A]

Premises used: ENNReal.toNNReal_top
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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∞)

Tactic:
hasSum_le (fun b => ?_) ENNReal.summable.hasSum (ENNReal.hasSum_coe.2 hfr)

Premises used: Iff.mpr, hasSum_le, ENNReal.summable, Summable.hasSum, ENNReal.hasSum_coe
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
β : Type u_2
f g : β → ℝ≥0
r : ℝ≥0
hgf : ∀ (b : β), g b ≤ f b
hfr : HasSum f r
refine : ∀ (b : β), (↑(g b) : ℝ≥0∞) ≤ (↑(f b) : ℝ≥0∞)
⊢ ∑' (b : β), (↑(g b) : ℝ≥0∞) ≤ (↑r : ℝ≥0∞)

Tactic:
refine hasSum_le (fun b => ?_) ENNReal.summable.hasSum (ENNReal.hasSum_coe.2 hfr)

Premises used: Iff.mpr, hasSum_le, ENNReal.summable, Summable.hasSum, ENNReal.hasSum_coe
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
β : Type u_2
f g : β → ℝ≥0
r : ℝ≥0
hgf : ∀ (b : β), g b ≤ f b
hfr : HasSum f r
b : β
⊢ (↑(g b) : ℝ≥0∞) ≤ (↑(f b) : ℝ≥0∞)

Tactic:
ENNReal.coe_le_coe.2 (hgf _)

Premises used: Iff.mpr, ENNReal.coe_le_coe
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
β : Type u_2
f g : β → ℝ≥0
r : ℝ≥0
hgf : ∀ (b : β), g b ≤ f b
hfr : HasSum f r
b : β
⊢ (↑(g b) : ℝ≥0∞) ≤ (↑(f b) : ℝ≥0∞)

Tactic:
exact ENNReal.coe_le_coe.2 (hgf _)

Premises used: Iff.mpr, ENNReal.coe_le_coe
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0
h : Summable f
⊢ Summable (α := ℝ) fun (a : α) ↦ (↑(f a) : ℝ)

Tactic:
rw [← NNReal.summable_coe] at h

Premises used: NNReal.summable_coe
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0
h : Summable (α := ℝ) fun (a : α) ↦ (↑(f a) : ℝ)
⊢ (support f).Countable

Tactic:
simpa [support] using h.countable_support

Premises used: Function.support, Summable.countable_support
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0
r : ℝ≥0
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)
⊢ HasSum f r ↔ Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)

Tactic:
rw [← ENNReal.hasSum_coe, ENNReal.hasSum_iff_tendsto_nat]

Premises used: ENNReal.hasSum_iff_tendsto_nat, ENNReal.hasSum_coe
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0
r : ℝ≥0
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)
⊢ 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:
simp only [← ENNReal.coe_finsetSum]

Premises used: ENNReal.coe_finsetSum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0
r : ℝ≥0
⊢ 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:
ENNReal.tendsto_coe

Premises used: ENNReal.tendsto_coe
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0
r : ℝ≥0
⊢ 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:
exact ENNReal.tendsto_coe

Premises used: ENNReal.tendsto_coe
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0
mp : ¬Summable f → Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop atTop
mpr : Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop atTop → ¬Summable f
⊢ ¬Summable f ↔ Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop atTop

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0
h : ¬Summable f
⊢ Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop atTop

Tactic:
((tendsto_atTop_of_monotone ?_).resolve_right h).comp ?_

Premises used: Multiset.sum, Multiset.foldr, Or.resolve_right, Filter.Tendsto.comp, tendsto_atTop_of_monotone, Finset.sum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0
h : ¬Summable f
mp : Monotone (β := ℝ≥0) fun (s : Finset ℕ) ↦ ∑ b ∈ s, f b
mp₁ : Tendsto Finset.range atTop atTop
⊢ Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop atTop

Tactic:
refine ((tendsto_atTop_of_monotone ?_).resolve_right h).comp ?_

Premises used: Or.resolve_right, Filter.Tendsto.comp, tendsto_atTop_of_monotone
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0
h : ¬Summable f
⊢ Monotone (β := ℝ≥0) fun (s : Finset ℕ) ↦ ∑ b ∈ s, f b

Tactic:
Finset.sum_mono_set _

Premises used: Finset.sum_mono_set
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0
h : ¬Summable f
⊢ Tendsto Finset.range atTop atTop

Tactic:
tendsto_finset_range

Premises used: Filter.tendsto_finset_range
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0
h : ¬Summable f
⊢ Monotone (β := ℝ≥0) fun (s : Finset ℕ) ↦ ∑ b ∈ s, f b

Tactic:
exacts [Finset.sum_mono_set _, tendsto_finset_range]

Premises used: Finset.sum_mono_set, Filter.tendsto_finset_range
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0
hnat : Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop atTop
r : ℝ≥0
hr : HasSum f r
⊢ False

Tactic:
not_tendsto_nhds_of_tendsto_atTop hnat _ (hasSum_iff_tendsto_nat.1 hr)

Premises used: not_tendsto_nhds_of_tendsto_atTop, NNReal.hasSum_iff_tendsto_nat, Iff.mp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0
hnat : Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop atTop
r : ℝ≥0
hr : HasSum f r
⊢ False

Tactic:
exact not_tendsto_nhds_of_tendsto_atTop hnat _ (hasSum_iff_tendsto_nat.1 hr)

Premises used: not_tendsto_nhds_of_tendsto_atTop, NNReal.hasSum_iff_tendsto_nat, Iff.mp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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
rw₂ 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
⊢ 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]

Premises used: not_iff_not, NNReal.not_summable_iff_tendsto_nat_atTop, Classical.not_not
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0
c : ℝ≥0
h : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c
⊢ Summable f

Tactic:
summable_iff_not_tendsto_nat_atTop.2 fun H => ?_

Premises used: Iff.mpr, NNReal.summable_iff_not_tendsto_nat_atTop
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0
c : ℝ≥0
h : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c
refine : ∀ (H : Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop atTop), False
⊢ Summable f

Tactic:
refine summable_iff_not_tendsto_nat_atTop.2 fun H => ?_

Premises used: Iff.mpr, NNReal.summable_iff_not_tendsto_nat_atTop
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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
rcases : ∀ (n : ℕ) (hn : c < ∑ i ∈ Finset.range n, f i), False
⊢ False

Tactic:
rcases exists_lt_of_tendsto_atTop H 0 c with ⟨n, -, hn⟩

Premises used: Filter.exists_lt_of_tendsto_atTop, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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
n : ℕ
hn : c < ∑ i ∈ Finset.range n, f i
⊢ False

Tactic:
lt_irrefl _ (hn.trans_le (h n))

Premises used: lt_irrefl, LT.lt.trans_le
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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
n : ℕ
hn : c < ∑ i ∈ Finset.range n, f i
⊢ False

Tactic:
exact lt_irrefl _ (hn.trans_le (h n))

Premises used: lt_irrefl, LT.lt.trans_le
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0
c : ℝ≥0
h : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c
⊢ ∑' (n : ℕ), f n ≤ c

Tactic:
(summable_of_sum_range_le h).tsum_le_of_sum_range_le h

Premises used: NNReal.summable_of_sum_range_le, Summable.tsum_le_of_sum_range_le
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
β : Type u_4
f : α → ℝ≥0
hf : Summable f
i : β → α
hi : Injective i
⊢ LE.le (α := ℝ≥0) (∑' (x : β), f (i x)) (∑' (x : α), f x)

Tactic:
(summable_comp_injective hf hi).tsum_le_tsum_of_inj i hi (fun _ _ => zero_le) (fun _ => le_rfl)
    hf

Premises used: zero_le, le_rfl, NNReal.summable_comp_injective, Summable.tsum_le_tsum_of_inj
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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)
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
⊢ 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
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
β : α → Type u_4
f : (x : α) × β x → ℝ≥0
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)) : ℝ)
⊢ 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:
simp only [← NNReal.summable_coe, NNReal.coe_tsum]

Premises used: NNReal.summable_coe, NNReal.coe_tsum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
β : α → Type u_4
f : (x : α) × β x → ℝ≥0
⊢ (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:
fun h => ⟨h.sigma_factor, h.sigma⟩

Premises used: Summable.sigma, Summable.sigma_factor, And.intro
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
β : α → Type u_4
f : (x : α) × β x → ℝ≥0
⊢ (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:
exact fun h => ⟨h.sigma_factor, h.sigma⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
β : α → Type u_4
f : (x : α) × β x → ℝ≥0
h₁ : ∀ (x : α), Summable (α := ℝ≥0) fun (y : β x) ↦ f (Sigma.mk (β := fun (x : α) ↦ β x) x y)
h₂ : Summable (α := ℝ≥0) fun (x : α) ↦ ∑' (y : β x), f (Sigma.mk (β := fun (x : α) ↦ β x) x y)
⊢ Summable f

Tactic:
simpa only [← ENNReal.tsum_coe_ne_top_iff_summable, ENNReal.tsum_sigma',
      ENNReal.coe_tsum (h₁ _)] using h₂

Premises used: ENNReal.coe_tsum, ENNReal.tsum_sigma', ENNReal.tsum_coe_ne_top_iff_summable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
s : Set α
⊢ Summable (s.indicator f)

Tactic:
NNReal.summable_of_le (fun a => le_trans (le_of_eq (s.indicator_apply f a)) ?_) hf

Premises used: Set.indicator_apply, NNReal.summable_of_le, le_of_eq, le_trans
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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)

Tactic:
refine NNReal.summable_of_le (fun a => le_trans (le_of_eq (s.indicator_apply f a)) ?_) hf

Premises used: Set.indicator_apply, NNReal.summable_of_le, le_of_eq, le_trans
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
s : Set α
a : α
pos : a ∈ s → f a ≤ f a
neg : a ∉ s → 0 ≤ f a
⊢ (if a ∈ s then f a else 0) ≤ f a

Tactic:
split_ifs
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
s : Set α
a : α
h : a ∈ s
⊢ f a ≤ f a

Tactic:
le_refl (f a)

Premises used: le_refl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
s : Set α
a : α
h : a ∈ s
⊢ f a ≤ f a

Tactic:
exact le_refl (f a)

Premises used: le_refl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
s : Set α
a : α
h : a ∉ s
⊢ 0 ≤ f a

Tactic:
zero_le_coe

Premises used: NNReal.zero_le_coe, NNReal.toReal
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
s : Set α
a : α
h : a ∉ s
⊢ 0 ≤ f a

Tactic:
exact zero_le_coe

Premises used: NNReal.zero_le_coe
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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
neg neg₁ : ∀ a ∉ s, 0 ≤ f a
⊢ Summable (s.indicator f)

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

Premises used: NNReal.zero_le_coe
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
s : Set α
h : ∃ a ∈ s, f a ≠ 0
⊢ Ne (α := ℝ≥0) (∑' (x : α), s.indicator f x) 0

Tactic:
fun h' =>
  let ⟨a, ha, hap⟩ := h
  hap ((Set.indicator_apply_eq_self.mpr (absurd ha)).symm.trans
    ((indicator_summable hf s).tsum_eq_zero_iff.1 h' a))

Premises used: Iff.mpr, False, absurd, Set.indicator_apply_eq_self, NNReal.indicator_summable, Iff.mp, _private.0.NNReal.tsum_indicator_ne_zero.match_1, Summable.tsum_eq_zero_iff, Eq.symm, Not, Eq.trans
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0
rw : Tendsto (fun (a : ℕ) ↦ (↑(∑' (k : ℕ), f (k + a)) : ℝ)) atTop (𝓝 (↑0 : ℝ))
⊢ Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ∑' (k : ℕ), f (k + i)) atTop (𝓝 0)

Tactic:
rw [← tendsto_coe]

Premises used: NNReal.tendsto_coe
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0
⊢ Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∑' (k : ℕ), (↑(f (k + i)) : ℝ)) atTop (𝓝 0)

Tactic:
_root_.tendsto_sum_nat_add fun i => (f i : ℝ)

Premises used: tendsto_sum_nat_add, NNReal.toReal
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0
h : ∀ (x : ℕ), (↑(∑' (k : ℕ), f (k + x)) : ℝ) = ∑' (k : ℕ), (↑(f (k + x)) : ℝ)
⊢ Tendsto (fun (a : ℕ) ↦ (↑(∑' (k : ℕ), f (k + a)) : ℝ)) atTop (𝓝 (↑0 : ℝ))

Tactic:
convert! _root_.tendsto_sum_nat_add fun i => (f i : ℝ)

Premises used: tendsto_sum_nat_add, NNReal.toReal
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0
x : ℕ
h h₁ h₂ h₃ : Eq (α := ℝ≥0) (∑' (k : ℕ), f (k + x)) (∑' (k : ℕ), f (k + x))
⊢ (↑(∑' (k : ℕ), f (k + x)) : ℝ) = ∑' (k : ℕ), (↑(f (k + x)) : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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 : α), (↑(f a) : ℝ) ≤ (↑(g a) : ℝ)

Tactic:
have A : ∀ a : α, (f a : ℝ) ≤ g a := fun a => NNReal.coe_le_coe.2 (h a)