awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
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_1 : 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
h : ∀ (x : Finset ι), ∏ b ∈ x, (fun (x : ι) ↦ 1 + f x) b
| fun (s : Finset ι) ↦ ∏ b ∈ s, (fun (x : ι) ↦ 1 + f x) b

Tactic:
ext _
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
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_1 : 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 ι
h : HAdd.hAdd (α := α) 1 (∑ i ∈ x_1, f i * ∏ j ∈ x_1 with j < i, (1 + f j))
| ∏ b ∈ x_1, (fun (x : ι) ↦ 1 + f x) b

Tactic:
rw [prod_one_add_ordered]

Premises used: Finset.prod_one_add_ordered
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
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_1 : 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
h : ∀ (x : Finset ι), HAdd.hAdd (α := α) 1 (∑ i ∈ x, f i * ∏ j ∈ x with j < i, (1 + f j))
| fun (s : Finset ι) ↦ ∏ b ∈ s, (fun (x : ι) ↦ 1 + f x) b

Tactic:
ext _; rw [prod_one_add_ordered]

Premises used: Finset.prod_one_add_ordered
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
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_1 : 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
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
⊢ 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]

Premises used: Finset.prod_one_add_ordered
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
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_1 : 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
h : 1 + a = x
⊢ HAdd.hAdd (α := α) 1 (∑' (i : ι), f i * ∏ j ∈ Iio i, (1 + f j)) = x

Tactic:
rw [ha.tsum_eq]

Premises used: HasSum.tsum_eq
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
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

Tactic:
(tendsto_nhds_unique (hx.comp tendsto_finset_Iic_atTop_atTop) ?_).symm

Premises used: Filter.Tendsto.comp, Eq.symm, Filter.tendsto_finset_Iic_atTop_atTop, tendsto_nhds_unique
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
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_1 : 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
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))
⊢ 1 + a = x

Tactic:
refine (tendsto_nhds_unique (hx.comp tendsto_finset_Iic_atTop_atTop) ?_).symm

Premises used: Filter.Tendsto.comp, Eq.symm, Filter.tendsto_finset_Iic_atTop_atTop, tendsto_nhds_unique
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
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_1 : 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
h : Tendsto (fun (x : ι) ↦ ∑ i ∈ Iic x, f i * ∏ j ∈ Iic x with j < i, (1 + f j)) atTop (nhds 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))

Tactic:
apply Tendsto.const_add

Premises used: Filter.Tendsto.const_add
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
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 (s : Finset ι) ↦ ∑ b ∈ s, (fun (i : ι) ↦ f i * ∏ j ∈ Iio i, (1 + f j)) b) ∘ Iic)
    atTop (nhds a)

Tactic:
ha.comp tendsto_finset_Iic_atTop_atTop

Premises used: Filter.Tendsto.comp, Filter.tendsto_finset_Iic_atTop_atTop
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
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_1 : 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
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)
⊢ Tendsto (fun (x : ι) ↦ ∑ i ∈ Iic x, f i * ∏ j ∈ Iic x with j < i, (1 + f j)) atTop (nhds a)

Tactic:
convert! ha.comp tendsto_finset_Iic_atTop_atTop using 2 with s

Premises used: Filter.Tendsto.comp, Filter.tendsto_finset_Iic_atTop_atTop
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
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)

Tactic:
sum_congr rfl (fun i hi ↦ ?_)

Premises used: Multiset.sum, Multiset.foldr, Finset.sum_congr, Finset.sum, rfl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
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_1 : 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 : ι
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
⊢ 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:
refine sum_congr rfl (fun i hi ↦ ?_)

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
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_1 : 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
h : {j ∈ Iic s | j < i} = Iio i
⊢ f i * ∏ j ∈ Iic s with j < i, (1 + f j) = (fun (i : ι) ↦ f i * ∏ j ∈ Iio i, (1 + f j)) i

Tactic:
congr
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
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
⊢ {j ∈ Iic s | j < i} = Iio i

Tactic:
grind
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
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
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))
⊢ ∏' (i : ι), (1 - f i) = HSub.hSub (α := α) 1 (∑' (i : ι), f i * ∏ j ∈ Iio i, (1 - f j))

Tactic:
simp_rw [sub_eq_add_neg] at hsum hprod ⊢

Premises used: sub_eq_add_neg
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
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
⊢ Summable.{u_4, u_1} (α := α) fun (b : ι) ↦ -(f b * ∏ x ∈ Iio b, (1 + -f x))

Tactic:
obtain hsum' := hsum.neg

Premises used: Summable.neg
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
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))
⊢ Summable.{u_4, u_1} (α := α) fun (b : ι) ↦ -f b * ∏ x ∈ Iio b, (1 + -f x)

Tactic:
simp_rw [← neg_mul] at hsum'

Premises used: neg_mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
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)
simp_rw : ∏' (i : ι), (1 + -f i) = HAdd.hAdd (α := α) 1 (∑' (b : ι), -f b * ∏ i ∈ Iio b, (1 + -f i))
⊢ ∏' (i : ι), (1 + -f i) = HAdd.hAdd (α := α) 1 (-∑' (i : ι), f i * ∏ i ∈ Iio i, (1 + -f i))

Tactic:
simp_rw [← tsum_neg, ← neg_mul]

Premises used: tsum_neg, neg_mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
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 (∑' (b : ι), -f b * ∏ i ∈ Iio b, (1 + -f i))

Tactic:
tprod_one_add_ordered hsum' hprod

Premises used: tprod_one_add_ordered
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
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 (∑' (b : ι), -f b * ∏ i ∈ Iio b, (1 + -f i))

Tactic:
exact tprod_one_add_ordered hsum' hprod

Premises used: tprod_one_add_ordered
-- Module: Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
⊢ HasSumUniformlyOn f (fun (x : β) ↦ ∑' (n : α), f n x) s

Tactic:
simp [hasSumUniformlyOn_iff_tendstoUniformlyOn, tendstoUniformlyOn_tsum hu hfu]

Premises used: tendstoUniformlyOn_tsum, hasSumUniformlyOn_iff_tendstoUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn
Goal:
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
hfu : ∀ᶠ (n : ι) in cofinite, ∀ x ∈ s, ‖f n x‖ ≤ u n
⊢ HasSumUniformlyOn f (fun (x : β) ↦ ∑' (n : ι), f n x) s

Tactic:
simp [hasSumUniformlyOn_iff_tendstoUniformlyOn,
    tendstoUniformlyOn_tsum_of_cofinite_eventually hu hfu]

Premises used: tendstoUniformlyOn_tsum_of_cofinite_eventually, hasSumUniformlyOn_iff_tendstoUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn
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
apply : HasSumLocallyUniformlyOn f (fun (x : β) ↦ ∑' (n : α), f n x) s
⊢ SummableLocallyUniformlyOn f s

Tactic:
apply HasSumLocallyUniformlyOn.summableLocallyUniformlyOn (g := fun x ↦ ∑' n, f n x)

Premises used: HasSumLocallyUniformlyOn.summableLocallyUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn
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
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
⊢ HasSumLocallyUniformlyOn f (fun (x : β) ↦ ∑' (n : α), f n x) s

Tactic:
rw [hasSumLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn,
    tendstoLocallyUniformlyOn_iff_forall_isCompact hs]

Premises used: hasSumLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn, tendstoLocallyUniformlyOn_iff_forall_isCompact
-- Module: Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn
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
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
⊢ 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
-- Module: Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn
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
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:
tendstoUniformlyOn_tsum_of_cofinite_eventually hu1 hu2

Premises used: tendstoUniformlyOn_tsum_of_cofinite_eventually
-- Module: Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn
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
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:
exact tendstoUniformlyOn_tsum_of_cofinite_eventually hu1 hu2

Premises used: tendstoUniformlyOn_tsum_of_cofinite_eventually
-- Module: Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn
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
apply : ∀ K ⊆ s, IsCompact K → ∃ (u : α → ℝ), Summable u ∧ ∀ᶠ (n : α) in cofinite, ∀ k ∈ K, ‖f n k‖ ≤ u n
⊢ SummableLocallyUniformlyOn f s

Tactic:
apply SummableLocallyUniformlyOn.of_locally_bounded_eventually hs

Premises used: SummableLocallyUniformlyOn.of_locally_bounded_eventually
-- Module: Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn
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
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
⊢ ∃ (u : α → ℝ), Summable u ∧ ∀ᶠ (n : α) in cofinite, ∀ k ∈ K, ‖f n k‖ ≤ u n

Tactic:
obtain ⟨u, hu1, hu2⟩ := hu K hK hKc
-- Module: Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn
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
⊢ ∀ (a : α), ∀ k ∈ K, ‖f a k‖ ≤ u a

Tactic:
hu2
-- Module: Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn
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
h : ∀ (a : α), Membership.mem (γ := Set α) {x : α | (fun (n : α) ↦ ∀ k ∈ K, ‖f n k‖ ≤ u n) x} a
h₁ : ∀ (a : α), ∀ k ∈ K, ‖f a k‖ ≤ u a
⊢ ∀ᶠ (n : α) in cofinite, ∀ k ∈ K, ‖f n k‖ ≤ u n

Tactic:
filter_upwards using hu2
-- Module: Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn
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
⊢ ∃ (u : α → ℝ), Summable u ∧ ∀ᶠ (n : α) in cofinite, ∀ k ∈ K, ‖f n k‖ ≤ u n

Tactic:
exact ⟨u, hu1, by filter_upwards using hu2⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn
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 : HasDerivWithinAt.{u_2, u_3} (F := F) (fun (z : 𝕜) ↦ ∑' (n : ι), f n z) (∑' (n : ι), derivWithin (f n) s x) s x
⊢ Eq.{u_3 + 1} (α := F) (derivWithin (fun (z : 𝕜) ↦ ∑' (n : ι), f n z) s x) (∑' (n : ι), derivWithin (f n) s x)

Tactic:
apply HasDerivWithinAt.derivWithin ?_ (hs.uniqueDiffWithinAt hx)

Premises used: IsOpen.uniqueDiffWithinAt, HasDerivWithinAt.derivWithin
-- Module: Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn
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
h₁ : HasDerivAt.{u_2, u_3} (F := F) (fun (z : 𝕜) ↦ ∑' (n : ι), f n z) (∑' (n : ι), derivWithin (f n) s x) x
⊢ HasDerivWithinAt.{u_2, u_3} (F := F) (fun (z : 𝕜) ↦ ∑' (n : ι), f n z) (∑' (n : ι), derivWithin (f n) s x) s x

Tactic:
apply HasDerivAt.hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt