awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : CommSemiring α
inst_1 : TopologicalSpace α
f : ι → α
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
inst_4 : T2Space α
inst_5 : ContinuousAdd α
hsum : Summable.{u_3, u_1} (α := α) fun (i : ι) ↦ f i * ∏ j ∈ Iio i, (1 + f j)
hprod : Multipliable.{u_3, u_1} (α := α) fun (x : ι) ↦ 1 + f x
⊢ ∏' (i : ι), (1 + f i) = HAdd.hAdd (α := α) 1 (∑' (i : ι), f i * ∏ j ∈ Iio i, (1 + f j))
have inl : IsEmpty ι → ∏' (i : ι), (1 + f i) = HAdd.hAdd (α := α) 1 (∑' (i : ι), f i * ∏ j ∈ Iio i, (1 + f j))
Tactic: rcases isEmpty_or_nonempty ι with _ | _
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : CommSemiring α
inst_1 : TopologicalSpace α
f : ι → α
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
inst_4 : T2Space α
inst_5 : ContinuousAdd α
hsum : Summable.{u_3, u_1} (α := α) fun (i : ι) ↦ f i * ∏ j ∈ Iio i, (1 + f j)
hprod : Multipliable.{u_3, u_1} (α := α) fun (x : ι) ↦ 1 + f x
inl : IsEmpty ι → ∏' (i : ι), (1 + f i) = HAdd.hAdd (α := α) 1 (∑' (i : ι), f i * ∏ j ∈ Iio i, (1 + f j))
⊢ ∏' (i : ι), (1 + f i) = HAdd.hAdd (α := α) 1 (∑' (i : ι), f i * ∏ j ∈ Iio i, (1 + f j))
have inr : Nonempty ι → ∏' (i : ι), (1 + f i) = HAdd.hAdd (α := α) 1 (∑' (i : ι), f i * ∏ j ∈ Iio i, (1 + f j))
Tactic: rcases isEmpty_or_nonempty ι with _ | _
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : CommSemiring α
inst_1 : TopologicalSpace α
f : ι → α
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
inst_4 : T2Space α
inst_5 : ContinuousAdd α
hsum : Summable.{u_3, u_1} (α := α) fun (i : ι) ↦ f i * ∏ j ∈ Iio i, (1 + f j)
hprod : Multipliable.{u_3, u_1} (α := α) fun (x : ι) ↦ 1 + f x
h : Nonempty ι
⊢ ∏' (i : ι), (1 + f i) = HAdd.hAdd (α := α) 1 (∑' (i : ι), f i * ∏ j ∈ Iio i, (1 + f j))
have inr : ∀ (x : α) (hx : HasProd (fun (x : ι) ↦ 1 + f x) x),
  ∏' (i : ι), (1 + f i) = HAdd.hAdd (α := α) 1 (∑' (i : ι), f i * ∏ j ∈ Iio i, (1 + f j))
Tactic: obtain ⟨x, hx⟩ := hprod
Cleared hypotheses: hprod
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : CommSemiring α
inst_1 : TopologicalSpace α
f : ι → α
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
inst_4 : T2Space α
inst_5 : ContinuousAdd α
hsum : Summable.{u_3, u_1} (α := α) fun (i : ι) ↦ f i * ∏ j ∈ Iio i, (1 + f j)
h : Nonempty ι
x : α
hx : HasProd (fun (x : ι) ↦ 1 + f x) x
⊢ ∏' (i : ι), (1 + f i) = HAdd.hAdd (α := α) 1 (∑' (i : ι), f i * ∏ j ∈ Iio i, (1 + f j))
have inr : ∀ (a : α) (ha : HasSum (fun (i : ι) ↦ f i * ∏ j ∈ Iio i, (1 + f j)) a),
  ∏' (i : ι), (1 + f i) = HAdd.hAdd (α := α) 1 (∑' (i : ι), f i * ∏ j ∈ Iio i, (1 + f j))
Tactic: obtain ⟨a, ha⟩ := hsum
Cleared hypotheses: hsum
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : CommSemiring α
inst_1 : TopologicalSpace α
f : ι → α
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
inst_4 : T2Space α
inst_5 : ContinuousAdd α
h : Nonempty ι
x : α
hx : HasProd (fun (x : ι) ↦ 1 + f x) x
a : α
ha : HasSum (fun (i : ι) ↦ f i * ∏ j ∈ Iio i, (1 + f j)) a
⊢ ∏' (i : ι), (1 + f i) = HAdd.hAdd (α := α) 1 (∑' (i : ι), f i * ∏ j ∈ Iio i, (1 + f j))
have h : HAdd.hAdd (α := α) 1 (∑' (i : ι), f i * ∏ j ∈ Iio i, (1 + f j)) = x
Tactic: convert! hx.tprod_eq
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : CommSemiring α
inst_1 : TopologicalSpace α
f : ι → α
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
inst_4 : T2Space α
inst_5 : ContinuousAdd α
h : Nonempty ι
x : α
hx : Tendsto (fun (s : Finset ι) ↦ ∏ b ∈ s, (fun (x : ι) ↦ 1 + f x) b) (SummationFilter.unconditional ι).filter (nhds x)
a : α
ha : HasSum (fun (i : ι) ↦ f i * ∏ j ∈ Iio i, (1 + f j)) a
| fun (s : Finset ι) ↦ ∏ b ∈ s, (fun (x : ι) ↦ 1 + f x) b
have h : ∀ (x : Finset ι), ∏ b ∈ x, (fun (x : ι) ↦ 1 + f x) b
Tactic: ext _
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : CommSemiring α
inst_1 : TopologicalSpace α
f : ι → α
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
inst_4 : T2Space α
inst_5 : ContinuousAdd α
h : Nonempty ι
x : α
hx : Tendsto (fun (s : Finset ι) ↦ ∏ b ∈ s, (fun (x : ι) ↦ 1 + f x) b) (SummationFilter.unconditional ι).filter (nhds x)
a : α
ha : HasSum (fun (i : ι) ↦ f i * ∏ j ∈ Iio i, (1 + f j)) a
x_1 : Finset ι
| ∏ b ∈ x_1, (fun (x : ι) ↦ 1 + f x) b
have h : HAdd.hAdd (α := α) 1 (∑ i ∈ x_1, f i * ∏ j ∈ x_1 with j < i, (1 + f j))
Tactic: rw [prod_one_add_ordered]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : CommSemiring α
inst_1 : TopologicalSpace α
f : ι → α
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
inst_4 : T2Space α
inst_5 : ContinuousAdd α
h : Nonempty ι
x : α
hx : Tendsto (fun (s : Finset ι) ↦ ∏ b ∈ s, (fun (x : ι) ↦ 1 + f x) b) (SummationFilter.unconditional ι).filter (nhds x)
a : α
ha : HasSum (fun (i : ι) ↦ f i * ∏ j ∈ Iio i, (1 + f j)) a
| fun (s : Finset ι) ↦ ∏ b ∈ s, (fun (x : ι) ↦ 1 + f x) b
have h : ∀ (x : Finset ι), HAdd.hAdd (α := α) 1 (∑ i ∈ x, f i * ∏ j ∈ x with j < i, (1 + f j))
Tactic: ext _; rw [prod_one_add_ordered]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : CommSemiring α
inst_1 : TopologicalSpace α
f : ι → α
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
inst_4 : T2Space α
inst_5 : ContinuousAdd α
h : Nonempty ι
x : α
hx : Tendsto (fun (s : Finset ι) ↦ ∏ b ∈ s, (fun (x : ι) ↦ 1 + f x) b) (SummationFilter.unconditional ι).filter (nhds x)
a : α
ha : HasSum (fun (i : ι) ↦ f i * ∏ j ∈ Iio i, (1 + f j)) a
⊢ HAdd.hAdd (α := α) 1 (∑' (i : ι), f i * ∏ j ∈ Iio i, (1 + f j)) = x
have h : ∀
  (hx :
    Tendsto (fun (x : Finset ι) ↦ HAdd.hAdd (α := α) 1 (∑ i ∈ x, f i * ∏ j ∈ x with j < i, (1 + f j)))
      (SummationFilter.unconditional ι).filter (nhds x))
  (a : α) (ha : HasSum (fun (i : ι) ↦ f i * ∏ j ∈ Iio i, (1 + f j)) a),
  HAdd.hAdd (α := α) 1 (∑' (i : ι), f i * ∏ j ∈ Iio i, (1 + f j)) = x
Tactic: conv at hx in fun _ ↦ _ => ext _; rw [prod_one_add_ordered]
Cleared hypotheses: hx, a, ha
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : CommSemiring α
inst_1 : TopologicalSpace α
f : ι → α
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
inst_4 : T2Space α
inst_5 : ContinuousAdd α
h : Nonempty ι
x : α
hx :
  Tendsto (fun (x : Finset ι) ↦ HAdd.hAdd (α := α) 1 (∑ i ∈ x, f i * ∏ j ∈ x with j < i, (1 + f j)))
    (SummationFilter.unconditional ι).filter (nhds x)
a : α
ha : HasSum (fun (i : ι) ↦ f i * ∏ j ∈ Iio i, (1 + f j)) a
⊢ HAdd.hAdd (α := α) 1 (∑' (i : ι), f i * ∏ j ∈ Iio i, (1 + f j)) = x
have h : 1 + a = x
Tactic: rw [ha.tsum_eq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : CommSemiring α
inst_1 : TopologicalSpace α
f : ι → α
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
inst_4 : T2Space α
inst_5 : ContinuousAdd α
h : Nonempty ι
x : α
hx :
  Tendsto (fun (x : Finset ι) ↦ HAdd.hAdd (α := α) 1 (∑ i ∈ x, f i * ∏ j ∈ x with j < i, (1 + f j)))
    (SummationFilter.unconditional ι).filter (nhds x)
a : α
ha : HasSum (fun (i : ι) ↦ f i * ∏ j ∈ Iio i, (1 + f j)) a
⊢ 1 + a = x
have h : Tendsto.{u_1, u_3} (α := ι)
  ((fun (x : Finset ι) ↦ HAdd.hAdd (α := α) 1 (∑ i ∈ x, f i * ∏ j ∈ x with j < i, (1 + f j))) ∘ Iic) atTop
  (nhds (1 + a))
Tactic: refine (tendsto_nhds_unique (hx.comp tendsto_finset_Iic_atTop_atTop) ?_).symm
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : CommSemiring α
inst_1 : TopologicalSpace α
f : ι → α
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
inst_4 : T2Space α
inst_5 : ContinuousAdd α
h : Nonempty ι
x : α
hx :
  Tendsto (fun (x : Finset ι) ↦ HAdd.hAdd (α := α) 1 (∑ i ∈ x, f i * ∏ j ∈ x with j < i, (1 + f j)))
    (SummationFilter.unconditional ι).filter (nhds x)
a : α
ha : HasSum (fun (i : ι) ↦ f i * ∏ j ∈ Iio i, (1 + f j)) a
⊢ Tendsto.{u_1, u_3} (α := ι)
    ((fun (x : Finset ι) ↦ HAdd.hAdd (α := α) 1 (∑ i ∈ x, f i * ∏ j ∈ x with j < i, (1 + f j))) ∘ Iic) atTop
    (nhds (1 + a))
have h : Tendsto (fun (x : ι) ↦ ∑ i ∈ Iic x, f i * ∏ j ∈ Iic x with j < i, (1 + f j)) atTop (nhds a)
Tactic: apply Tendsto.const_add
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : CommSemiring α
inst_1 : TopologicalSpace α
f : ι → α
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
inst_4 : T2Space α
inst_5 : ContinuousAdd α
h : Nonempty ι
x : α
hx :
  Tendsto (fun (x : Finset ι) ↦ HAdd.hAdd (α := α) 1 (∑ i ∈ x, f i * ∏ j ∈ x with j < i, (1 + f j)))
    (SummationFilter.unconditional ι).filter (nhds x)
a : α
ha : HasSum (fun (i : ι) ↦ f i * ∏ j ∈ Iio i, (1 + f j)) a
⊢ Tendsto (fun (x : ι) ↦ ∑ i ∈ Iic x, f i * ∏ j ∈ Iic x with j < i, (1 + f j)) atTop (nhds a)
have h : ∀ (s : ι),
  Eq.{u_3 + 1} (α := α) (∑ i ∈ Iic s, f i * ∏ j ∈ Iic s with j < i, (1 + f j))
    (((fun (s : Finset ι) ↦ ∑ b ∈ s, (fun (i : ι) ↦ f i * ∏ j ∈ Iio i, (1 + f j)) b) ∘ Iic) s)
Tactic: convert! ha.comp tendsto_finset_Iic_atTop_atTop using 2 with s
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : CommSemiring α
inst_1 : TopologicalSpace α
f : ι → α
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
inst_4 : T2Space α
inst_5 : ContinuousAdd α
h : Nonempty ι
x : α
hx :
  Tendsto (fun (x : Finset ι) ↦ HAdd.hAdd (α := α) 1 (∑ i ∈ x, f i * ∏ j ∈ x with j < i, (1 + f j)))
    (SummationFilter.unconditional ι).filter (nhds x)
a : α
ha : HasSum (fun (i : ι) ↦ f i * ∏ j ∈ Iio i, (1 + f j)) a
s : ι
⊢ Eq.{u_3 + 1} (α := α) (∑ i ∈ Iic s, f i * ∏ j ∈ Iic s with j < i, (1 + f j))
    (((fun (s : Finset ι) ↦ ∑ b ∈ s, (fun (i : ι) ↦ f i * ∏ j ∈ Iio i, (1 + f j)) b) ∘ Iic) s)
have h : ∀ (i : ι) (hi : i ∈ Iic s), f i * ∏ j ∈ Iic s with j < i, (1 + f j) = (fun (i : ι) ↦ f i * ∏ j ∈ Iio i, (1 + f j)) i
Tactic: refine sum_congr rfl (fun i hi ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : CommSemiring α
inst_1 : TopologicalSpace α
f : ι → α
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
inst_4 : T2Space α
inst_5 : ContinuousAdd α
h : Nonempty ι
x : α
hx :
  Tendsto (fun (x : Finset ι) ↦ HAdd.hAdd (α := α) 1 (∑ i ∈ x, f i * ∏ j ∈ x with j < i, (1 + f j)))
    (SummationFilter.unconditional ι).filter (nhds x)
a : α
ha : HasSum (fun (i : ι) ↦ f i * ∏ j ∈ Iio i, (1 + f j)) a
s i : ι
hi : i ∈ Iic s
⊢ f i * ∏ j ∈ Iic s with j < i, (1 + f j) = (fun (i : ι) ↦ f i * ∏ j ∈ Iio i, (1 + f j)) i
have h : {j ∈ Iic s | j < i} = Iio i
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrderBot ι
α : Type u_4
f : ι → α
inst_2 : CommRing α
inst_3 : TopologicalSpace α
inst_4 : T2Space α
inst_5 : IsTopologicalAddGroup α
hsum : Summable.{u_4, u_1} (α := α) fun (i : ι) ↦ f i * ∏ j ∈ Iio i, (1 - f j)
hprod : Multipliable.{u_4, u_1} (α := α) fun (x : ι) ↦ 1 - f x
⊢ ∏' (i : ι), (1 - f i) = HSub.hSub (α := α) 1 (∑' (i : ι), f i * ∏ j ∈ Iio i, (1 - f j))
have simp_rw : ∀ (hsum : Summable.{u_4, u_1} (α := α) fun (i : ι) ↦ f i * ∏ x ∈ Iio i, (1 + -f x))
  (hprod : Multipliable.{u_4, u_1} (α := α) fun (x : ι) ↦ 1 + -f x),
  ∏' (i : ι), (1 + -f i) = HAdd.hAdd (α := α) 1 (-∑' (i : ι), f i * ∏ i ∈ Iio i, (1 + -f i))
Tactic: simp_rw [sub_eq_add_neg] at hsum hprod ⊢
Cleared hypotheses: hsum, hprod
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (hypothesis)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrderBot ι
α : Type u_4
f : ι → α
inst_2 : CommRing α
inst_3 : TopologicalSpace α
inst_4 : T2Space α
inst_5 : IsTopologicalAddGroup α
hsum : Summable.{u_4, u_1} (α := α) fun (i : ι) ↦ f i * ∏ x ∈ Iio i, (1 + -f x)
hprod : Multipliable.{u_4, u_1} (α := α) fun (x : ι) ↦ 1 + -f x
⊢ ∏' (i : ι), (1 + -f i) = HAdd.hAdd (α := α) 1 (-∑' (i : ι), f i * ∏ i ∈ Iio i, (1 + -f i))
have hsum' : Summable.{u_4, u_1} (α := α) fun (b : ι) ↦ -(f b * ∏ x ∈ Iio b, (1 + -f x))
Tactic: obtain hsum' := hsum.neg
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (hypothesis)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrderBot ι
α : Type u_4
f : ι → α
inst_2 : CommRing α
inst_3 : TopologicalSpace α
inst_4 : T2Space α
inst_5 : IsTopologicalAddGroup α
hsum : Summable.{u_4, u_1} (α := α) fun (i : ι) ↦ f i * ∏ x ∈ Iio i, (1 + -f x)
hprod : Multipliable.{u_4, u_1} (α := α) fun (x : ι) ↦ 1 + -f x
hsum' : Summable.{u_4, u_1} (α := α) fun (b : ι) ↦ -(f b * ∏ x ∈ Iio b, (1 + -f x))
⊢ ∏' (i : ι), (1 + -f i) = HAdd.hAdd (α := α) 1 (-∑' (i : ι), f i * ∏ i ∈ Iio i, (1 + -f i))
have hsum'₁ : Summable.{u_4, u_1} (α := α) fun (b : ι) ↦ -f b * ∏ x ∈ Iio b, (1 + -f x)
Tactic: simp_rw [← neg_mul] at hsum'
Cleared hypotheses: hsum'
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrderBot ι
α : Type u_4
f : ι → α
inst_2 : CommRing α
inst_3 : TopologicalSpace α
inst_4 : T2Space α
inst_5 : IsTopologicalAddGroup α
hsum : Summable.{u_4, u_1} (α := α) fun (i : ι) ↦ f i * ∏ x ∈ Iio i, (1 + -f x)
hprod : Multipliable.{u_4, u_1} (α := α) fun (x : ι) ↦ 1 + -f x
hsum' : Summable.{u_4, u_1} (α := α) fun (b : ι) ↦ -f b * ∏ x ∈ Iio b, (1 + -f x)
⊢ ∏' (i : ι), (1 + -f i) = HAdd.hAdd (α := α) 1 (-∑' (i : ι), f i * ∏ i ∈ Iio i, (1 + -f i))
have simp_rw : ∏' (i : ι), (1 + -f i) = HAdd.hAdd (α := α) 1 (∑' (b : ι), -f b * ∏ i ∈ Iio b, (1 + -f i))
Tactic: simp_rw [← tsum_neg, ← neg_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
inst_2 : TopologicalSpace β
inst_3 : LocallyCompactSpace β
f : α → β → F
s : Set β
hs : IsOpen[inst_2] s
hu : ∀ K ⊆ s, IsCompact K → ∃ (u : α → ℝ), Summable u ∧ ∀ᶠ (n : α) in cofinite, ∀ k ∈ K, ‖f n k‖ ≤ u n
⊢ SummableLocallyUniformlyOn f s
have apply : HasSumLocallyUniformlyOn f (fun (x : β) ↦ ∑' (n : α), f n x) s
Tactic: apply HasSumLocallyUniformlyOn.summableLocallyUniformlyOn (g := fun x ↦ ∑' n, f n x)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
inst_2 : TopologicalSpace β
inst_3 : LocallyCompactSpace β
f : α → β → F
s : Set β
hs : IsOpen[inst_2] s
hu : ∀ K ⊆ s, IsCompact K → ∃ (u : α → ℝ), Summable u ∧ ∀ᶠ (n : α) in cofinite, ∀ k ∈ K, ‖f n k‖ ≤ u n
⊢ HasSumLocallyUniformlyOn f (fun (x : β) ↦ ∑' (n : α), f n x) s
have rw : ∀ K ⊆ s,
  IsCompact K →
    TendstoUniformlyOn.{u_2, u_3, u_1} (β := F) (fun (x1 : Finset α) (x2 : β) ↦ ∑ i ∈ x1, f i x2)
      (fun (x : β) ↦ ∑' (n : α), f n x) atTop K
Tactic: rw [hasSumLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn,
    tendstoLocallyUniformlyOn_iff_forall_isCompact hs]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
inst_2 : TopologicalSpace β
inst_3 : LocallyCompactSpace β
f : α → β → F
s : Set β
hs : IsOpen[inst_2] s
hu : ∀ K ⊆ s, IsCompact K → ∃ (u : α → ℝ), Summable u ∧ ∀ᶠ (n : α) in cofinite, ∀ k ∈ K, ‖f n k‖ ≤ u n
K : Set β
hK : K ⊆ s
hKc : IsCompact K
⊢ TendstoUniformlyOn.{u_2, u_3, u_1} (β := F) (fun (x1 : Finset α) (x2 : β) ↦ ∑ i ∈ x1, f i x2)
    (fun (x : β) ↦ ∑' (n : α), f n x) atTop K
have obtain : ∀ (u : α → ℝ) (hu1 : Summable u) (hu2 : ∀ᶠ (n : α) in cofinite, ∀ k ∈ K, ‖f n k‖ ≤ u n),
  TendstoUniformlyOn.{u_2, u_3, u_1} (β := F) (fun (x1 : Finset α) (x2 : β) ↦ ∑ i ∈ x1, f i x2)
    (fun (x : β) ↦ ∑' (n : α), f n x) atTop K
Tactic: obtain ⟨u, hu1, hu2⟩ := hu K hK hKc
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
inst_2 : TopologicalSpace β
inst_3 : LocallyCompactSpace β
f : α → β → F
s : Set β
hs : IsOpen[inst_2] s
hu : ∀ K ⊆ s, IsCompact K → ∃ (u : α → ℝ), Summable u ∧ ∀ (n : α), ∀ k ∈ K, ‖f n k‖ ≤ u n
⊢ SummableLocallyUniformlyOn f s
have apply : ∀ K ⊆ s, IsCompact K → ∃ (u : α → ℝ), Summable u ∧ ∀ᶠ (n : α) in cofinite, ∀ k ∈ K, ‖f n k‖ ≤ u n
Tactic: apply SummableLocallyUniformlyOn.of_locally_bounded_eventually hs
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
inst_2 : TopologicalSpace β
inst_3 : LocallyCompactSpace β
f : α → β → F
s : Set β
hs : IsOpen[inst_2] s
hu : ∀ K ⊆ s, IsCompact K → ∃ (u : α → ℝ), Summable u ∧ ∀ (n : α), ∀ k ∈ K, ‖f n k‖ ≤ u n
K : Set β
hK : K ⊆ s
hKc : IsCompact K
⊢ ∃ (u : α → ℝ), Summable u ∧ ∀ᶠ (n : α) in cofinite, ∀ k ∈ K, ‖f n k‖ ≤ u n
have obtain : ∀ (u : α → ℝ) (hu1 : Summable u) (hu2 : ∀ (n : α), ∀ k ∈ K, ‖f n k‖ ≤ u n),
  ∃ (u : α → ℝ), Summable u ∧ ∀ᶠ (n : α) in cofinite, ∀ k ∈ K, ‖f n k‖ ≤ u n
Tactic: obtain ⟨u, hu1, hu2⟩ := hu K hK hKc
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
inst_2 : TopologicalSpace β
inst_3 : LocallyCompactSpace β
f : α → β → F
s : Set β
hs : IsOpen[inst_2] s
hu : ∀ K ⊆ s, IsCompact K → ∃ (u : α → ℝ), Summable u ∧ ∀ (n : α), ∀ k ∈ K, ‖f n k‖ ≤ u n
K : Set β
hK : K ⊆ s
hKc : IsCompact K
u : α → ℝ
hu1 : Summable u
hu2 : ∀ (n : α), ∀ k ∈ K, ‖f n k‖ ≤ u n
⊢ ∀ᶠ (n : α) in cofinite, ∀ k ∈ K, ‖f n k‖ ≤ u n
have h : ∀ (a : α), Membership.mem (γ := Set α) {x : α | (fun (n : α) ↦ ∀ k ∈ K, ‖f n k‖ ≤ u n) x} a
Tactic: filter_upwards using hu2
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
s : Set 𝕜
f : ι → 𝕜 → F
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : 𝕜
hx : x ∈ s
hf : ∀ y ∈ s, Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ f n y
h : SummableLocallyUniformlyOn.{u_3, u_2, u_1} (α := F) (fun (n : ι) ↦ derivWithin (fun (z : 𝕜) ↦ f n z) s) s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt 𝕜 (f n) r
⊢ Eq.{u_3 + 1} (α := F) (derivWithin (fun (z : 𝕜) ↦ ∑' (n : ι), f n z) s x) (∑' (n : ι), derivWithin (f n) s x)
have apply : HasDerivWithinAt.{u_2, u_3} (F := F) (fun (z : 𝕜) ↦ ∑' (n : ι), f n z) (∑' (n : ι), derivWithin (f n) s x) s x
Tactic: apply HasDerivWithinAt.derivWithin ?_ (hs.uniqueDiffWithinAt hx)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
s : Set 𝕜
f : ι → 𝕜 → F
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : 𝕜
hx : x ∈ s
hf : ∀ y ∈ s, Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ f n y
h : SummableLocallyUniformlyOn.{u_3, u_2, u_1} (α := F) (fun (n : ι) ↦ derivWithin (fun (z : 𝕜) ↦ f n z) s) s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt 𝕜 (f n) r
⊢ HasDerivWithinAt.{u_2, u_3} (F := F) (fun (z : 𝕜) ↦ ∑' (n : ι), f n z) (∑' (n : ι), derivWithin (f n) s x) s x
have h₁ : HasDerivAt.{u_2, u_3} (F := F) (fun (z : 𝕜) ↦ ∑' (n : ι), f n z) (∑' (n : ι), derivWithin (f n) s x) x
Tactic: apply HasDerivAt.hasDerivWithinAt
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
s : Set 𝕜
f : ι → 𝕜 → F
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : 𝕜
hx : x ∈ s
hf : ∀ y ∈ s, Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ f n y
h : SummableLocallyUniformlyOn.{u_3, u_2, u_1} (α := F) (fun (n : ι) ↦ derivWithin (fun (z : 𝕜) ↦ f n z) s) s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt 𝕜 (f n) r
⊢ HasDerivAt.{u_2, u_3} (F := F) (fun (z : 𝕜) ↦ ∑' (n : ι), f n z) (∑' (n : ι), derivWithin (f n) s x) x
have apply : TendstoLocallyUniformlyOn.{u_2, u_3, u_1} (β := F)
  (fun (n : Finset ι) (a : 𝕜) ↦ ∑ i ∈ n, derivWithin (fun (z : 𝕜) ↦ f i z) s a)
  (fun {x : 𝕜} ↦ ∑' (n : ι), derivWithin (f n) s x) (SummationFilter.unconditional ι).filter s
Tactic: apply hasDerivAt_of_tendstoLocallyUniformlyOn hs _ _ (fun y hy ↦ (hf y hy).hasSum) hx
    (f' := fun n : Finset ι ↦ fun a ↦ ∑ i ∈ n, derivWithin (fun z ↦ f i z) s a)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
s : Set 𝕜
f : ι → 𝕜 → F
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : 𝕜
hx : x ∈ s
hf : ∀ y ∈ s, Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ f n y
h : SummableLocallyUniformlyOn.{u_3, u_2, u_1} (α := F) (fun (n : ι) ↦ derivWithin (fun (z : 𝕜) ↦ f n z) s) s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt 𝕜 (f n) r
apply :
  TendstoLocallyUniformlyOn.{u_2, u_3, u_1} (β := F)
    (fun (n : Finset ι) (a : 𝕜) ↦ ∑ i ∈ n, derivWithin (fun (z : 𝕜) ↦ f i z) s a)
    (fun {x : 𝕜} ↦ ∑' (n : ι), derivWithin (f n) s x) (SummationFilter.unconditional ι).filter s
⊢ HasDerivAt.{u_2, u_3} (F := F) (fun (z : 𝕜) ↦ ∑' (n : ι), f n z) (∑' (n : ι), derivWithin (f n) s x) x
have apply₁ : ∀ᶠ (n : Finset ι) in (SummationFilter.unconditional ι).filter,
  ∀ x ∈ s,
    HasDerivAt.{u_2, u_3} (F := F) (fun (y : 𝕜) ↦ ∑ b ∈ n, (fun (n : ι) ↦ f n y) b)
      ((fun (n : Finset ι) (a : 𝕜) ↦ (∑ i ∈ n, derivWithin (fun (z : 𝕜) ↦ f i z) s a : F)) n x) x
Tactic: apply hasDerivAt_of_tendstoLocallyUniformlyOn hs _ _ (fun y hy ↦ (hf y hy).hasSum) hx
    (f' := fun n : Finset ι ↦ fun a ↦ ∑ i ∈ n, derivWithin (fun z ↦ f i z) s a)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
s : Set 𝕜
f : ι → 𝕜 → F
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : 𝕜
hx : x ∈ s
hf : ∀ y ∈ s, Summable.{u_3, u_1} (α := F) fun (n : ι) ↦ f n y
h : SummableLocallyUniformlyOn.{u_3, u_2, u_1} (α := F) (fun (n : ι) ↦ derivWithin (fun (z : 𝕜) ↦ f n z) s) s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt 𝕜 (f n) r
⊢ TendstoLocallyUniformlyOn.{u_2, u_3, u_1} (β := F)
    (fun (n : Finset ι) (a : 𝕜) ↦ ∑ i ∈ n, derivWithin (fun (z : 𝕜) ↦ f i z) s a)
    (fun {x : 𝕜} ↦ ∑' (n : ι), derivWithin (f n) s x) (SummationFilter.unconditional ι).filter s
have obtain : ∀ (g : 𝕜 → F) (hg : HasSumLocallyUniformlyOn (fun (n : ι) ↦ derivWithin (fun (z : 𝕜) ↦ f n z) s) g s),
  TendstoLocallyUniformlyOn.{u_2, u_3, u_1} (β := F)
    (fun (n : Finset ι) (a : 𝕜) ↦ ∑ i ∈ n, derivWithin (fun (z : 𝕜) ↦ f i z) s a)
    (fun {x : 𝕜} ↦ ∑' (n : ι), derivWithin (f n) s x) (SummationFilter.unconditional ι).filter s
Tactic: obtain ⟨g, hg⟩ := h
Cleared hypotheses: h