awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
h : TendstoUniformlyOn (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop s
⊢ TendstoLocallyUniformlyOn (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop s

Tactic:
h.tendstoLocallyUniformlyOn

Premises used: TendstoUniformlyOn.tendstoLocallyUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
h : TendstoUniformlyOn (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop s
⊢ TendstoLocallyUniformlyOn (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop s

Tactic:
exact h.tendstoLocallyUniformlyOn

Premises used: TendstoUniformlyOn.tendstoLocallyUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
hs : IsOpen[inst_2] s
inst_3 : LocallyCompactSpace β
h : ∀ K ⊆ s, IsCompact K → HasProdUniformlyOn f g K
rw : ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop K
⊢ HasProdLocallyUniformlyOn f g s

Tactic:
rw [HasProdLocallyUniformlyOn, tendstoLocallyUniformlyOn_iff_forall_isCompact hs]

Premises used: tendstoLocallyUniformlyOn_iff_forall_isCompact, HasProdLocallyUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
hs : IsOpen[inst_2] s
inst_3 : LocallyCompactSpace β
h : ∀ K ⊆ s, IsCompact K → HasProdUniformlyOn f g K
⊢ ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop K

Tactic:
simpa [hasProdUniformlyOn_iff_tendstoUniformlyOn] using h

Premises used: hasProdUniformlyOn_iff_tendstoUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
h : HasProdLocallyUniformlyOn f g s
⊢ MultipliableLocallyUniformlyOn f s

Tactic:
⟨g, h⟩

Premises used: Exists.intro, MultipliableLocallyUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
t : Set β
h : HasProdLocallyUniformlyOn f g t
hst : s ⊆ t
⊢ HasProdLocallyUniformlyOn f g s

Tactic:
TendstoLocallyUniformlyOn.mono h hst

Premises used: TendstoLocallyUniformlyOn.mono, HasProdLocallyUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
t : Set β
h : MultipliableLocallyUniformlyOn f t
hst : s ⊆ t
⊢ MultipliableLocallyUniformlyOn f s

Tactic:
(h.choose_spec.mono hst).multipliableLocallyUniformlyOn

Premises used: Exists.choose_spec, HasProdLocallyUniformlyOn.multipliableLocallyUniformlyOn, HasProdLocallyUniformlyOn.mono
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
h : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, MultipliableUniformlyOn f t
⊢ MultipliableLocallyUniformlyOn f s

Tactic:
(hasProdLocallyUniformlyOn_of_of_forall_exists_nhds <| fun x hx ↦ match h x hx with
  | ⟨t, ht, htr⟩ => ⟨t, ht, htr.hasProdUniformlyOn⟩).multipliableLocallyUniformlyOn

Premises used: MultipliableUniformlyOn.hasProdUniformlyOn, HasProdLocallyUniformlyOn.multipliableLocallyUniformlyOn, nhdsWithin, Membership.mem, Exists, And, hasProdLocallyUniformlyOn_of_of_forall_exists_nhds, _private.0.multipliableLocallyUniformlyOn_of_of_forall_exists_nhds.match_1, And.intro, Exists.intro, tprod, HasProdUniformlyOn, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
h : MultipliableLocallyUniformlyOn f s
hs : IsCompact s
⊢ MultipliableUniformlyOn f s

Tactic:
(h.choose_spec.hasProdUniformlyOn_of_isCompact hs).multipliableUniformlyOn

Premises used: Exists.choose_spec, HasProdUniformlyOn.multipliableUniformlyOn, HasProdLocallyUniformlyOn.hasProdUniformlyOn_of_isCompact
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
x : β
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
inst_3 : LocallyCompactSpace β
h : MultipliableLocallyUniformlyOn f s
hx : s ∈ 𝓝 x
⊢ ∃ t ∈ 𝓝[s] x, MultipliableUniformlyOn f t

Tactic:
let H := (h.choose_spec.exists_hasProdUniformlyOn hx).choose_spec
  ⟨_, H.1, H.2.multipliableUniformlyOn⟩

Premises used: Exists.choose_spec, HasProdLocallyUniformlyOn.exists_hasProdUniformlyOn, And.right, And.left, And.intro, Exists.intro, HasProdUniformlyOn.multipliableUniformlyOn, Exists.choose
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
x : β
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
h : HasProdLocallyUniformlyOn f g s
hx : x ∈ s
⊢ HasProd (fun (x_1 : ι) ↦ f x_1 x) (g x)

Tactic:
h.tendsto_at hx

Premises used: iInf, HasProd, Filter.atTop, TendstoLocallyUniformlyOn.tendsto_at
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
x : β
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
h : MultipliableLocallyUniformlyOn f s
hx : x ∈ s
⊢ Multipliable.{u_1, u_3} (α := α) fun (x_1 : ι) ↦ f x_1 x

Tactic:
match h with | ⟨_, hg⟩ => (hg.hasProd hx).multipliable

Premises used: _private.0.MultipliableLocallyUniformlyOn.multipliable.match_1, Multipliable, HasProdLocallyUniformlyOn.hasProd, HasProd.multipliable, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
h : MultipliableLocallyUniformlyOn f s
⊢ HasProdLocallyUniformlyOn f (fun (x : β) ↦ ∏' (i : ι), f i x) s

Tactic:
h.elim fun _ hg => hg.congr_inseparable_right fun _ hx =>
    tendsto_nhds_unique_inseparable (hg.hasProd hx) (hg.hasProd hx).multipliable.hasProd

Premises used: tendsto_nhds_unique_inseparable, Multipliable.hasProd, TendstoLocallyUniformlyOn.congr_inseparable_right, HasProdLocallyUniformlyOn.hasProd, HasProd.multipliable, Exists.elim
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
inst_3 : T2Space α
h : HasProdLocallyUniformlyOn f g s
⊢ Set.EqOn (fun (x : β) ↦ ∏' (i : ι), f i x) g s

Tactic:
fun _ hx ↦ (h.hasProd hx).tprod_eq

Premises used: Set.EqOn, HasProd.tprod_eq, HasProdLocallyUniformlyOn.hasProd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
f f' : ι → β → α
h : ∀ (i : ι), Set.EqOn (f i) (f' i) s
h2 : MultipliableLocallyUniformlyOn f s
h₁ : HasProdLocallyUniformlyOn f' (fun (x : β) ↦ ∏' (i : ι), f i x) s
g : β → α
⊢ MultipliableLocallyUniformlyOn f' s

Tactic:
apply HasProdLocallyUniformlyOn.multipliableLocallyUniformlyOn

Premises used: HasProdLocallyUniformlyOn.multipliableLocallyUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
f f' : ι → β → α
h : ∀ (i : ι), Set.EqOn (f i) (f' i) s
h2 : MultipliableLocallyUniformlyOn f s
⊢ HasProdLocallyUniformlyOn f' (fun (x : β) ↦ ∏' (i : ι), f i x) s

Tactic:
(h2.hasProdLocallyUniformlyOn).congr fun v ↦ eqOn_fun_finsetProd h v

Premises used: eqOn_fun_finsetProd, TendstoLocallyUniformlyOn.congr, HasProdLocallyUniformlyOn, MultipliableLocallyUniformlyOn.hasProdLocallyUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
γ : Type u_4
inst_3 : TopologicalSpace γ
t : Set γ
h : HasProdLocallyUniformlyOn f g s
h' : γ → β
hh : Set.MapsTo h' t s
chh : ContinuousOn h' t
⊢ HasProdLocallyUniformlyOn (fun (i : ι) (y : γ) ↦ f i (h' y)) (g ∘ h') t

Tactic:
TendstoLocallyUniformlyOn.comp h h' hh chh

Premises used: Multiset.foldr, Multiset.prod, Finset.prod, TendstoLocallyUniformlyOn.comp, HasProdLocallyUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
γ : Type u_4
inst_3 : TopologicalSpace γ
t : Set γ
h : MultipliableLocallyUniformlyOn f s
h' : γ → β
hh : Set.MapsTo h' t s
chh : ContinuousOn h' t
⊢ MultipliableLocallyUniformlyOn.{u_1, u_4, u_3} (α := α) (fun (i : ι) (y : γ) ↦ f i (h' y)) t

Tactic:
(h.hasProdLocallyUniformlyOn.comp h' hh chh).multipliableLocallyUniformlyOn

Premises used: HasProdLocallyUniformlyOn.multipliableLocallyUniformlyOn, HasProdLocallyUniformlyOn.comp, MultipliableLocallyUniformlyOn.hasProdLocallyUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
g : β → α
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
f : ℕ → β → α
h : HasProdLocallyUniformlyOn f g s
⊢ TendstoLocallyUniformlyOn (fun (x1 : Finset ℕ) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop s

Tactic:
rw [hasProdLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn] at h

Premises used: hasProdLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
g : β → α
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
f : ℕ → β → α
h : TendstoLocallyUniformlyOn (fun (x1 : Finset ℕ) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop s
v : Set (α × α)
hv : v ∈ uniformity α
r : β
hr : r ∈ s
obtain :
  ∀ (t : Set β) (ht : t ∈ 𝓝[s] r)
    (htr : ∀ᶠ (n : Finset ℕ) in atTop, ∀ y ∈ t, (g y, (fun (x1 : Finset ℕ) (x2 : β) ↦ (∏ i ∈ x1, f i x2 : α)) n y) ∈ v),
    ∃ t ∈ 𝓝[s] r, ∀ᶠ (n : ℕ) in atTop, ∀ y ∈ t, (g y, (fun (N : ℕ) (b : β) ↦ (∏ i ∈ Finset.range N, f i b : α)) n y) ∈ v
⊢ ∃ t ∈ 𝓝[s] r, ∀ᶠ (n : ℕ) in atTop, ∀ y ∈ t, (g y, (fun (N : ℕ) (b : β) ↦ (∏ i ∈ Finset.range N, f i b : α)) n y) ∈ v

Tactic:
obtain ⟨t, ht, htr⟩ := h v hv r hr
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
g : β → α
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
f : ℕ → β → α
h : TendstoLocallyUniformlyOn (fun (x1 : Finset ℕ) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop s
v : Set (α × α)
hv : v ∈ uniformity α
r : β
hr : r ∈ s
t : Set β
ht : t ∈ 𝓝[s] r
htr : ∀ᶠ (n : Finset ℕ) in atTop, ∀ y ∈ t, (g y, (fun (x1 : Finset ℕ) (x2 : β) ↦ (∏ i ∈ x1, f i x2 : α)) n y) ∈ v
⊢ ∃ t ∈ 𝓝[s] r, ∀ᶠ (n : ℕ) in atTop, ∀ y ∈ t, (g y, (fun (N : ℕ) (b : β) ↦ (∏ i ∈ Finset.range N, f i b : α)) n y) ∈ v

Tactic:
⟨t, ht, Filter.tendsto_finset_range.eventually htr⟩

Premises used: Filter.tendsto_finset_range, And.intro, Filter.Tendsto.eventually, Exists.intro
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
g : β → α
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
f : ℕ → β → α
h : TendstoLocallyUniformlyOn (fun (x1 : Finset ℕ) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop s
v : Set (α × α)
hv : v ∈ uniformity α
r : β
hr : r ∈ s
t : Set β
ht : t ∈ 𝓝[s] r
htr : ∀ᶠ (n : Finset ℕ) in atTop, ∀ y ∈ t, (g y, (fun (x1 : Finset ℕ) (x2 : β) ↦ (∏ i ∈ x1, f i x2 : α)) n y) ∈ v
⊢ ∃ t ∈ 𝓝[s] r, ∀ᶠ (n : ℕ) in atTop, ∀ y ∈ t, (g y, (fun (N : ℕ) (b : β) ↦ (∏ i ∈ Finset.range N, f i b : α)) n y) ∈ v

Tactic:
exact ⟨t, ht, Filter.tendsto_finset_range.eventually htr⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
⊢ MultipliableLocallyUniformlyOn f s ↔ HasProdLocallyUniformlyOn f (fun (x : β) ↦ ∏' (i : ι), f i x) s

Tactic:
⟨MultipliableLocallyUniformlyOn.hasProdLocallyUniformlyOn,
    HasProdLocallyUniformlyOn.multipliableLocallyUniformlyOn⟩

Premises used: HasProdLocallyUniformlyOn.multipliableLocallyUniformlyOn, Iff.intro, MultipliableLocallyUniformlyOn.hasProdLocallyUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
inst_1 : UniformSpace α
h : MultipliableUniformly f
⊢ ∃ (g : β → α), HasProdUniformly f g

Tactic:
h

Premises used: MultipliableUniformly, Multipliable, UniformFun, HasProdUniformly
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
inst_1 : UniformSpace α
h : HasProdUniformly f g
⊢ MultipliableUniformly f

Tactic:
⟨g, h⟩

Premises used: MultipliableUniformly, Multipliable, Exists.intro
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
inst_1 : UniformSpace α
⊢ HasProdUniformly f g ↔ TendstoUniformly (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop

Tactic:
simpa [HasProdUniformly, HasProd, ← UniformFun.ofFun_prod, Finset.prod_fn] using
    UniformFun.tendsto_iff_tendstoUniformly

Premises used: UniformFun.tendsto_iff_tendstoUniformly, HasProd, UniformFun.ofFun_prod, Finset.prod_fn, SummationFilter.unconditional, HasProdUniformly
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
s : Set β
inst_1 : UniformSpace α
h : HasProdUniformly f g
⊢ HasProdUniformlyOn f g s

Tactic:
hasProdUniformlyOn_iff_tendstoUniformlyOn.mpr h.tendstoUniformly.tendstoUniformlyOn

Premises used: Iff.mpr, TendstoUniformly.tendstoUniformlyOn, hasProdUniformlyOn_iff_tendstoUniformlyOn, HasProdUniformly.tendstoUniformly
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
inst_1 : UniformSpace α
⊢ HasProdUniformlyOn f g Set.univ ↔ HasProdUniformly f g

Tactic:
simp [hasProdUniformly_iff_tendstoUniformly, hasProdUniformlyOn_iff_tendstoUniformlyOn,
    tendstoUniformlyOn_univ]

Premises used: tendstoUniformlyOn_univ, hasProdUniformly_iff_tendstoUniformly, hasProdUniformlyOn_iff_tendstoUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
s : Set β
inst_1 : UniformSpace α
h : MultipliableUniformly f
⊢ MultipliableUniformlyOn f s

Tactic:
h.exists.choose_spec.hasProdUniformlyOn.multipliableUniformlyOn

Premises used: Exists.choose_spec, HasProdUniformly.hasProdUniformlyOn, MultipliableUniformly.exists, HasProdUniformlyOn.multipliableUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
inst_1 : UniformSpace α
⊢ MultipliableUniformlyOn f Set.univ ↔ MultipliableUniformly f

Tactic:
⟨fun h ↦ (hasProdUniformlyOn_univ_iff.mp h.exists.choose_spec).multipliableUniformly,
    MultipliableUniformly.multipliableUniformlyOn⟩

Premises used: Exists.choose_spec, MultipliableUniformlyOn.exists, HasProdUniformly.multipliableUniformly, MultipliableUniformly.multipliableUniformlyOn, hasProdUniformlyOn_univ_iff, Iff.intro, Iff.mp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
inst_1 : UniformSpace α
f' : ι → β → α
h : HasProdUniformly f g
hff' : ∀ᶠ (n : Finset ι) in atTop, ∀ (b : β), Eq.{u_1 + 1} (α := α) (∏ i ∈ n, f i b) (∏ i ∈ n, f' i b)
rw :
  ∀ (h : TendstoUniformly (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop)
    (hff' : ∀ᶠ (n : Finset ι) in atTop, ∀ (b : β), Eq.{u_1 + 1} (α := α) (∏ i ∈ n, f i b) (∏ i ∈ n, f' i b)),
    TendstoUniformly (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f' i x2) g atTop
⊢ HasProdUniformly f' g

Tactic:
rw [hasProdUniformly_iff_tendstoUniformly] at *

Premises used: hasProdUniformly_iff_tendstoUniformly
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
inst_1 : UniformSpace α
f' : ι → β → α
h : TendstoUniformly (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop
hff' : ∀ᶠ (n : Finset ι) in atTop, ∀ (b : β), Eq.{u_1 + 1} (α := α) (∏ i ∈ n, f i b) (∏ i ∈ n, f' i b)
⊢ EventuallyEq (β := β → α) atTop (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) fun (x1 : Finset ι) (x2 : β) ↦
    ∏ i ∈ x1, f' i x2

Tactic:
simpa only [EventuallyEq, funext_iff]

Premises used: funext_iff, Filter.EventuallyEq
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
inst_1 : UniformSpace α
f' : ι → β → α
h : TendstoUniformly (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop
hff' : ∀ᶠ (n : Finset ι) in atTop, ∀ (b : β), Eq.{u_1 + 1} (α := α) (∏ i ∈ n, f i b) (∏ i ∈ n, f' i b)
⊢ TendstoUniformly (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f' i x2) g atTop

Tactic:
exact (tendstoUniformly_congr (by simpa only [EventuallyEq, funext_iff])).mp h

Premises used: Iff.mp, tendstoUniformly_congr
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
g : β → α
inst_1 : UniformSpace α
f : ℕ → β → α
h : HasProdUniformly f g
⊢ TendstoUniformly (fun (x1 : ℕ) (x2 : β) ↦ ∏ i ∈ Finset.range x1, f i x2) g atTop

Tactic:
(tendsto_finset_range.eventually <| h.tendstoUniformly · ·)

Premises used: Set.Mem, Filter.tendsto_finset_range, TendstoUniformly, Filter.Tendsto.eventually, HasProdUniformly.tendstoUniformly
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
x : β
inst_1 : UniformSpace α
h : HasProdUniformly f g
⊢ HasProd (fun (x_1 : ι) ↦ f x_1 x) (g x)

Tactic:
h.tendstoUniformly.tendsto_at _

Premises used: iInf, HasProd, TendstoUniformly.tendsto_at, Filter.atTop, HasProdUniformly.tendstoUniformly
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
x : β
inst_1 : UniformSpace α
h : MultipliableUniformly f
⊢ Multipliable.{u_1, u_3} (α := α) fun (x_1 : ι) ↦ f x_1 x

Tactic:
h.exists.choose_spec.hasProd.multipliable

Premises used: Exists.choose_spec, HasProdUniformly.hasProd, MultipliableUniformly.exists, HasProd.multipliable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
inst_1 : UniformSpace α
h : MultipliableUniformly f
⊢ HasProdUniformly f fun (x : β) ↦ ∏' (i : ι), f i x

Tactic:
hasProdUniformlyOn_univ_iff.1 (multipliableUniformlyOn_univ_iff.2 h).hasProdUniformlyOn

Premises used: Iff.mpr, MultipliableUniformlyOn.hasProdUniformlyOn, hasProdUniformlyOn_univ_iff, multipliableUniformlyOn_univ_iff, Iff.mp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
inst_1 : UniformSpace α
⊢ MultipliableUniformly f ↔ HasProdUniformly f fun (x : β) ↦ ∏' (i : ι), f i x

Tactic:
⟨MultipliableUniformly.hasProdUniformly, HasProdUniformly.multipliableUniformly⟩

Premises used: HasProdUniformly.multipliableUniformly, Iff.intro, MultipliableUniformly.hasProdUniformly
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
h : MultipliableLocallyUniformly f
⊢ ∃ (g : β → α), HasProdLocallyUniformly f g

Tactic:
h

Premises used: MultipliableLocallyUniformly
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
h : HasProdLocallyUniformly f g
⊢ MultipliableLocallyUniformly f

Tactic:
⟨g, h⟩

Premises used: MultipliableLocallyUniformly, Exists.intro
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
⊢ HasProdLocallyUniformly f g ↔ TendstoLocallyUniformly (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop

Tactic:
.rfl

Premises used: HasProdLocallyUniformly, Iff.rfl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
h : HasProdLocallyUniformly f g
⊢ HasProdLocallyUniformlyOn f g s

Tactic:
h.tendstoLocallyUniformlyOn

Premises used: TendstoLocallyUniformly.tendstoLocallyUniformlyOn, HasProdLocallyUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
h : MultipliableLocallyUniformly f
⊢ MultipliableLocallyUniformlyOn f s

Tactic:
h.exists.choose_spec.hasProdLocallyUniformlyOn.multipliableLocallyUniformlyOn

Premises used: Exists.choose_spec, HasProdLocallyUniformlyOn.multipliableLocallyUniformlyOn, MultipliableLocallyUniformly.exists, HasProdLocallyUniformly.hasProdLocallyUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
h : ∀ (x : β), ∃ t ∈ 𝓝 x, HasProdUniformlyOn f g t
⊢ ∀ (x : β), ∃ t ∈ 𝓝 x, TendstoUniformlyOn (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop t

Tactic:
simpa [hasProdUniformlyOn_iff_tendstoUniformlyOn] using h

Premises used: hasProdUniformlyOn_iff_tendstoUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
h : HasProdUniformly f g
⊢ TendstoUniformly (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop

Tactic:
simp only [hasProdUniformly_iff_tendstoUniformly, HasProdLocallyUniformly] at *

Premises used: HasProdLocallyUniformly, hasProdUniformly_iff_tendstoUniformly
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
h : TendstoUniformly (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop
⊢ TendstoLocallyUniformly (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop

Tactic:
TendstoUniformly.tendstoLocallyUniformly h

Premises used: TendstoUniformly.tendstoLocallyUniformly
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
h : TendstoUniformly (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop
⊢ TendstoLocallyUniformly (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop

Tactic:
exact TendstoUniformly.tendstoLocallyUniformly h

Premises used: TendstoUniformly.tendstoLocallyUniformly