awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0∞
h₀ : ∀ (i : α), f i ≤ 1
⊢ HasProd f (⨅ (s : Finset α), ∏ i ∈ s, f i)

Tactic:
tendsto_atTop_iInf (Finset.prod_anti_set_of_le_one' h₀)

Premises used: iInf, HasProd, Finset.prod_anti_set_of_le_one', Filter.atTop, tendsto_atTop_iInf
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0∞
h₀ : ∀ (i : α), f i ≤ 1
⊢ Eq (α := ℝ≥0∞) (∏' (i : α), f i) (⨅ (s : Finset α), ∏ i ∈ s, f i)

Tactic:
(hasProd_iInf_prod h₀).tprod_eq

Premises used: HasProd.tprod_eq, ENNReal.hasProd_iInf_prod
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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

Tactic:
EMetric.cauchySeq_iff_NNReal.2 fun ε εpos ↦ ?_

Premises used: Iff.mpr, EMetric.cauchySeq_iff_NNReal
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ (↑(d n) : ℝ≥0∞)
hd : Summable d
refine : ∀ (ε : ℝ≥0) (εpos : 0 < ε), ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → edist (f n) (f N) < (↑ε : ℝ≥0∞)
⊢ CauchySeq f

Tactic:
refine EMetric.cauchySeq_iff_NNReal.2 fun ε εpos ↦ ?_

Premises used: Iff.mpr, EMetric.cauchySeq_iff_NNReal
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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 < ε
⊢ 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
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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∞)

Tactic:
(Metric.cauchySeq_iff'.1 hd ε (NNReal.coe_pos.2 εpos)).imp fun N hN n hn ↦ ?_

Premises used: Iff.mpr, Exists.imp, Iff.mp, NNReal.coe_pos, Metric.cauchySeq_iff', NNReal.toReal
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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
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∞)
⊢ ∃ (N : ℕ), ∀ (n : ℕ), 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 ↦ ?_

Premises used: Iff.mpr, Exists.imp, Iff.mp, NNReal.coe_pos, Metric.cauchySeq_iff', NNReal.toReal
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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
⊢ dist (α := ℝ≥0) (∑ x ∈ Finset.range n, d x) (∑ x ∈ Finset.range N, d x) < (↑ε : ℝ)

Tactic:
specialize hN n hn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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) < (↑ε : ℝ)
⊢ ∑ 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

Premises used: Finset.sum_range_add_sum_Ico, add_tsub_cancel_left, max_lt_iff, dist_nndist, NNReal.nndist_eq, NNReal.coe_lt_coe
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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) < ε
rw : edist (f N) (f n) < (↑ε : ℝ≥0∞)
⊢ edist (f n) (f N) < (↑ε : ℝ≥0∞)

Tactic:
rw [edist_comm]

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

Tactic:
lt_of_le_of_lt (edist_le_Ico_sum_of_edist_le hn fun _ _ ↦ hf _) ?_

Premises used: lt_of_le_of_lt, edist_le_Ico_sum_of_edist_le
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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) < ε
refine : ∑ i ∈ Finset.Ico N n, (↑(d i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)
⊢ edist (f N) (f n) < (↑ε : ℝ≥0∞)

Tactic:
refine lt_of_le_of_lt (edist_le_Ico_sum_of_edist_le hn fun _ _ ↦ hf _) ?_

Premises used: lt_of_le_of_lt, edist_le_Ico_sum_of_edist_le, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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) < ε
⊢ ∑ i ∈ Finset.Ico N n, (↑(d i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)

Tactic:
mod_cast hN.1

Premises used: ENNReal.ofNNReal, congrArg, cast, ENNReal.coe_lt_coe._simp_1, ENNReal.coe_finsetSum._simp_1, And.left, LT.lt, congrFun', Eq.symm, Eq.trans
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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) < ε
⊢ ∑ i ∈ Finset.Ico N n, (↑(d i) : ℝ≥0∞) < (↑ε : ℝ≥0∞)

Tactic:
exact mod_cast hN.1

Premises used: And.left
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n
hd : tsum d ≠ ∞
⊢ ∀ (i : ℕ), d i ≠ ∞

Tactic:
fun i => ENNReal.ne_top_of_tsum_ne_top hd i

Premises used: ENNReal.ne_top_of_tsum_ne_top
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n
hd : tsum d ≠ ∞
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
⊢ CauchySeq f

Tactic:
lift d to ℕ → NNReal using fun i => ENNReal.ne_top_of_tsum_ne_top hd i

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

Tactic:
rw [ENNReal.tsum_coe_ne_top_iff_summable] at hd

Premises used: ENNReal.tsum_coe_ne_top_iff_summable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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 : Summable d
⊢ CauchySeq f

Tactic:
cauchySeq_of_edist_le_of_summable d hf hd

Premises used: cauchySeq_of_edist_le_of_summable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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 : Summable d
⊢ CauchySeq f

Tactic:
exact cauchySeq_of_edist_le_of_summable d hf hd

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

Tactic:
le_of_tendsto (tendsto_const_nhds.edist ha) (mem_atTop_sets.2 ⟨n, fun m hnm => ?_⟩)

Premises used: Iff.mpr, tendsto_const_nhds, Filter.mem_atTop_sets, le_of_tendsto, Exists.intro, Filter.Tendsto.edist
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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 : ℕ
refine :
  ∀ (m : ℕ) (hnm : m ≥ n),
    Membership.mem (γ := Set ℕ) {x : ℕ | (fun (c : ℕ) ↦ edist (f n) (f c) ≤ ∑' (m : ℕ), d (n + m)) x} m
⊢ edist (f n) a ≤ ∑' (m : ℕ), d (n + m)

Tactic:
refine le_of_tendsto (tendsto_const_nhds.edist ha) (mem_atTop_sets.2 ⟨n, fun m hnm => ?_⟩)

Premises used: Iff.mpr, tendsto_const_nhds, Filter.mem_atTop_sets, le_of_tendsto, Exists.intro, Filter.Tendsto.edist
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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)

Tactic:
le_trans (edist_le_Ico_sum_of_edist_le hnm fun _ _ => hf _) ?_

Premises used: edist_le_Ico_sum_of_edist_le, le_trans
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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
refine : LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.Ico n m, d i) (∑' (m : ℕ), d (n + m))
⊢ edist (f n) (f m) ≤ ∑' (m : ℕ), d (n + m)

Tactic:
refine le_trans (edist_le_Ico_sum_of_edist_le hnm fun _ _ => hf _) ?_

Premises used: edist_le_Ico_sum_of_edist_le, HAdd.hAdd, OfNat.ofNat, le_trans
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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
rw : LE.le (α := ℝ≥0∞) (∑ k ∈ Finset.range (m - n), d (n + k)) (∑' (m : ℕ), d (n + m))
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.Ico n m, d i) (∑' (m : ℕ), d (n + m))

Tactic:
rw [Finset.sum_Ico_eq_sum_range]

Premises used: Finset.sum_Ico_eq_sum_range
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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∞) (∑ k ∈ Finset.range (m - n), d (n + k)) (∑' (m : ℕ), d (n + m))

Tactic:
ENNReal.summable.sum_le_tsum _ (fun _ _ => zero_le)

Premises used: zero_le, ENNReal.summable, Summable.sum_le_tsum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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∞) (∑ k ∈ Finset.range (m - n), d (n + k)) (∑' (m : ℕ), d (n + m))

Tactic:
exact ENNReal.summable.sum_le_tsum _ (fun _ _ => zero_le)

Premises used: zero_le, ENNReal.summable, Summable.sum_le_tsum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
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)
⊢ edist (f 0) a ≤ ∑' (m : ℕ), d m

Tactic:
simpa using edist_le_tsum_of_edist_le_of_tendsto d hf ha 0

Premises used: edist_le_tsum_of_edist_le_of_tendsto, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_4
s : Set α
inl : ∀ (hfin : s.Finite), ∑' (x : (↑s : Type u_4)), 1 = (↑s.encard : ℝ≥0∞)
inr : ∀ (hinf : s.Infinite), ∑' (x : (↑s : Type u_4)), 1 = (↑s.encard : ℝ≥0∞)
⊢ ∑' (x : (↑s : Type u_4)), 1 = (↑s.encard : ℝ≥0∞)

Tactic:
obtain (hfin | hinf) := Set.finite_or_infinite s

Premises used: Set.finite_or_infinite
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_4
s : Set α
hfin : s.Finite
⊢ s.Finite

Tactic:
hfin
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_4
s : Set α
hfin : s.Finite
inl : ∀ (s : Finset α), ∑' (x : (↑(↑s : Set α) : Type u_4)), 1 = (↑(↑s : Set α).encard : ℝ≥0∞)
⊢ ∑' (x : (↑s : Type u_4)), 1 = (↑s.encard : ℝ≥0∞)

Tactic:
lift s to Finset α using hfin

Premises used: Finset
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_4
s : Finset α
⊢ ∑' (x : (↑(↑s : Set α) : Type u_4)), 1 = (↑(↑s : Set α).encard : ℝ≥0∞)

Tactic:
simp [tsum_fintype]

Premises used: tsum_fintype
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_4
s : Set α
hinf : s.Infinite
⊢ Infinite.{u_4 + 1} (↑s : Type u_4)

Tactic:
have : Infinite s := infinite_coe_iff.mpr hinf
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_4
s : Set α
hinf : s.Infinite
this : Infinite.{u_4 + 1} (↑s : Type u_4)
inr : ∞ = (↑s.encard : ℝ≥0∞)
inr₁ : ∞ = (↑⊤ : ℝ≥0∞)
inr₂ inr₃ : Eq (α := ℝ≥0∞) ∞ ∞
⊢ ∑' (x : (↑s : Type u_4)), 1 = (↑s.encard : ℝ≥0∞)

Tactic:
rw [tsum_const_eq_top_of_ne_zero one_ne_zero, encard_eq_top hinf, ENat.toENNReal_top]

Premises used: ENNReal.tsum_const_eq_top_of_ne_zero, ENat.toENNReal_top, Set.encard_eq_top, one_ne_zero
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_4
s : Set α
c : ℝ≥0∞
⊢ ∑' (x : (↑s : Type u_4)), c = (↑s.encard : ℝ≥0∞) * c

Tactic:
simp [← tsum_set_one, ← ENNReal.tsum_mul_right]

Premises used: ENNReal.tsum_set_one, ENNReal.tsum_mul_right
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_4
rw : ∑' (x : (↑univ : Type u_4)), 1 = (↑(ENat.card α) : ℝ≥0∞)
⊢ ∑' (x : α), 1 = (↑(ENat.card α) : ℝ≥0∞)

Tactic:
rw [← tsum_univ]

Premises used: tsum_univ
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_4
⊢ ∑' (x : (↑univ : Type u_4)), 1 = (↑(ENat.card α) : ℝ≥0∞)

Tactic:
simpa [encard_univ] using tsum_set_one univ

Premises used: Set.univ, ENNReal.tsum_set_one, Set.encard_univ
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_4
c : ℝ≥0∞
rw : ∑' (x : (↑univ : Type u_4)), c = (↑(ENat.card α) : ℝ≥0∞) * c
⊢ ∑' (x : α), c = (↑(ENat.card α) : ℝ≥0∞) * c

Tactic:
rw [← tsum_univ]

Premises used: tsum_univ
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_4
c : ℝ≥0∞
⊢ ∑' (x : (↑univ : Type u_4)), c = (↑(ENat.card α) : ℝ≥0∞) * c

Tactic:
simpa [encard_univ] using tsum_set_const univ c

Premises used: ENNReal.tsum_set_const, Set.univ, Set.encard_univ
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Field
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
simp :
  Filter.Tendsto (fun (s : Finset α) ↦ Norm.norm.{u_2} (E := E) (∏ b ∈ s, f b)) (SummationFilter.unconditional α).filter
    (nhds ‖x‖)
⊢ HasProd (fun (x : α) ↦ ‖f x‖) ‖x‖

Tactic:
simp only [HasProd, ← norm_prod]

Premises used: HasProd, norm_prod, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Field
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
⊢ Filter.Tendsto (fun (s : Finset α) ↦ Norm.norm.{u_2} (E := E) (∏ b ∈ s, f b)) (SummationFilter.unconditional α).filter
    (nhds ‖x‖)

Tactic:
hfx.norm

Premises used: Filter.Tendsto.norm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Field
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
⊢ Filter.Tendsto (fun (s : Finset α) ↦ Norm.norm.{u_2} (E := E) (∏ b ∈ s, f b)) (SummationFilter.unconditional α).filter
    (nhds ‖x‖)

Tactic:
exact hfx.norm

Premises used: HasProd.norm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Field
Goal:
α : Type u_1
E : Type u_2
inst : SeminormedCommRing E
inst_1 : NormMulClass E
inst_2 : NormOneClass E
f : α → E
hf : Multipliable f
⊢ Multipliable (α := ℝ) fun (x : α) ↦ ‖f x‖

Tactic:
let ⟨x, hx⟩ := hf; ⟨‖x‖, hx.norm⟩

Premises used: Norm.norm, Multipliable, Exists.intro, _private.0.Multipliable.norm.match_1, HasProd.norm, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Field
Goal:
α : Type u_1
E : Type u_2
inst : SeminormedCommRing E
inst_1 : NormMulClass E
inst_2 : NormOneClass E
f : α → E
hf : Multipliable f
⊢ Norm.norm.{u_2} (E := E) (∏' (i : α), f i) = ∏' (i : α), ‖f i‖

Tactic:
hf.hasProd.norm.tprod_eq.symm

Premises used: HasProd.tprod_eq, Multipliable.hasProd, Eq.symm, HasProd.norm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
a : α
h : HasProd f a L
⊢ HasProd (fun (b : β) ↦ (f b)⁻¹) a⁻¹ L

Tactic:
simpa only using h.map (MonoidHom.id α)⁻¹ continuous_inv

Premises used: HasProd.map, Inv.inv, MonoidHom.id, ContinuousInv.continuous_inv
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
hf : Multipliable f L
⊢ Multipliable.{u_1, u_2} (α := α) (fun (b : β) ↦ (f b)⁻¹) L

Tactic:
hf.hasProd.inv.multipliable

Premises used: Multipliable.hasProd, HasProd.inv, HasProd.multipliable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
hf : Multipliable.{u_1, u_2} (α := α) (fun (b : β) ↦ (f b)⁻¹) L
⊢ Multipliable f L

Tactic:
simpa only [inv_inv] using hf.inv

Premises used: Multipliable.inv, inv_inv
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
⊢ Multipliable.{u_1, u_2} (α := α) (fun (b : β) ↦ (f b)⁻¹) L ↔ Multipliable f L

Tactic:
⟨Multipliable.of_inv, Multipliable.inv⟩

Premises used: Multipliable.inv, Iff.intro, Multipliable.of_inv
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
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
simp : HasProd (fun (b : β) ↦ f b * (g b)⁻¹) (a₁ * a₂⁻¹) L
⊢ HasProd (fun (b : β) ↦ f b / g b) (a₁ / a₂) L

Tactic:
simp only [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
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

Tactic:
hf.mul hg.inv

Premises used: HasProd.inv, HasProd.mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
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

Tactic:
exact hf.mul hg.inv

Premises used: HasProd.inv, HasProd.mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f g : β → α
hf : Multipliable f L
hg : Multipliable g L
⊢ Multipliable.{u_1, u_2} (α := α) (fun (b : β) ↦ f b / g b) L

Tactic:
(hf.hasProd.div hg.hasProd).multipliable

Premises used: HasProd.div, Multipliable.hasProd, HasProd.multipliable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f g : β → α
hg : Multipliable g L
hfg : Multipliable.{u_1, u_2} (α := α) (fun (b : β) ↦ f b / g b) L
⊢ Multipliable f L

Tactic:
simpa only [div_mul_cancel] using hfg.mul hg

Premises used: div_mul_cancel, Multipliable.mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f g : β → α
hfg : Multipliable.{u_1, u_2} (α := α) (fun (b : β) ↦ f b / g b) L
hf : Multipliable f L
⊢ Multipliable.{u_1, u_2} (α := α) (fun (b : β) ↦ g b / f b) L

Tactic:
simpa only [inv_div] using hfg.inv

Premises used: Multipliable.inv, inv_div
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
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 (fun (b_1 : β) ↦ (if b_1 = b then a / f b else 1) * f b_1) (a / f b * a₁) L

Tactic:
(hasProd_ite_eq b (a / f b) (L := L)).mul hf

Premises used: hasProd_ite_eq, HDiv.hDiv, HasProd.mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
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 : α
h : ∀ (b' : β), Function.update (β := fun (a : β) ↦ α) f b a b' = (if b' = b then a / f b else 1) * f b'
⊢ HasProd (Function.update (β := fun (a : β) ↦ α) f b a) (a / f b * a₁) L

Tactic:
convert! (hasProd_ite_eq b (a / f b) (L := L)).mul hf with b'

Premises used: hasProd_ite_eq, HDiv.hDiv, HasProd.mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
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'
neg : ∀ (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'

Tactic:
by_cases h : b' = b
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
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
pos : a = (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'

Tactic:
rw [h, update_self]

Premises used: Function.update_self