awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ∀ (a : α), (↑(f a) : ℝ) ≤ (↑(g a) : ℝ)
⊢ (↑sf : ℝ) < (↑sg : ℝ)

Tactic:
have : (sf : ℝ) < sg := hasSum_lt A (NNReal.coe_lt_coe.2 hi) (hasSum_coe.2 hf) (hasSum_coe.2 hg)
-- 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 : ∀ (a : α), (↑(f a) : ℝ) ≤ (↑(g a) : ℝ)
this : (↑sf : ℝ) < (↑sg : ℝ)
⊢ sf < sg

Tactic:
NNReal.coe_lt_coe.1 this

Premises used: Iff.mp, NNReal.coe_lt_coe
-- 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 : ∀ (a : α), (↑(f a) : ℝ) ≤ (↑(g a) : ℝ)
this : (↑sf : ℝ) < (↑sg : ℝ)
⊢ sf < sg

Tactic:
exact NNReal.coe_lt_coe.1 this

Premises used: Iff.mp, NNReal.coe_lt_coe
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f g : α → ℝ≥0
sf sg : ℝ≥0
hf : HasSum f sf
hg : HasSum g sg
h : f < g
⊢ sf < sg

Tactic:
let ⟨hle, _i, hi⟩ := Pi.lt_def.mp h
  hasSum_lt hle hi hf hg

Premises used: NNReal.hasSum_lt, Pi.lt_def, _private.0.NNReal.hasSum_strict_mono.match_1, LT.lt, Iff.mp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f g : α → ℝ≥0
i : α
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
hg : Summable g
⊢ LT.lt (α := ℝ≥0) (∑' (n : α), f n) (∑' (n : α), g n)

Tactic:
hasSum_lt h hi (summable_of_le h hg).hasSum hg.hasSum

Premises used: NNReal.hasSum_lt, Summable.hasSum, NNReal.summable_of_le
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f g : α → ℝ≥0
hg : Summable g
h : f < g
⊢ LT.lt (α := ℝ≥0) (∑' (n : α), f n) (∑' (n : α), g n)

Tactic:
let ⟨hle, _i, hi⟩ := Pi.lt_def.mp h
  tsum_lt_tsum hle hi hg

Premises used: Pi.lt_def, NNReal.tsum_lt_tsum, tsum, _private.0.NNReal.hasSum_strict_mono.match_1, LT.lt, Iff.mp, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
g : α → ℝ≥0
hg : Summable g
i : α
hi : 0 < g i
⊢ LT.lt (α := ℝ≥0) 0 (∑' (b : α), g b)

Tactic:
simpa using tsum_lt_tsum (fun a => zero_le) hi hg

Premises used: zero_le, NNReal.tsum_lt_tsum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
i : α
⊢ ∑' (x : α), f x = f i + ∑' (x : α), if x = i then 0 else f x

Tactic:
(NNReal.summable_of_le (fun i' => ?_) hf).tsum_eq_add_tsum_ite' i

Premises used: Summable.tsum_eq_add_tsum_ite', NNReal.summable_of_le
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
i : α
refine : ∀ (i' : α), update (β := fun (a : α) ↦ ℝ≥0) f i (0 : ℝ≥0) i' ≤ f i'
⊢ ∑' (x : α), f x = f i + ∑' (x : α), if x = i then 0 else f x

Tactic:
refine (NNReal.summable_of_le (fun i' => ?_) hf).tsum_eq_add_tsum_ite' i

Premises used: Summable.tsum_eq_add_tsum_ite', NNReal.summable_of_le
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
i i' : α
rw : (if i' = i then 0 else f i') ≤ f i'
⊢ update (β := fun (a : α) ↦ ℝ≥0) f i (0 : ℝ≥0) i' ≤ f i'

Tactic:
rw [Function.update_apply]

Premises used: Function.update_apply
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
i i' : α
pos : i' = i → 0 ≤ f i'
neg : ¬i' = i → f i' ≤ f i'
⊢ (if i' = i then 0 else f i') ≤ f i'

Tactic:
split_ifs
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
i i' : α
h : i' = i
⊢ 0 ≤ f i'

Tactic:
simp only [zero_le', le_rfl]

Premises used: le_rfl, zero_le'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
i i' : α
h : ¬i' = i
⊢ f i' ≤ f i'

Tactic:
simp only [zero_le', le_rfl]

Premises used: le_rfl, zero_le'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0∞
hf : ∀ (a : α), f a ≠ ∞
⊢ ENNReal.toNNReal (∑' (a : α), f a) = ∑' (a : α), (f a).toNNReal

Tactic:
(congr_arg ENNReal.toNNReal (tsum_congr fun x => (coe_toNNReal (hf x)).symm)).trans
    NNReal.tsum_eq_toNNReal_tsum.symm

Premises used: ENNReal.coe_toNNReal, tsum_congr, ENNReal.toNNReal, congr_arg, NNReal.tsum_eq_toNNReal_tsum, Eq.symm, Eq.trans
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0∞
hf : ∀ (a : α), f a ≠ ∞
⊢ ENNReal.toReal (∑' (a : α), f a) = ∑' (a : α), (f a).toReal

Tactic:
simp only [ENNReal.toReal, tsum_toNNReal_eq hf, NNReal.coe_tsum]

Premises used: ENNReal.tsum_toNNReal_eq, ENNReal.toReal, NNReal.coe_tsum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0∞
hf : Ne (α := ℝ≥0∞) (∑' (i : ℕ), f i) ∞
⊢ ∀ (i : ℕ), f i ≠ ∞

Tactic:
ENNReal.ne_top_of_tsum_ne_top hf

Premises used: ENNReal.ne_top_of_tsum_ne_top
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0∞
hf : Ne (α := ℝ≥0∞) (∑' (i : ℕ), f i) ∞
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)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ ∑' (k : ℕ), f (k + i)) atTop (𝓝 0)

Tactic:
lift f to ℕ → ℝ≥0 using ENNReal.ne_top_of_tsum_ne_top hf

Premises used: ENNReal.ne_top_of_tsum_ne_top
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : (i : ℕ) → ℝ≥0
hf : Ne (α := ℝ≥0∞) (∑' (i : ℕ), (fun (i : ℕ) ↦ (↑(f i) : ℝ≥0∞)) i) ∞
⊢ Summable f

Tactic:
replace hf : Summable f := tsum_coe_ne_top_iff_summable.1 hf
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : (i : ℕ) → ℝ≥0
hf : Summable f
simp : Tendsto (fun (i : ℕ) ↦ (↑(∑' (a : ℕ), f (a + i)) : ℝ≥0∞)) atTop (𝓝 (↑0 : ℝ≥0∞))
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ ∑' (k : ℕ), (fun (i : ℕ) ↦ (↑(f i) : ℝ≥0∞)) (k + i)) atTop (𝓝 0)

Tactic:
simp only [← ENNReal.coe_tsum, NNReal.summable_nat_add _ hf, ← ENNReal.coe_zero]

Premises used: ENNReal.coe_tsum, NNReal.summable_nat_add, ENNReal.coe_zero
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : (i : ℕ) → ℝ≥0
hf : Summable f
⊢ Tendsto (fun (i : ℕ) ↦ (↑(∑' (a : ℕ), f (a + i)) : ℝ≥0∞)) atTop (𝓝 (↑0 : ℝ≥0∞))

Tactic:
mod_cast NNReal.tendsto_sum_nat_add f

Premises used: ENNReal.ofNNReal, ENNReal.tendsto_coe._simp_1, congrArg, cast, nhds, NNReal.tendsto_sum_nat_add, Filter.atTop, HAdd.hAdd, Filter.Tendsto, tsum, Nat, Nat.cast_zero, Eq.symm, SummationFilter.unconditional, Eq.trans
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : (i : ℕ) → ℝ≥0
hf : Summable f
⊢ Tendsto (fun (i : ℕ) ↦ (↑(∑' (a : ℕ), f (a + i)) : ℝ≥0∞)) atTop (𝓝 (↑0 : ℝ≥0∞))

Tactic:
exact mod_cast NNReal.tendsto_sum_nat_add f

Premises used: NNReal.tendsto_sum_nat_add
-- 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:
ENNReal.summable.tsum_le_of_sum_range_le h

Premises used: ENNReal.summable, Summable.tsum_le_of_sum_range_le
-- 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
hsf : sf ≠ ∞
hf : HasSum f sf
hg : HasSum g sg
pos : ∀ (hsg : sg = ∞), sf < sg
neg : ∀ (hsg : ¬sg = ∞), sf < sg
⊢ sf < sg

Tactic:
by_cases hsg : sg = ∞
-- 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
hsf : sf ≠ ∞
hf : HasSum f sf
hg : HasSum g sg
hsg : sg = ∞
⊢ sf < sg

Tactic:
hsg.symm ▸ lt_of_le_of_ne le_top hsf

Premises used: Eq.rec, le_top, Eq.symm, lt_of_le_of_ne
-- 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
hsf : sf ≠ ∞
hf : HasSum f sf
hg : HasSum g sg
hsg : sg = ∞
⊢ sf < sg

Tactic:
exact hsg.symm ▸ lt_of_le_of_ne le_top hsf
-- 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
hsf : sf ≠ ∞
hf : HasSum f sf
hg : HasSum g sg
hsg : ¬sg = ∞
⊢ ∀ (x : α), g x ≠ ∞

Tactic:
have hg' : ∀ x, g x ≠ ∞ := ENNReal.ne_top_of_tsum_ne_top (hg.tsum_eq.symm ▸ hsg)
-- 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
hsf : sf ≠ ∞
hf : HasSum f sf
hg : HasSum g sg
hsg : ¬sg = ∞
hg' : ∀ (x : α), g x ≠ ∞
⊢ ∀ (i : α), f i ≠ ∞

Tactic:
fun x =>
      ne_of_lt (lt_of_le_of_lt (h x) <| lt_of_le_of_ne le_top (hg' x))

Premises used: lt_of_le_of_lt, le_top, ne_of_lt, lt_of_le_of_ne
-- 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
hsf : sf ≠ ∞
hf : HasSum f sf
hg : HasSum g sg
hsg : ¬sg = ∞
hg' : ∀ (x : α), g x ≠ ∞
neg :
  ∀ (f : (i : α) → ℝ≥0) (h : ∀ (a : α), (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) a ≤ g a)
    (hi : (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) i < g i) (hf : HasSum (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) sf), sf < sg
⊢ sf < sg

Tactic:
lift f to α → ℝ≥0 using fun x =>
      ne_of_lt (lt_of_le_of_lt (h x) <| lt_of_le_of_ne le_top (hg' x))

Premises used: lt_of_le_of_lt, le_top, ne_of_lt, lt_of_le_of_ne
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
g : α → ℝ≥0∞
sf sg : ℝ≥0∞
i : α
hsf : sf ≠ ∞
hg : HasSum g sg
hsg : ¬sg = ∞
hg' : ∀ (x : α), g x ≠ ∞
f : (i : α) → ℝ≥0
h : ∀ (a : α), (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) a ≤ g a
hi : (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) i < g i
hf : HasSum (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) sf
⊢ ∀ (i : α), g i ≠ ∞

Tactic:
hg'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
g : α → ℝ≥0∞
sf sg : ℝ≥0∞
i : α
hsf : sf ≠ ∞
hg : HasSum g sg
hsg : ¬sg = ∞
hg' : ∀ (x : α), g x ≠ ∞
f : (i : α) → ℝ≥0
h : ∀ (a : α), (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) a ≤ g a
hi : (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) i < g i
hf : HasSum (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) sf
neg :
  ∀ (g : (i : α) → ℝ≥0) (hg : HasSum (fun (i : α) ↦ (↑(g i) : ℝ≥0∞)) sg)
    (h : ∀ (a : α), LE.le (α := ℝ≥0∞) ((fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) a) ((fun (i : α) ↦ (↑(g i) : ℝ≥0∞)) a))
    (hi : LT.lt (α := ℝ≥0∞) ((fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) i) ((fun (i : α) ↦ (↑(g i) : ℝ≥0∞)) i)), sf < sg
⊢ sf < sg

Tactic:
lift g to α → ℝ≥0 using hg'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
sf sg : ℝ≥0∞
i : α
hsf : sf ≠ ∞
hsg : ¬sg = ∞
f : (i : α) → ℝ≥0
hf : HasSum (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) sf
g : (i : α) → ℝ≥0
hg : HasSum (fun (i : α) ↦ (↑(g i) : ℝ≥0∞)) sg
h : ∀ (a : α), LE.le (α := ℝ≥0∞) ((fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) a) ((fun (i : α) ↦ (↑(g i) : ℝ≥0∞)) a)
hi : LT.lt (α := ℝ≥0∞) ((fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) i) ((fun (i : α) ↦ (↑(g i) : ℝ≥0∞)) i)
⊢ sf ≠ ∞

Tactic:
hsf
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
sf sg : ℝ≥0∞
i : α
hsf : sf ≠ ∞
hsg : ¬sg = ∞
f : (i : α) → ℝ≥0
hf : HasSum (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) sf
g : (i : α) → ℝ≥0
hg : HasSum (fun (i : α) ↦ (↑(g i) : ℝ≥0∞)) sg
h : ∀ (a : α), LE.le (α := ℝ≥0∞) ((fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) a) ((fun (i : α) ↦ (↑(g i) : ℝ≥0∞)) a)
hi : LT.lt (α := ℝ≥0∞) ((fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) i) ((fun (i : α) ↦ (↑(g i) : ℝ≥0∞)) i)
neg : ∀ (sf : ℝ≥0) (hf : HasSum (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) (↑sf : ℝ≥0∞)), (↑sf : ℝ≥0∞) < sg
⊢ sf < sg

Tactic:
lift sf to ℝ≥0 using hsf
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
sg : ℝ≥0∞
i : α
hsg : ¬sg = ∞
f g : (i : α) → ℝ≥0
hg : HasSum (fun (i : α) ↦ (↑(g i) : ℝ≥0∞)) sg
h : ∀ (a : α), LE.le (α := ℝ≥0∞) ((fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) a) ((fun (i : α) ↦ (↑(g i) : ℝ≥0∞)) a)
hi : LT.lt (α := ℝ≥0∞) ((fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) i) ((fun (i : α) ↦ (↑(g i) : ℝ≥0∞)) i)
sf : ℝ≥0
hf : HasSum (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) (↑sf : ℝ≥0∞)
⊢ sg ≠ ∞

Tactic:
hsg
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
sg : ℝ≥0∞
i : α
hsg : ¬sg = ∞
f g : (i : α) → ℝ≥0
hg : HasSum (fun (i : α) ↦ (↑(g i) : ℝ≥0∞)) sg
h : ∀ (a : α), LE.le (α := ℝ≥0∞) ((fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) a) ((fun (i : α) ↦ (↑(g i) : ℝ≥0∞)) a)
hi : LT.lt (α := ℝ≥0∞) ((fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) i) ((fun (i : α) ↦ (↑(g i) : ℝ≥0∞)) i)
sf : ℝ≥0
hf : HasSum (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) (↑sf : ℝ≥0∞)
neg : ∀ (sg : ℝ≥0) (hg : HasSum (fun (i : α) ↦ (↑(g i) : ℝ≥0∞)) (↑sg : ℝ≥0∞)), (↑sf : ℝ≥0∞) < (↑sg : ℝ≥0∞)
⊢ (↑sf : ℝ≥0∞) < sg

Tactic:
lift sg to ℝ≥0 using hsg
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
i : α
f g : (i : α) → ℝ≥0
h : ∀ (a : α), LE.le (α := ℝ≥0∞) ((fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) a) ((fun (i : α) ↦ (↑(g i) : ℝ≥0∞)) a)
hi : LT.lt (α := ℝ≥0∞) ((fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) i) ((fun (i : α) ↦ (↑(g i) : ℝ≥0∞)) i)
sf : ℝ≥0
hf : HasSum (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) (↑sf : ℝ≥0∞)
sg : ℝ≥0
hg : HasSum (fun (i : α) ↦ (↑(g i) : ℝ≥0∞)) (↑sg : ℝ≥0∞)
neg : ∀ (h : ∀ (a : α), f a ≤ g a) (hi : f i < g i), sf < sg
⊢ (↑sf : ℝ≥0∞) < (↑sg : ℝ≥0∞)

Tactic:
simp only [coe_le_coe, coe_lt_coe] at h hi ⊢

Premises used: ENNReal.coe_lt_coe, ENNReal.coe_le_coe
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
i : α
f g : (i : α) → ℝ≥0
sf : ℝ≥0
hf : HasSum (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) (↑sf : ℝ≥0∞)
sg : ℝ≥0
hg : HasSum (fun (i : α) ↦ (↑(g i) : ℝ≥0∞)) (↑sg : ℝ≥0∞)
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
⊢ sf < sg

Tactic:
NNReal.hasSum_lt h hi (ENNReal.hasSum_coe.1 hf) (ENNReal.hasSum_coe.1 hg)

Premises used: NNReal.hasSum_lt, Iff.mp, ENNReal.hasSum_coe
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
i : α
f g : (i : α) → ℝ≥0
sf : ℝ≥0
hf : HasSum (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) (↑sf : ℝ≥0∞)
sg : ℝ≥0
hg : HasSum (fun (i : α) ↦ (↑(g i) : ℝ≥0∞)) (↑sg : ℝ≥0∞)
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
⊢ sf < sg

Tactic:
exact NNReal.hasSum_lt h hi (ENNReal.hasSum_coe.1 hf) (ENNReal.hasSum_coe.1 hg)

Premises used: NNReal.hasSum_lt, Iff.mp, ENNReal.hasSum_coe
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f g : α → ℝ≥0∞
i : α
hfi : tsum f ≠ ∞
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
⊢ LT.lt (α := ℝ≥0∞) (∑' (x : α), f x) (∑' (x : α), g x)

Tactic:
hasSum_lt h hi hfi ENNReal.summable.hasSum ENNReal.summable.hasSum

Premises used: ENNReal.summable, Summable.hasSum, ENNReal.hasSum_lt
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
β : Type u_4
f : α → ℝ
hf : Summable f
hn : ∀ (a : α), 0 ≤ f a
i : β → α
hi : Injective i
⊢ ∀ (i : α), 0 ≤ f i

Tactic:
hn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
β : Type u_4
f : α → ℝ
hf : Summable f
hn : ∀ (a : α), 0 ≤ f a
i : β → α
hi : Injective i
lift :
  ∀ (f : (i : α) → ℝ≥0) (hf : Summable (α := ℝ) fun (i : α) ↦ (↑(f i) : ℝ)),
    LE.le (α := ℝ) (tsum ((fun (i : α) ↦ (↑(f i) : ℝ)) ∘ i)) (∑' (i : α), (↑(f i) : ℝ))
⊢ tsum (f ∘ i) ≤ tsum f

Tactic:
lift f to α → ℝ≥0 using hn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
β : Type u_4
i : β → α
hi : Injective i
f : (i : α) → ℝ≥0
hf : Summable (α := ℝ) fun (i : α) ↦ (↑(f i) : ℝ)
⊢ Summable f

Tactic:
rw [NNReal.summable_coe] at hf

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

Tactic:
simpa only [Function.comp_def, ← NNReal.coe_tsum] using NNReal.tsum_comp_le_tsum_of_inj hf hi

Premises used: NNReal.tsum_comp_le_tsum_of_inj, Function.comp_def, NNReal.coe_tsum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
β : Type u_2
f g : β → ℝ
hg : ∀ (b : β), 0 ≤ g b
hgf : ∀ (b : β), g b ≤ f b
hf : Summable f
⊢ ∀ (i : β), 0 ≤ f i

Tactic:
fun b => (hg b).trans (hgf b)

Premises used: LE.le.trans
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
β : Type u_2
f g : β → ℝ
hg : ∀ (b : β), 0 ≤ g b
hgf : ∀ (b : β), g b ≤ f b
hf : Summable f
lift :
  ∀ (f : (i : β) → ℝ≥0) (hgf : ∀ (b : β), g b ≤ (fun (i : β) ↦ (↑(f i) : ℝ)) b)
    (hf : Summable (α := ℝ) fun (i : β) ↦ (↑(f i) : ℝ)), Summable g
⊢ Summable g

Tactic:
lift f to β → ℝ≥0 using fun b => (hg b).trans (hgf b)

Premises used: LE.le.trans
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
β : Type u_2
g : β → ℝ
hg : ∀ (b : β), 0 ≤ g b
f : (i : β) → ℝ≥0
hgf : ∀ (b : β), g b ≤ (fun (i : β) ↦ (↑(f i) : ℝ)) b
hf : Summable (α := ℝ) fun (i : β) ↦ (↑(f i) : ℝ)
⊢ ∀ (i : β), 0 ≤ g i

Tactic:
hg
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
β : Type u_2
g : β → ℝ
hg : ∀ (b : β), 0 ≤ g b
f : (i : β) → ℝ≥0
hgf : ∀ (b : β), g b ≤ (fun (i : β) ↦ (↑(f i) : ℝ)) b
hf : Summable (α := ℝ) fun (i : β) ↦ (↑(f i) : ℝ)
lift :
  ∀ (g : (i : β) → ℝ≥0)
    (hgf : ∀ (b : β), LE.le (α := ℝ) ((fun (i : β) ↦ (↑(g i) : ℝ)) b) ((fun (i : β) ↦ (↑(f i) : ℝ)) b)),
    Summable (α := ℝ) fun (i : β) ↦ (↑(g i) : ℝ)
⊢ Summable g

Tactic:
lift g to β → ℝ≥0 using hg
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
β : Type u_2
f : (i : β) → ℝ≥0
hf : Summable (α := ℝ) fun (i : β) ↦ (↑(f i) : ℝ)
g : (i : β) → ℝ≥0
hgf : ∀ (b : β), LE.le (α := ℝ) ((fun (i : β) ↦ (↑(g i) : ℝ)) b) ((fun (i : β) ↦ (↑(f i) : ℝ)) b)
rw :
  ∀ (hf : Summable f) (g : (i : β) → ℝ≥0)
    (hgf : ∀ (b : β), LE.le (α := ℝ) ((fun (i : β) ↦ (↑(g i) : ℝ)) b) ((fun (i : β) ↦ (↑(f i) : ℝ)) b)), Summable g
⊢ Summable (α := ℝ) fun (i : β) ↦ (↑(g i) : ℝ)

Tactic:
rw [NNReal.summable_coe] at hf ⊢

Premises used: NNReal.summable_coe
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
β : Type u_2
f : (i : β) → ℝ≥0
hf : Summable f
g : (i : β) → ℝ≥0
hgf : ∀ (b : β), LE.le (α := ℝ) ((fun (i : β) ↦ (↑(g i) : ℝ)) b) ((fun (i : β) ↦ (↑(f i) : ℝ)) b)
⊢ Summable g

Tactic:
NNReal.summable_of_le (fun b => NNReal.coe_le_coe.1 (hgf b)) hf

Premises used: Iff.mp, NNReal.summable_of_le, NNReal.coe_le_coe
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
β : Type u_2
f : (i : β) → ℝ≥0
hf : Summable f
g : (i : β) → ℝ≥0
hgf : ∀ (b : β), LE.le (α := ℝ) ((fun (i : β) ↦ (↑(g i) : ℝ)) b) ((fun (i : β) ↦ (↑(f i) : ℝ)) b)
⊢ Summable g

Tactic:
exact NNReal.summable_of_le (fun b => NNReal.coe_le_coe.1 (hgf b)) hf

Premises used: Iff.mp, NNReal.summable_of_le, NNReal.coe_le_coe
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ
hf : Summable f
apply : Summable (α := ℝ) fun (a : α) ↦ (↑(f a).toNNReal : ℝ)
⊢ Summable (α := ℝ≥0) fun (n : α) ↦ (f n).toNNReal

Tactic:
apply NNReal.summable_coe.1

Premises used: NNReal.summable_coe, Iff.mp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ
hf : Summable f
⊢ Summable (α := ℝ) fun (a : α) ↦ (↑(f a).toNNReal : ℝ)

Tactic:
.of_nonneg_of_le (fun n => NNReal.coe_nonneg _) (fun n => ?_) hf.abs

Premises used: Summable.abs, Summable.of_nonneg_of_le, NNReal.coe_nonneg, Real.toNNReal
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ
hf : Summable f
refine : ∀ (n : α), (↑(f n).toNNReal : ℝ) ≤ |f n|
⊢ Summable (α := ℝ) fun (a : α) ↦ (↑(f a).toNNReal : ℝ)

Tactic:
refine .of_nonneg_of_le (fun n => NNReal.coe_nonneg _) (fun n => ?_) hf.abs
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ
hf : Summable f
n : α
⊢ (↑(f n).toNNReal : ℝ) ≤ |f n|

Tactic:
simp only [le_abs_self, Real.coe_toNNReal', max_le_iff, abs_nonneg, and_self_iff]

Premises used: le_abs_self, Real.coe_toNNReal', max_le_iff, and_self_iff, abs_nonneg
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ
hf : Summable f
rw : Summable (α := ℝ≥0) fun (i : α) ↦ (f i).toNNReal
⊢ LT.lt (α := ℝ≥0∞) (∑' (i : α), (↑(f i).toNNReal : ℝ≥0∞)) ∞

Tactic:
rw [lt_top_iff_ne_top, ENNReal.tsum_coe_ne_top_iff_summable]

Premises used: lt_top_iff_ne_top, ENNReal.tsum_coe_ne_top_iff_summable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ
hf : Summable f
⊢ Summable (α := ℝ≥0) fun (i : α) ↦ (f i).toNNReal

Tactic:
hf.toNNReal

Premises used: Summable.toNNReal
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ
hf : Summable f
⊢ Summable (α := ℝ≥0) fun (i : α) ↦ (f i).toNNReal

Tactic:
exact hf.toNNReal

Premises used: Summable.toNNReal
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ
hf : Summable f
⊢ Ne (α := ℝ≥0∞) (∑' (i : α), ENNReal.ofReal (f i)) ∞

Tactic:
hf.tsum_ofReal_lt_top.ne

Premises used: Summable.tsum_ofReal_lt_top, LT.lt.ne
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0∞
h : Ne (α := ℝ≥0∞) (∑' (i : α), f i) ∞
⊢ ∀ (i : α), f i ≠ ∞

Tactic:
ENNReal.ne_top_of_tsum_ne_top h

Premises used: ENNReal.ne_top_of_tsum_ne_top
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0∞
h : Ne (α := ℝ≥0∞) (∑' (i : α), f i) ∞
lift :
  ∀ (f : (i : α) → ℝ≥0) (h : Ne (α := ℝ≥0∞) (∑' (i : α), (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) i) ∞),
    Set.Countable.{u_1} (α := α) (support (M := ℝ≥0∞) fun (i : α) ↦ (↑(f i) : ℝ≥0∞))
⊢ (support f).Countable

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

Premises used: ENNReal.ne_top_of_tsum_ne_top
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : (i : α) → ℝ≥0
h : Ne (α := ℝ≥0∞) (∑' (i : α), (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) i) ∞
⊢ Set.Countable.{u_1} (α := α) (support (M := ℝ≥0∞) fun (i : α) ↦ (↑(f i) : ℝ≥0∞))

Tactic:
simpa [support] using (ENNReal.tsum_coe_ne_top_iff_summable.1 h).countable_support_nnreal

Premises used: Summable.countable_support_nnreal, ENNReal.tsum_coe_ne_top_iff_summable, Function.support, Iff.mp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ
hf : ∀ (i : ℕ), 0 ≤ f i
r : ℝ
⊢ ∀ (i : ℕ), 0 ≤ f i

Tactic:
hf
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ
hf : ∀ (i : ℕ), 0 ≤ f i
r : ℝ
lift :
  ∀ (f : (i : ℕ) → ℝ≥0),
    HasSum (fun (i : ℕ) ↦ (↑(f i) : ℝ)) r ↔
      Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, (fun (i : ℕ) ↦ (↑(f i) : ℝ)) i) atTop (𝓝 r)
⊢ HasSum f r ↔ Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)

Tactic:
lift f to ℕ → ℝ≥0 using hf
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
r : ℝ
f : (i : ℕ) → ℝ≥0
simp :
  (∃ (hx : 0 ≤ r),
      Tendsto (fun (a : Finset ℕ) ↦ ∑ i ∈ a, f i) (SummationFilter.unconditional ℕ).filter
        (𝓝 (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) r hx))) ↔
    ∃ (hx : 0 ≤ r),
      Tendsto (fun (a : ℕ) ↦ ∑ i ∈ Finset.range a, f i) atTop (𝓝 (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) r hx))
⊢ HasSum (fun (i : ℕ) ↦ (↑(f i) : ℝ)) r ↔
    Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, (fun (i : ℕ) ↦ (↑(f i) : ℝ)) i) atTop (𝓝 r)

Tactic:
simp only [HasSum, ← NNReal.coe_sum, NNReal.tendsto_coe']

Premises used: NNReal.coe_sum, HasSum, NNReal.tendsto_coe', SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
r : ℝ
f : (i : ℕ) → ℝ≥0
⊢ (∃ (hx : 0 ≤ r),
      Tendsto (fun (a : Finset ℕ) ↦ ∑ i ∈ a, f i) (SummationFilter.unconditional ℕ).filter
        (𝓝 (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) r hx))) ↔
    ∃ (hx : 0 ≤ r),
      Tendsto (fun (a : ℕ) ↦ ∑ i ∈ Finset.range a, f i) atTop (𝓝 (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) r hx))

Tactic:
exists_congr fun hr => NNReal.hasSum_iff_tendsto_nat

Premises used: NNReal.hasSum_iff_tendsto_nat, exists_congr
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
r : ℝ
f : (i : ℕ) → ℝ≥0
⊢ (∃ (hx : 0 ≤ r),
      Tendsto (fun (a : Finset ℕ) ↦ ∑ i ∈ a, f i) (SummationFilter.unconditional ℕ).filter
        (𝓝 (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) r hx))) ↔
    ∃ (hx : 0 ≤ r),
      Tendsto (fun (a : ℕ) ↦ ∑ i ∈ Finset.range a, f i) atTop (𝓝 (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) r hx))

Tactic:
exact exists_congr fun hr => NNReal.hasSum_iff_tendsto_nat

Premises used: NNReal.hasSum_iff_tendsto_nat, exists_congr
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0∞
h₀ : ∀ (i : α), f i ≤ 1
⊢ Multipliable f

Tactic:
⟨_, _root_.hasProd_of_isGLB_of_le_one _ h₀ (isGLB_sInf _)⟩

Premises used: Multipliable, isGLB_sInf, Exists.intro, hasProd_of_isGLB_of_le_one