awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hsg : ¬sg = ∞
hg' : ∀ (x : α), g x ≠ ∞
⊢ sf < sg
have 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
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))
Cleared hypotheses: f, h, hi, hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
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
⊢ sf < sg
have 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
Tactic: lift g to α → ℝ≥0 using hg'
Cleared hypotheses: g, hg, hg', h, hi
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
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 < sg
have neg : ∀ (sf : ℝ≥0) (hf : HasSum (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) (↑sf : ℝ≥0∞)), (↑sf : ℝ≥0∞) < sg
Tactic: lift sf to ℝ≥0 using hsf
Cleared hypotheses: sf, hsf, hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
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∞)
⊢ (↑sf : ℝ≥0∞) < sg
have neg : ∀ (sg : ℝ≥0) (hg : HasSum (fun (i : α) ↦ (↑(g i) : ℝ≥0∞)) (↑sg : ℝ≥0∞)), (↑sf : ℝ≥0∞) < (↑sg : ℝ≥0∞)
Tactic: lift sg to ℝ≥0 using hsg
Cleared hypotheses: sg, hsg, hg
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
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∞)
⊢ (↑sf : ℝ≥0∞) < (↑sg : ℝ≥0∞)
have neg : ∀ (h : ∀ (a : α), f a ≤ g a) (hi : f i < g i), sf < sg
Tactic: simp only [coe_le_coe, coe_lt_coe] at h hi ⊢
Cleared hypotheses: h, hi
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
β : Type u_4
f : α → ℝ
hf : Summable f
hn : ∀ (a : α), 0 ≤ f a
i : β → α
hi : Injective i
⊢ tsum (f ∘ i) ≤ tsum f
have lift : ∀ (f : (i : α) → ℝ≥0) (hf : Summable (α := ℝ) fun (i : α) ↦ (↑(f i) : ℝ)),
  LE.le (α := ℝ) (tsum ((fun (i : α) ↦ (↑(f i) : ℝ)) ∘ i)) (∑' (i : α), (↑(f i) : ℝ))
Tactic: lift f to α → ℝ≥0 using hn
Cleared hypotheses: f, hf, hn
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (hypothesis)
Goal:
α : Type u_1
β : Type u_4
i : β → α
hi : Injective i
f : (i : α) → ℝ≥0
hf : Summable (α := ℝ) fun (i : α) ↦ (↑(f i) : ℝ)
⊢ LE.le (α := ℝ) (tsum ((fun (i : α) ↦ (↑(f i) : ℝ)) ∘ i)) (∑' (i : α), (↑(f i) : ℝ))
have hf₁ : Summable f
Tactic: rw [NNReal.summable_coe] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
β : Type u_2
f g : β → ℝ
hg : ∀ (b : β), 0 ≤ g b
hgf : ∀ (b : β), g b ≤ f b
hf : Summable f
⊢ Summable g
have lift : ∀ (f : (i : β) → ℝ≥0) (hgf : ∀ (b : β), g b ≤ (fun (i : β) ↦ (↑(f i) : ℝ)) b)
  (hf : Summable (α := ℝ) fun (i : β) ↦ (↑(f i) : ℝ)), Summable g
Tactic: lift f to β → ℝ≥0 using fun b => (hg b).trans (hgf b)
Cleared hypotheses: f, hgf, hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
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) : ℝ)
⊢ Summable g
have lift : ∀ (g : (i : β) → ℝ≥0)
  (hgf : ∀ (b : β), LE.le (α := ℝ) ((fun (i : β) ↦ (↑(g i) : ℝ)) b) ((fun (i : β) ↦ (↑(f i) : ℝ)) b)),
  Summable (α := ℝ) fun (i : β) ↦ (↑(g i) : ℝ)
Tactic: lift g to β → ℝ≥0 using hg
Cleared hypotheses: g, hg, hgf
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
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)
⊢ Summable (α := ℝ) fun (i : β) ↦ (↑(g i) : ℝ)
have rw : ∀ (hf : Summable f) (g : (i : β) → ℝ≥0)
  (hgf : ∀ (b : β), LE.le (α := ℝ) ((fun (i : β) ↦ (↑(g i) : ℝ)) b) ((fun (i : β) ↦ (↑(f i) : ℝ)) b)), Summable g
Tactic: rw [NNReal.summable_coe] at hf ⊢
Cleared hypotheses: hf, g, hgf
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
f : α → ℝ
hf : Summable f
⊢ Summable (α := ℝ≥0) fun (n : α) ↦ (f n).toNNReal
have apply : Summable (α := ℝ) fun (a : α) ↦ (↑(f a).toNNReal : ℝ)
Tactic: apply NNReal.summable_coe.1
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
f : α → ℝ
hf : Summable f
⊢ Summable (α := ℝ) fun (a : α) ↦ (↑(f a).toNNReal : ℝ)
have refine : ∀ (n : α), (↑(f n).toNNReal : ℝ) ≤ |f n|
Tactic: refine .of_nonneg_of_le (fun n => NNReal.coe_nonneg _) (fun n => ?_) hf.abs
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
f : α → ℝ
hf : Summable f
⊢ LT.lt (α := ℝ≥0∞) (∑' (i : α), (↑(f i).toNNReal : ℝ≥0∞)) ∞
have rw : Summable (α := ℝ≥0) fun (i : α) ↦ (f i).toNNReal
Tactic: rw [lt_top_iff_ne_top, ENNReal.tsum_coe_ne_top_iff_summable]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
f : α → ℝ≥0∞
h : Ne (α := ℝ≥0∞) (∑' (i : α), f i) ∞
⊢ (support f).Countable
have 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∞))
Tactic: lift f to α → ℝ≥0 using ENNReal.ne_top_of_tsum_ne_top h
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
f : ℕ → ℝ
hf : ∀ (i : ℕ), 0 ≤ f i
r : ℝ
⊢ HasSum f r ↔ Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
have lift : ∀ (f : (i : ℕ) → ℝ≥0),
  HasSum (fun (i : ℕ) ↦ (↑(f i) : ℝ)) r ↔
    Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, (fun (i : ℕ) ↦ (↑(f i) : ℝ)) i) atTop (𝓝 r)
Tactic: lift f to ℕ → ℝ≥0 using hf
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
r : ℝ
f : (i : ℕ) → ℝ≥0
⊢ HasSum (fun (i : ℕ) ↦ (↑(f i) : ℝ)) r ↔
    Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, (fun (i : ℕ) ↦ (↑(f i) : ℝ)) i) atTop (𝓝 r)
have 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))
Tactic: simp only [HasSum, ← NNReal.coe_sum, NNReal.tendsto_coe']
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ (↑(d n) : ℝ≥0∞)
hd : Summable d
⊢ CauchySeq f
have refine : ∀ (ε : ℝ≥0) (εpos : 0 < ε), ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → edist (f n) (f N) < (↑ε : ℝ≥0∞)
Tactic: refine EMetric.cauchySeq_iff_NNReal.2 fun ε εpos ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (hypothesis)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ (↑(d n) : ℝ≥0∞)
hd : Summable d
ε : ℝ≥0
εpos : 0 < ε
⊢ ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → edist (f n) (f N) < (↑ε : ℝ≥0∞)
have hd₁ : CauchySeq (α := ℝ≥0) fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, d x
Tactic: replace hd : CauchySeq fun n : ℕ ↦ ∑ x ∈ Finset.range n, d x :=
    let ⟨_, H⟩ := hd
    H.tendsto_sum_nat.cauchySeq
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ (↑(d n) : ℝ≥0∞)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq (α := ℝ≥0) fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, d x
⊢ ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → edist (f n) (f N) < (↑ε : ℝ≥0∞)
have refine : ∀ (N : ℕ) (hN : ∀ n ≥ N, dist (α := ℝ≥0) (∑ x ∈ Finset.range n, d x) (∑ x ∈ Finset.range N, d x) < (↑ε : ℝ)) (n : ℕ)
  (hn : N ≤ n), edist (f n) (f N) < (↑ε : ℝ≥0∞)
Tactic: refine (Metric.cauchySeq_iff'.1 hd ε (NNReal.coe_pos.2 εpos)).imp fun N hN n hn ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (hypothesis)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ (↑(d n) : ℝ≥0∞)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq (α := ℝ≥0) fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, d x
N : ℕ
hN : ∀ n ≥ N, dist (α := ℝ≥0) (∑ x ∈ Finset.range n, d x) (∑ x ∈ Finset.range N, d x) < (↑ε : ℝ)
n : ℕ
hn : N ≤ n
⊢ edist (f n) (f N) < (↑ε : ℝ≥0∞)
have hN₁ : dist (α := ℝ≥0) (∑ x ∈ Finset.range n, d x) (∑ x ∈ Finset.range N, d x) < (↑ε : ℝ)
Tactic: specialize hN n hn
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (hypothesis)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ (↑(d n) : ℝ≥0∞)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq (α := ℝ≥0) fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, d x
N n : ℕ
hn : N ≤ n
hN : dist (α := ℝ≥0) (∑ x ∈ Finset.range n, d x) (∑ x ∈ Finset.range N, d x) < (↑ε : ℝ)
⊢ edist (f n) (f N) < (↑ε : ℝ≥0∞)
have hN₁ : ∑ k ∈ Finset.Ico N n, d k < ε ∧
  ∑ x ∈ Finset.range N, d x - HAdd.hAdd (α := ℝ≥0) (∑ k ∈ Finset.range N, d k) (∑ k ∈ Finset.Ico N n, d k) < ε
Tactic: rw [dist_nndist, NNReal.nndist_eq, ← Finset.sum_range_add_sum_Ico _ hn, add_tsub_cancel_left,
    NNReal.coe_lt_coe, max_lt_iff] at hN
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ (↑(d n) : ℝ≥0∞)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq (α := ℝ≥0) fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, d x
N n : ℕ
hn : N ≤ n
hN :
  ∑ k ∈ Finset.Ico N n, d k < ε ∧
    ∑ x ∈ Finset.range N, d x - HAdd.hAdd (α := ℝ≥0) (∑ k ∈ Finset.range N, d k) (∑ k ∈ Finset.Ico N n, d k) < ε
⊢ edist (f n) (f N) < (↑ε : ℝ≥0∞)
have rw : edist (f N) (f n) < (↑ε : ℝ≥0∞)
Tactic: rw [edist_comm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ (↑(d n) : ℝ≥0∞)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq (α := ℝ≥0) fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, d x
N n : ℕ
hn : N ≤ n
hN :
  ∑ k ∈ Finset.Ico N n, d k < ε ∧
    ∑ x ∈ Finset.range N, d x - HAdd.hAdd (α := ℝ≥0) (∑ k ∈ Finset.range N, d k) (∑ k ∈ Finset.Ico N n, d k) < ε
⊢ edist (f N) (f n) < (↑ε : ℝ≥0∞)
have refine : ∑ i ∈ Finset.Ico N n, (↑(d i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
Tactic: refine lt_of_le_of_lt (edist_le_Ico_sum_of_edist_le hn fun _ _ ↦ hf _) ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n
hd : tsum d ≠ ∞
⊢ CauchySeq f
have lift : ∀ (d : (i : ℕ) → ℝ≥0) (hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ (fun (i : ℕ) ↦ (↑(d i) : ℝ≥0∞)) n)
  (hd : Ne (α := ℝ≥0∞) (∑' (i : ℕ), (↑(d i) : ℝ≥0∞)) ∞), CauchySeq f
Tactic: lift d to ℕ → NNReal using fun i => ENNReal.ne_top_of_tsum_ne_top hd i
Cleared hypotheses: d, hf, hd
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (hypothesis)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : ℕ → α
d : (i : ℕ) → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ (fun (i : ℕ) ↦ (↑(d i) : ℝ≥0∞)) n
hd : Ne (α := ℝ≥0∞) (∑' (i : ℕ), (↑(d i) : ℝ≥0∞)) ∞
⊢ CauchySeq f
have hd₁ : Summable d
Tactic: rw [ENNReal.tsum_coe_ne_top_iff_summable] at hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ edist (f n) a ≤ ∑' (m : ℕ), d (n + m)
have refine : ∀ (m : ℕ) (hnm : m ≥ n),
  Membership.mem (γ := Set ℕ) {x : ℕ | (fun (c : ℕ) ↦ edist (f n) (f c) ≤ ∑' (m : ℕ), d (n + m)) x} m
Tactic: refine le_of_tendsto (tendsto_const_nhds.edist ha) (mem_atTop_sets.2 ⟨n, fun m hnm => ?_⟩)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ edist (f n) (f m) ≤ ∑' (m : ℕ), d (n + m)
have refine : LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.Ico n m, d i) (∑' (m : ℕ), d (n + m))
Tactic: refine le_trans (edist_le_Ico_sum_of_edist_le hnm fun _ _ => hf _) ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.Ico n m, d i) (∑' (m : ℕ), d (n + m))
have rw : LE.le (α := ℝ≥0∞) (∑ k ∈ Finset.range (m - n), d (n + k)) (∑' (m : ℕ), d (n + m))
Tactic: rw [Finset.sum_Ico_eq_sum_range]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_4
s : Set α
⊢ ∑' (x : (↑s : Type u_4)), 1 = (↑s.encard : ℝ≥0∞)
have inl : ∀ (hfin : s.Finite), ∑' (x : (↑s : Type u_4)), 1 = (↑s.encard : ℝ≥0∞)
Tactic: obtain (hfin | hinf) := Set.finite_or_infinite s
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_4
s : Set α
inl : ∀ (hfin : s.Finite), ∑' (x : (↑s : Type u_4)), 1 = (↑s.encard : ℝ≥0∞)
⊢ ∑' (x : (↑s : Type u_4)), 1 = (↑s.encard : ℝ≥0∞)
have inr : ∀ (hinf : s.Infinite), ∑' (x : (↑s : Type u_4)), 1 = (↑s.encard : ℝ≥0∞)
Tactic: obtain (hfin | hinf) := Set.finite_or_infinite s
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_4
s : Set α
hfin : s.Finite
⊢ ∑' (x : (↑s : Type u_4)), 1 = (↑s.encard : ℝ≥0∞)
have inl : ∀ (s : Finset α), ∑' (x : (↑(↑s : Set α) : Type u_4)), 1 = (↑(↑s : Set α).encard : ℝ≥0∞)
Tactic: lift s to Finset α using hfin
Cleared hypotheses: s, hfin
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (hypothesis)
Goal:
α : Type u_4
s : Set α
hinf : s.Infinite
⊢ ∑' (x : (↑s : Type u_4)), 1 = (↑s.encard : ℝ≥0∞)
have this : Infinite.{u_4 + 1} (↑s : Type u_4)
Tactic: have : Infinite s := infinite_coe_iff.mpr hinf
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_4
s : Set α
hinf : s.Infinite
this : Infinite.{u_4 + 1} (↑s : Type u_4)
⊢ ∑' (x : (↑s : Type u_4)), 1 = (↑s.encard : ℝ≥0∞)
have inr : ∞ = (↑s.encard : ℝ≥0∞)
Tactic: rw [tsum_const_eq_top_of_ne_zero one_ne_zero, encard_eq_top hinf, ENat.toENNReal_top]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_4
s : Set α
hinf : s.Infinite
this : Infinite.{u_4 + 1} (↑s : Type u_4)
inr : ∞ = (↑s.encard : ℝ≥0∞)
⊢ ∑' (x : (↑s : Type u_4)), 1 = (↑s.encard : ℝ≥0∞)
have inr₁ : ∞ = (↑⊤ : ℝ≥0∞)
Tactic: rw [tsum_const_eq_top_of_ne_zero one_ne_zero, encard_eq_top hinf, ENat.toENNReal_top]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_4
s : Set α
hinf : s.Infinite
this : Infinite.{u_4 + 1} (↑s : Type u_4)
inr : ∞ = (↑s.encard : ℝ≥0∞)
inr₁ : ∞ = (↑⊤ : ℝ≥0∞)
⊢ ∑' (x : (↑s : Type u_4)), 1 = (↑s.encard : ℝ≥0∞)
have inr₂ : Eq (α := ℝ≥0∞) ∞ ∞
Tactic: rw [tsum_const_eq_top_of_ne_zero one_ne_zero, encard_eq_top hinf, ENat.toENNReal_top]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_4
⊢ ∑' (x : α), 1 = (↑(ENat.card α) : ℝ≥0∞)
have rw : ∑' (x : (↑univ : Type u_4)), 1 = (↑(ENat.card α) : ℝ≥0∞)
Tactic: rw [← tsum_univ]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_4
c : ℝ≥0∞
⊢ ∑' (x : α), c = (↑(ENat.card α) : ℝ≥0∞) * c
have rw : ∑' (x : (↑univ : Type u_4)), c = (↑(ENat.card α) : ℝ≥0∞) * c
Tactic: rw [← tsum_univ]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Field (goal)
Goal:
α : Type u_1
E : Type u_2
inst : SeminormedCommRing E
inst_1 : NormMulClass E
inst_2 : NormOneClass E
f : α → E
x : E
hfx : HasProd f x
⊢ HasProd (fun (x : α) ↦ ‖f x‖) ‖x‖
have simp : Filter.Tendsto (fun (s : Finset α) ↦ Norm.norm.{u_2} (E := E) (∏ b ∈ s, f b)) (SummationFilter.unconditional α).filter
  (nhds ‖x‖)
Tactic: simp only [HasProd, ← norm_prod]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f g : β → α
a₁ a₂ : α
hf : HasProd f a₁ L
hg : HasProd g a₂ L
⊢ HasProd (fun (b : β) ↦ f b / g b) (a₁ / a₂) L
have simp : HasProd (fun (b : β) ↦ f b * (g b)⁻¹) (a₁ * a₂⁻¹) L
Tactic: simp only [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
a₁ : α
inst_3 : L.LeAtTop
hf : HasProd f a₁ L
b : β
inst_4 : DecidableEq β
a : α
⊢ HasProd (Function.update (β := fun (a : β) ↦ α) f b a) (a / f b * a₁) L
have h : ∀ (b' : β), Function.update (β := fun (a : β) ↦ α) f b a b' = (if b' = b then a / f b else 1) * f b'
Tactic: convert! (hasProd_ite_eq b (a / f b) (L := L)).mul hf with b'
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
a₁ : α
inst_3 : L.LeAtTop
hf : HasProd f a₁ L
b : β
inst_4 : DecidableEq β
a : α
b' : β
⊢ Function.update (β := fun (a : β) ↦ α) f b a b' = (if b' = b then a / f b else 1) * f b'
have pos : ∀ (h : b' = b), Function.update (β := fun (a : β) ↦ α) f b a b' = (if b' = b then a / f b else 1) * f b'
Tactic: by_cases h : b' = b
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
a₁ : α
inst_3 : L.LeAtTop
hf : HasProd f a₁ L
b : β
inst_4 : DecidableEq β
a : α
b' : β
pos : ∀ (h : b' = b), Function.update (β := fun (a : β) ↦ α) f b a b' = (if b' = b then a / f b else 1) * f b'
⊢ Function.update (β := fun (a : β) ↦ α) f b a b' = (if b' = b then a / f b else 1) * f b'
have neg : ∀ (h : ¬b' = b), Function.update (β := fun (a : β) ↦ α) f b a b' = (if b' = b then a / f b else 1) * f b'
Tactic: by_cases h : b' = b
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
a₁ : α
inst_3 : L.LeAtTop
hf : HasProd f a₁ L
b : β
inst_4 : DecidableEq β
a : α
b' : β
h : b' = b
⊢ Function.update (β := fun (a : β) ↦ α) f b a b' = (if b' = b then a / f b else 1) * f b'
have pos : a = (if b = b then a / f b else 1) * f b
Tactic: rw [h, update_self]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
a₁ a₂ : α
s : Set β
hf : HasProd (β := (↑s : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s)) a₁
⊢ HasProd (β := (↑sᶜ : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ sᶜ)) a₂ ↔ HasProd f (a₁ * a₂)
have refine : ∀ (h : HasProd f (a₁ * a₂)), HasProd (β := (↑sᶜ : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ sᶜ)) a₂
Tactic: refine ⟨fun h ↦ hf.mul_compl h, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
a₁ a₂ : α
s : Set β
hf : HasProd (β := (↑s : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s)) a₁
h : HasProd f (a₁ * a₂)
⊢ HasProd (β := (↑sᶜ : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ sᶜ)) a₂
have rw : ∀ (hf : HasProd (s.mulIndicator f) a₁) (h : HasProd f (a₁ * a₂)), HasProd (sᶜ.mulIndicator f) a₂
Tactic: rw [hasProd_subtype_iff_mulIndicator] at hf ⊢
Cleared hypotheses: hf, h
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
a₁ a₂ : α
s : Set β
hf : HasProd (s.mulIndicator f) a₁
h : HasProd f (a₁ * a₂)
⊢ HasProd (sᶜ.mulIndicator f) a₂
have rw : HasProd (f * (s.mulIndicator f)⁻¹) a₂
Tactic: rw [Set.mulIndicator_compl]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
a₁ a₂ : α
s : Set β
hf : HasProd (β := (↑s : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s)) a₁
⊢ HasProd f (a₁ * (a₂ / a₁)) ↔ HasProd f a₂
have rw : HasProd f a₂ ↔ HasProd f a₂
Tactic: rw [mul_div_cancel]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
a : α
s : Finset β
⊢ HasProd f ((∏ b ∈ s, f b) * a) ↔ HasProd f (a * ∏ i ∈ s, f i)
have rw : HasProd f (a * ∏ b ∈ s, f b) ↔ HasProd f (a * ∏ i ∈ s, f i)
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
a : α
inst_3 : L.LeAtTop
inst_4 : DecidableEq β
hf : HasProd f a L
b : β
⊢ HasProd (fun (n : β) ↦ if n = b then 1 else f n) (a / f b) L
have h : (fun (n : β) ↦ if n = b then 1 else f n) = update (β := fun (a : β) ↦ α) f b 1
Tactic: convert! hf.update b 1 using 1
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
a : α
inst_3 : L.LeAtTop
inst_4 : DecidableEq β
hf : HasProd f a L
b : β
h : (fun (n : β) ↦ if n = b then 1 else f n) = update (β := fun (a : β) ↦ α) f b 1
⊢ HasProd (fun (n : β) ↦ if n = b then 1 else f n) (a / f b) L
have h₁ : a / f b = 1 / f b * a
Tactic: convert! hf.update b 1 using 1
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
a : α
inst_3 : L.LeAtTop
inst_4 : DecidableEq β
hf : HasProd f a L
b : β
⊢ (fun (n : β) ↦ if n = b then 1 else f n) = update (β := fun (a : β) ↦ α) f b 1
have h : ∀ (n : β), (if n = b then 1 else f n) = update (β := fun (a : β) ↦ α) f b 1 n
Tactic: ext n