awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
hf : ¬Eq (α := ℝ≥0∞) (∑' (i : α), f i) 0
⊢ Tendsto (fun (s : Finset α) ↦ a * ∑ i ∈ s, f i) atTop (𝓝 (a * ∑' (i : α), f i))

Tactic:
exact ENNReal.Tendsto.const_mul ENNReal.summable.hasSum (Or.inl hf)

Premises used: ENNReal.Tendsto.const_mul, ENNReal.summable, Summable.hasSum, Or.inl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
hf : ¬Eq (α := ℝ≥0∞) (∑' (i : α), f i) 0
⊢ Tendsto (fun (s : Finset α) ↦ ∑ j ∈ s, a * f j) atTop (𝓝 (a * ∑' (i : α), f i))

Tactic:
have : Tendsto (fun s : Finset α => ∑ j ∈ s, a * f j) atTop (𝓝 (a * ∑' i, f i)) := by
      simp only [← Finset.mul_sum]
      exact ENNReal.Tendsto.const_mul ENNReal.summable.hasSum (Or.inl hf)
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
hf : ¬Eq (α := ℝ≥0∞) (∑' (i : α), f i) 0
this : Tendsto (fun (s : Finset α) ↦ ∑ j ∈ s, a * f j) atTop (𝓝 (a * ∑' (i : α), f i))
⊢ ∑' (i : α), a * f i = a * ∑' (i : α), f i

Tactic:
HasSum.tsum_eq this

Premises used: HasSum.tsum_eq
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
hf : ¬Eq (α := ℝ≥0∞) (∑' (i : α), f i) 0
this : Tendsto (fun (s : Finset α) ↦ ∑ j ∈ s, a * f j) atTop (𝓝 (a * ∑' (i : α), f i))
⊢ ∑' (i : α), a * f i = a * ∑' (i : α), f i

Tactic:
exact HasSum.tsum_eq this
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
⊢ ∑' (i : α), f i * a = (∑' (i : α), f i) * a

Tactic:
simp [mul_comm, ENNReal.tsum_mul_left]

Premises used: ENNReal.tsum_mul_left, mul_comm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0∞
R : Type u_4
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
a : R
⊢ ∑' (i : α), a • f i = HSMul.hSMul (β := ℝ≥0∞) a (∑' (i : α), f i)

Tactic:
simpa only [smul_one_mul] using @ENNReal.tsum_mul_left _ (a • (1 : ℝ≥0∞)) _

Premises used: ENNReal.tsum_mul_left, smul_one_mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_4
a : α
f : α → ℝ≥0∞
x : α
h : x ≠ a
⊢ Eq (α := ℝ≥0∞) (⨆ (_ : a = x), f x) 0

Tactic:
simp [h.symm]

Premises used: Ne.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_4
a : α
f : α → ℝ≥0∞
⊢ ⨆ (_ : a = a), f a = f a

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

Tactic:
⟨HasSum.tendsto_sum_nat, fun h => ?_⟩

Premises used: HasSum.tendsto_sum_nat, Iff.intro
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0∞
r : ℝ≥0∞
refine : ∀ (h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)), HasSum f r
⊢ HasSum f r ↔ Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)

Tactic:
refine ⟨HasSum.tendsto_sum_nat, fun h => ?_⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0∞
r : ℝ≥0∞
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
rw : HasSum f (∑' (i : ℕ), f i)
rw₁ : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i
⊢ HasSum f r

Tactic:
rw [← iSup_eq_of_tendsto _ h, ← ENNReal.tsum_eq_iSup_nat]

Premises used: iSup_eq_of_tendsto, ENNReal.tsum_eq_iSup_nat
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0∞
r : ℝ≥0∞
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
⊢ HasSum f (∑' (i : ℕ), f i)

Tactic:
ENNReal.summable.hasSum

Premises used: ENNReal.summable, Summable.hasSum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0∞
r : ℝ≥0∞
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
⊢ HasSum f (∑' (i : ℕ), f i)

Tactic:
exact ENNReal.summable.hasSum

Premises used: ENNReal.summable, Summable.hasSum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0∞
r : ℝ≥0∞
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
⊢ Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i

Tactic:
fun s t hst => Finset.sum_le_sum_of_subset (Finset.range_subset_range.2 hst)

Premises used: Iff.mpr, Monotone, Finset.range_subset_range, Finset.sum_le_sum_of_subset
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0∞
r : ℝ≥0∞
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
⊢ Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i

Tactic:
exact fun s t hst => Finset.sum_le_sum_of_subset (Finset.range_subset_range.2 hst)

Premises used: Iff.mpr, Finset.range_subset_range, Finset.sum_le_sum_of_subset
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0∞
rw : HasSum f (∑' (n : ℕ), f n)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))

Tactic:
rw [← hasSum_iff_tendsto_nat]

Premises used: ENNReal.hasSum_iff_tendsto_nat
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0∞
⊢ HasSum f (∑' (n : ℕ), f n)

Tactic:
ENNReal.summable.hasSum

Premises used: ENNReal.summable, Summable.hasSum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0∞
⊢ HasSum f (∑' (n : ℕ), f n)

Tactic:
exact ENNReal.summable.hasSum

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

Tactic:
coe_toNNReal <| ENNReal.ne_top_of_tsum_ne_top hf _

Premises used: ENNReal.coe_toNNReal, ENNReal.toNNReal, WithTop.untopD, WithTop.recTopCoe, ENNReal.ne_top_of_tsum_ne_top
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_4
f : α → ℝ≥0∞
hf : Ne (α := ℝ≥0∞) (∑' (i : α), f i) ∞
⊢ Summable (ENNReal.toNNReal ∘ f)

Tactic:
simpa only [← tsum_coe_ne_top_iff_summable, toNNReal_apply_of_tsum_ne_top hf] using hf

Premises used: ENNReal.tsum_coe_ne_top_iff_summable, ENNReal.toNNReal_apply_of_tsum_ne_top
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_4
f : α → ℝ≥0∞
hf : Ne (α := ℝ≥0∞) (∑' (x : α), f x) ∞
⊢ ∀ (n : α), f n ≠ ∞

Tactic:
have f_ne_top : ∀ n, f n ≠ ∞ := ENNReal.ne_top_of_tsum_ne_top hf
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_4
f : α → ℝ≥0∞
hf : Ne (α := ℝ≥0∞) (∑' (x : α), f x) ∞
f_ne_top : ∀ (n : α), f n ≠ ∞
⊢ f = fun (n : α) ↦ (↑(f n).toNNReal : ℝ≥0∞)

Tactic:
have h_f_coe : f = fun n => ((f n).toNNReal : ENNReal) :=
    funext fun n => (coe_toNNReal (f_ne_top n)).symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_4
f : α → ℝ≥0∞
hf : Ne (α := ℝ≥0∞) (∑' (x : α), f x) ∞
f_ne_top : ∀ (n : α), f n ≠ ∞
h_f_coe : f = fun (n : α) ↦ (↑(f n).toNNReal : ℝ≥0∞)
rw : Tendsto (β := ℝ≥0) (fun (n : α) ↦ (f n).toNNReal) cofinite (𝓝 0)
⊢ Tendsto f cofinite (𝓝 0)

Tactic:
rw [h_f_coe, ← @coe_zero, tendsto_coe]

Premises used: ENNReal.coe_zero, ENNReal.tendsto_coe
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_4
f : α → ℝ≥0∞
hf : Ne (α := ℝ≥0∞) (∑' (x : α), f x) ∞
f_ne_top : ∀ (n : α), f n ≠ ∞
h_f_coe : f = fun (n : α) ↦ (↑(f n).toNNReal : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0) (fun (n : α) ↦ (f n).toNNReal) cofinite (𝓝 0)

Tactic:
NNReal.tendsto_cofinite_zero_of_summable (summable_toNNReal_of_tsum_ne_top hf)

Premises used: ENNReal.summable_toNNReal_of_tsum_ne_top, NNReal.tendsto_cofinite_zero_of_summable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_4
f : α → ℝ≥0∞
hf : Ne (α := ℝ≥0∞) (∑' (x : α), f x) ∞
f_ne_top : ∀ (n : α), f n ≠ ∞
h_f_coe : f = fun (n : α) ↦ (↑(f n).toNNReal : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0) (fun (n : α) ↦ (f n).toNNReal) cofinite (𝓝 0)

Tactic:
exact NNReal.tendsto_cofinite_zero_of_summable (summable_toNNReal_of_tsum_ne_top hf)

Premises used: ENNReal.summable_toNNReal_of_tsum_ne_top, NNReal.tendsto_cofinite_zero_of_summable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0∞
hf : Ne (α := ℝ≥0∞) (∑' (x : ℕ), f x) ∞
rw : Tendsto f cofinite (𝓝 0)
⊢ Tendsto f atTop (𝓝 0)

Tactic:
rw [← Nat.cofinite_eq_atTop]

Premises used: Nat.cofinite_eq_atTop
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0∞
hf : Ne (α := ℝ≥0∞) (∑' (x : ℕ), f x) ∞
⊢ Tendsto f cofinite (𝓝 0)

Tactic:
tendsto_cofinite_zero_of_tsum_ne_top hf

Premises used: ENNReal.tendsto_cofinite_zero_of_tsum_ne_top
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0∞
hf : Ne (α := ℝ≥0∞) (∑' (x : ℕ), f x) ∞
⊢ Tendsto f cofinite (𝓝 0)

Tactic:
exact tendsto_cofinite_zero_of_tsum_ne_top hf

Premises used: ENNReal.tendsto_cofinite_zero_of_tsum_ne_top
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_4
f : α → ℝ≥0∞
hf : Ne (α := ℝ≥0∞) (∑' (x : α), f x) ∞
⊢ ∀ (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:
α : Type u_4
f : α → ℝ≥0∞
hf : Ne (α := ℝ≥0∞) (∑' (x : α), f x) ∞
lift :
  ∀ (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)
⊢ Tendsto (β := ℝ≥0∞) (fun (s : Finset α) ↦ ∑' (b : { x : α // x ∉ s }), f (↑b : α)) 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:
α : Type u_4
f : (i : α) → ℝ≥0
hf : Ne (α := ℝ≥0∞) (∑' (x : α), (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) x) ∞
⊢ Tendsto (fun (a : Finset α) ↦ (↑(∑' (b : { x : α // x ∉ a }), f (↑b : α)) : ℝ≥0∞)) atTop (𝓝 (↑0 : ℝ≥0∞))

Tactic:
ENNReal.tendsto_coe.2 (NNReal.tendsto_tsum_compl_atTop_zero f)

Premises used: Iff.mpr, ENNReal.tendsto_coe, NNReal.tendsto_tsum_compl_atTop_zero
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_4
f : (i : α) → ℝ≥0
hf : Ne (α := ℝ≥0∞) (∑' (x : α), (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) x) ∞
h :
  ∀ (x : Finset α),
    ∑' (b : { x_1 : α // x_1 ∉ x }), (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) (↑b : α) =
      (↑(∑' (b : { x_1 : α // x_1 ∉ x }), f (↑b : α)) : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (s : Finset α) ↦ ∑' (b : { x : α // x ∉ s }), (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) (↑b : α)) atTop
    (𝓝 0)

Tactic:
convert! ENNReal.tendsto_coe.2 (NNReal.tendsto_tsum_compl_atTop_zero f)

Premises used: Iff.mpr, ENNReal.tendsto_coe, NNReal.tendsto_tsum_compl_atTop_zero
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_4
f : (i : α) → ℝ≥0
hf : Ne (α := ℝ≥0∞) (∑' (x : α), (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) x) ∞
x : Finset α
h : Summable (α := ℝ≥0) fun (b : { x_1 : α // x_1 ∉ x }) ↦ f (↑b : α)
⊢ ∑' (b : { x_1 : α // x_1 ∉ x }), (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) (↑b : α) =
    (↑(∑' (b : { x_1 : α // x_1 ∉ x }), f (↑b : α)) : ℝ≥0∞)

Tactic:
rw [ENNReal.coe_tsum]

Premises used: ENNReal.coe_tsum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_4
f : (i : α) → ℝ≥0
hf : Ne (α := ℝ≥0∞) (∑' (x : α), (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) x) ∞
x : Finset α
⊢ Summable (α := ℝ≥0) fun (b : { x_1 : α // x_1 ∉ x }) ↦ f (↑b : α)

Tactic:
NNReal.summable_comp_injective (tsum_coe_ne_top_iff_summable.1 hf) Subtype.coe_injective

Premises used: Subtype.coe_injective, NNReal.summable_comp_injective, ENNReal.tsum_coe_ne_top_iff_summable, Iff.mp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_4
f : (i : α) → ℝ≥0
hf : Ne (α := ℝ≥0∞) (∑' (x : α), (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) x) ∞
x : Finset α
⊢ Summable (α := ℝ≥0) fun (b : { x_1 : α // x_1 ∉ x }) ↦ f (↑b : α)

Tactic:
exact NNReal.summable_comp_injective (tsum_coe_ne_top_iff_summable.1 hf) Subtype.coe_injective

Premises used: Subtype.coe_injective, NNReal.summable_comp_injective, ENNReal.tsum_coe_ne_top_iff_summable, Iff.mp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
ι : Type u_4
α : Type u_5
f : ι → α → ℝ≥0∞
x : α
⊢ Eq (α := ℝ≥0∞) ((∑' (i : ι), f i) x) (∑' (i : ι), f i x)

Tactic:
tsum_apply <| Pi.summable.mpr fun _ => ENNReal.summable

Premises used: Iff.mpr, ENNReal.summable, tsum_apply, Pi.summable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f g : ℕ → ℝ≥0∞
h₁ : Ne (α := ℝ≥0∞) (∑' (i : ℕ), g i) ∞
h₂ : g ≤ f
this : ∀ (i : ℕ), f i - g i + g i = f i
⊢ HAdd.hAdd (α := ℝ≥0∞) (∑' (i : ℕ), (f i - g i)) (∑' (i : ℕ), g i) = ∑' (i : ℕ), f i

Tactic:
simp only [← ENNReal.tsum_add, this]

Premises used: ENNReal.tsum_add
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
g : β → ℝ≥0∞
⊢ LE.le (α := ℝ≥0∞) (∑' (x : α), g (f x)) (∑' (y : β), g y)

Tactic:
ENNReal.summable.tsum_le_tsum_of_inj f hf (fun _ _ => zero_le) (fun _ => le_rfl)
    ENNReal.summable

Premises used: zero_le, le_rfl, ENNReal.summable, Summable.tsum_le_tsum_of_inj
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
g : β → ℝ≥0∞
⊢ Eq (α := ℝ≥0∞) (∑' (y : β), g y) (∑' (y : β), g (f (surjInv hf y)))

Tactic:
simp only [surjInv_eq hf]

Premises used: Function.surjInv_eq
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0∞
s t : Set α
h : s ⊆ t
⊢ LE.le (α := ℝ≥0∞) (∑' (x : (↑s : Type u_1)), f (↑x : α)) (∑' (x : (↑t : Type u_1)), f (↑x : α))

Tactic:
tsum_comp_le_tsum_of_injective (inclusion_injective h) _

Premises used: ENNReal.tsum_comp_le_tsum_of_injective, Set.inclusion_injective
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
ι : Type u_4
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 : α))

Tactic:
calc ∑' x : ⋃ i, t i, f x ≤ ∑' x : Σ i, t i, f x.2 :=
    tsum_le_tsum_comp_of_surjective (sigmaToiUnion_surjective t) _
  _ = ∑' i, ∑' x : t i, f x := ENNReal.tsum_sigma' _

Premises used: Trans.trans, ENNReal.tsum_sigma', ENNReal.tsum_le_tsum_comp_of_surjective, Set.sigmaToiUnion_surjective
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
ι : Type u_4
f : α → ℝ≥0∞
s : Set ι
t : ι → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ s, t i) (⋃ (i : (↑s : Type u_4)), t (↑i : ι))

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
ι : Type u_4
f : α → ℝ≥0∞
s : Finset ι
t : ι → Set α
⊢ LE.le (α := ℝ≥0∞) (∑' (x : (↑(⋃ i ∈ s, t i) : Type u_1)), f (↑x : α))
    (∑ i ∈ s, ∑' (x : (↑(t i) : Type u_1)), f (↑x : α))

Tactic:
(tsum_biUnion_le_tsum f s t).trans_eq (Finset.tsum_subtype s fun i => ∑' x : t i, f x)

Premises used: LE.le.trans_eq, ENNReal.tsum_biUnion_le_tsum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
ι : Type u_4
inst : Fintype ι
f : α → ℝ≥0∞
t : ι → Set α
rw :
  LE.le (α := ℝ≥0∞) (∑' (x : (↑(⋃ (i : ι), t i) : Type u_1)), f (↑x : α))
    (∑' (b : ι) (x : (↑(t b) : Type u_1)), f (↑x : α))
⊢ LE.le (α := ℝ≥0∞) (∑' (x : (↑(⋃ (i : ι), t i) : Type u_1)), f (↑x : α))
    (∑ i : ι, ∑' (x : (↑(t i) : Type u_1)), f (↑x : α))

Tactic:
rw [← tsum_fintype (L := SummationFilter.unconditional _)]

Premises used: tsum_fintype
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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 : α))
    (∑' (b : ι) (x : (↑(t b) : Type u_1)), f (↑x : α))

Tactic:
tsum_iUnion_le_tsum f t

Premises used: ENNReal.tsum_iUnion_le_tsum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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 : α))
    (∑' (b : ι) (x : (↑(t b) : Type u_1)), f (↑x : α))

Tactic:
exact tsum_iUnion_le_tsum f t

Premises used: ENNReal.tsum_iUnion_le_tsum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0∞
s t : Set α
⊢ ∑' (x : (↑(⋃ (b : Bool), bif b then s else t) : Type u_1)), f (↑x : α) ≤
    HAdd.hAdd (α := ℝ≥0∞) (∑' (x : (↑s : Type u_1)), f (↑x : α)) (∑' (x : (↑t : Type u_1)), f (↑x : α))

Tactic:
simpa using tsum_iUnion_le f (cond · s t)

Premises used: cond, ENNReal.tsum_iUnion_le
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
β : Type u_2
f : β → ℝ≥0∞
b : β
⊢ ∑' (x : β), f x = f b + ∑' (x : β), if x = b then 0 else f x

Tactic:
ENNReal.summable.tsum_eq_add_tsum_ite' b

Premises used: ENNReal.summable, Summable.tsum_eq_add_tsum_ite'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0∞
hf : Eq (α := ℝ≥0∞) (∑' (n : ℕ), f n) ∞
hf0 : f 0 ≠ ∞
⊢ f 0 = ∞ ∨ Eq (α := ℝ≥0∞) (∑' (b : ℕ), f (b + 1)) ∞

Tactic:
rw [tsum_eq_zero_add' ENNReal.summable, add_eq_top] at hf

Premises used: ENNReal.add_eq_top, ENNReal.summable, tsum_eq_zero_add'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0∞
hf : Eq (α := ℝ≥0∞) (∑' (n : ℕ), f n) ∞
hf0 : f 0 ≠ ∞
hf₁ : f 0 = ∞ ∨ Eq (α := ℝ≥0∞) (∑' (b : ℕ), f (b + 1)) ∞
⊢ f 0 ≠ ∞

Tactic:
rw [tsum_eq_zero_add' ENNReal.summable, add_eq_top] at hf

Premises used: ENNReal.add_eq_top, ENNReal.summable, tsum_eq_zero_add'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0∞
hf : f 0 = ∞ ∨ Eq (α := ℝ≥0∞) (∑' (b : ℕ), f (b + 1)) ∞
hf0 : f 0 ≠ ∞
⊢ Eq (α := ℝ≥0∞) (∑' (n : ℕ), f (n + 1)) ∞

Tactic:
hf.resolve_left hf0

Premises used: Or.resolve_left
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0∞
hf : f 0 = ∞ ∨ Eq (α := ℝ≥0∞) (∑' (b : ℕ), f (b + 1)) ∞
hf0 : f 0 ≠ ∞
⊢ Eq (α := ℝ≥0∞) (∑' (n : ℕ), f (n + 1)) ∞

Tactic:
exact hf.resolve_left hf0

Premises used: Or.resolve_left
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
ι : Type u_4
a : ι → ℝ≥0∞
tsum_ne_top : Ne (α := ℝ≥0∞) (∑' (i : ι), a i) ∞
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
by_contra : ∀ (h : ¬Set.Finite.{u_4} (α := ι) {i : ι | ε ≤ a i}), False
⊢ Set.Finite.{u_4} (α := ι) {i : ι | ε ≤ a i}

Tactic:
by_contra h
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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}
⊢ Infinite.{u_4 + 1} (↑{i : ι | ε ≤ a i} : Type u_4)

Tactic:
have := Infinite.to_subtype h
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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

Tactic:
tsum_ne_top (top_unique ?_)

Premises used: top_unique
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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)
refine : LE.le (α := ℝ≥0∞) ∞ (∑' (i : ι), a i)
⊢ False

Tactic:
refine tsum_ne_top (top_unique ?_)

Premises used: top_unique
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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)
⊢ Eq (α := ℝ≥0∞) ∞ (∑' (x : (↑{i : ι | ε ≤ a i} : Type u_4)), ε)

Tactic:
(tsum_const_eq_top_of_ne_zero ε_ne_zero).symm

Premises used: ENNReal.tsum_const_eq_top_of_ne_zero, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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)
⊢ LE.le (α := ℝ≥0∞) (∑' (x : (↑{i : ι | ε ≤ a i} : Type u_4)), ε) (∑' (i : ι), a i)

Tactic:
ENNReal.summable.tsum_le_tsum_of_inj (↑)
    Subtype.val_injective (fun _ _ => zero_le) (fun i => i.2) ENNReal.summable

Premises used: zero_le, Subtype.val_injective, ENNReal.summable, Summable.tsum_le_tsum_of_inj, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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)
⊢ LE.le (α := ℝ≥0∞) ∞ (∑' (i : ι), a i)

Tactic:
calc ∞ = ∑' _ : { i | ε ≤ a i }, ε := (tsum_const_eq_top_of_ne_zero ε_ne_zero).symm
  _ ≤ ∑' i, a i := ENNReal.summable.tsum_le_tsum_of_inj (↑)
    Subtype.val_injective (fun _ _ => zero_le) (fun i => i.2) ENNReal.summable

Premises used: zero_le, ENNReal.tsum_const_eq_top_of_ne_zero, ENNReal.summable, Summable.tsum_le_tsum_of_inj, Eq.symm
-- 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
⊢ 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
-- 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}
⊢ ∃ (hf : Set.Finite.{u_4} (α := ι) {i : ι | ε ≤ a i}), (↑(#(hf.toFinset (s := {i : ι | ε ≤ a i}))) : ℝ≥0∞) ≤ c / ε

Tactic:
⟨hf, (ENNReal.le_div_iff_mul_le (.inl ε_ne_zero) (.inr c_ne_top)).2 ?_⟩

Premises used: Iff.mpr, ENNReal.le_div_iff_mul_le, Exists.intro, Or.inl, Or.inr
-- 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}
refine : (↑(#(hf.toFinset (s := {i : ι | ε ≤ a i}))) : ℝ≥0∞) * ε ≤ c
⊢ ∃ (hf : Set.Finite.{u_4} (α := ι) {i : ι | ε ≤ a i}), (↑(#(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 ?_⟩
-- 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}
rw : (↑(#(hf.toFinset (s := {i : ι | ε ≤ a i}))) : ℝ≥0∞) * ε = #(hf.toFinset (s := {i : ι | ε ≤ a i})) • ε
rw₁ rw₂ :
  (↑(#(hf.toFinset (s := {i : ι | ε ≤ a i}))) : ℝ≥0∞) * ε = (↑(#(hf.toFinset (s := {i : ι | ε ≤ a i}))) : ℝ≥0∞) * ε
⊢ (↑(#(hf.toFinset (s := {i : ι | ε ≤ a i}))) : ℝ≥0∞) * ε = ∑ _i ∈ hf.toFinset (s := {i : ι | ε ≤ a i}), ε

Tactic:
rw [Finset.sum_const, nsmul_eq_mul]

Premises used: nsmul_eq_mul, Finset.sum_const
-- 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}
⊢ LE.le (α := ℝ≥0∞) (∑ _i ∈ hf.toFinset (s := {i : ι | ε ≤ a i}), ε) (∑ i ∈ hf.toFinset (s := {i : ι | ε ≤ a i}), a i)

Tactic:
Finset.sum_le_sum fun i => hf.mem_toFinset.1

Premises used: Set.Finite.mem_toFinset, Iff.mp, Finset.sum_le_sum
-- 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}
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ hf.toFinset (s := {i : ι | ε ≤ a i}), a i) (∑' (i : ι), a i)

Tactic:
ENNReal.sum_le_tsum _

Premises used: ENNReal.sum_le_tsum
-- 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}
⊢ ∑' (i : ι), a i ≤ c

Tactic:
tsum_le_c