awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
refine :
  ∀ (ib : Set α), ib ∈ 𝓝 a ∧ IsClosed[inst_1] ib → ∃ (ia : Finset β), True ∧ ∀ x ∈ Set.Ici ia, ∏ b ∈ x, g b ∈ id ib
⊢ HasProd g a

Tactic:
refine (atTop_basis.tendsto_iff (closed_nhds_basis a)).mpr ?_

Premises used: Iff.mpr, Filter.atTop_basis, Filter.HasBasis.tendsto_iff, closed_nhds_basis
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed[inst_1] s
rcases :
  ∀ (u : Finset ((b : β) × γ b))
    (hu :
      ∀ b ≥ u,
        Membership.mem (γ := Set (Finset ((b : β) × γ b))) ((fun (s : Finset ((b : β) × γ b)) ↦ ∏ b ∈ s, f b) ⁻¹' s) b),
    ∃ (ia : Finset β), True ∧ ∀ x ∈ Set.Ici ia, ∏ b ∈ x, g b ∈ id s
⊢ ∃ (ia : Finset β), True ∧ ∀ x ∈ Set.Ici ia, ∏ b ∈ x, g b ∈ id s

Tactic:
rcases mem_atTop_sets.mp (ha hs) with ⟨u, hu⟩

Premises used: Filter.mem_atTop_sets, Iff.mp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed[inst_1] s
u : Finset ((b : β) × γ b)
hu :
  ∀ b ≥ u,
    Membership.mem (γ := Set (Finset ((b : β) × γ b))) ((fun (s : Finset ((b : β) × γ b)) ↦ ∏ b ∈ s, f b) ⁻¹' s) b
right : ∀ x ∈ Set.Ici (image (Sigma.fst (β := fun (b : β) ↦ γ b)) u), ∏ b ∈ x, g b ∈ id s
⊢ ∃ (ia : Finset β), True ∧ ∀ x ∈ Set.Ici ia, ∏ b ∈ x, g b ∈ id s

Tactic:
use u.image Sigma.fst, trivial

Premises used: trivial, Sigma.fst, Finset.image
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed[inst_1] s
u : Finset ((b : β) × γ b)
hu :
  ∀ b ≥ u,
    Membership.mem (γ := Set (Finset ((b : β) × γ b))) ((fun (s : Finset ((b : β) × γ b)) ↦ ∏ b ∈ s, f b) ⁻¹' s) b
bs : Finset β
hbs : bs ∈ Set.Ici (image (Sigma.fst (β := fun (b : β) ↦ γ b)) u)
⊢ ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∏ b ∈ b, f b ∈ s

Tactic:
simp only [Set.mem_preimage, Finset.le_iff_subset] at hu

Premises used: Finset.le_iff_subset, Set.mem_preimage
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed[inst_1] s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image (Sigma.fst (β := fun (b : β) ↦ γ b)) u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∏ b ∈ b, f b ∈ s
simp :
  Tendsto (β := α)
    (fun (t : Finset ((b : β) × γ b)) ↦
      ∏ a ∈ bs, ∏ s ∈ t.preimage (Sigma.mk (β := fun (a : β) ↦ γ a) a) ⋯, f (Sigma.mk (β := fun (a : β) ↦ γ a) a s))
    atTop (𝓝 (∏ b ∈ bs, g b))
⊢ Tendsto (β := α) (fun (t : Finset ((b : β) × γ b)) ↦ ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ bs, f p) atTop
    (𝓝 (∏ b ∈ bs, g b))

Tactic:
simp only [← sigma_preimage_mk, prod_sigma]

Premises used: Finset.prod_sigma, Finset.sigma_preimage_mk
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed[inst_1] s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image (Sigma.fst (β := fun (b : β) ↦ γ b)) u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∏ b ∈ b, f b ∈ s
⊢ Tendsto (β := α)
    (fun (t : Finset ((b : β) × γ b)) ↦
      ∏ a ∈ bs, ∏ s ∈ t.preimage (Sigma.mk (β := fun (a : β) ↦ γ a) a) ⋯, f (Sigma.mk (β := fun (a : β) ↦ γ a) a s))
    atTop (𝓝 (∏ b ∈ bs, g b))

Tactic:
tendsto_finsetProd _ fun b _ ↦ ?_

Premises used: tendsto_finsetProd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed[inst_1] s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image (Sigma.fst (β := fun (b : β) ↦ γ b)) u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∏ b ∈ b, f b ∈ s
refine :
  ∀ b ∈ bs,
    Tendsto
      (fun (t : Finset ((b : β) × γ b)) ↦
        ∏ s ∈ t.preimage (Sigma.mk (β := fun (a : β) ↦ γ a) b) ⋯, f (Sigma.mk (β := fun (a : β) ↦ γ a) b s))
      atTop (𝓝 (g b))
⊢ Tendsto (β := α)
    (fun (t : Finset ((b : β) × γ b)) ↦
      ∏ a ∈ bs, ∏ s ∈ t.preimage (Sigma.mk (β := fun (a : β) ↦ γ a) a) ⋯, f (Sigma.mk (β := fun (a : β) ↦ γ a) a s))
    atTop (𝓝 (∏ b ∈ bs, g b))

Tactic:
refine tendsto_finsetProd _ fun b _ ↦ ?_

Premises used: tendsto_finsetProd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed[inst_1] s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image (Sigma.fst (β := fun (b : β) ↦ γ b)) u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∏ b ∈ b, f b ∈ s
b : β
h : b ∈ bs
⊢ Tendsto
    (fun (t : Finset (Sigma γ)) ↦
      (fun (t : Finset (γ b)) ↦ (∏ s ∈ t, f (Sigma.mk (β := fun (b : β) ↦ γ b) b s) : α))
        (t.preimage (Sigma.mk (β := γ) b) ⋯))
    atTop (𝓝 (g b))

Tactic:
(hf b).comp (tendsto_finset_preimage_atTop_atTop (sigma_mk_injective))

Premises used: Multiset.foldr, Multiset.prod, Finset.prod, Filter.tendsto_finset_preimage_atTop_atTop, Filter.Tendsto.comp, sigma_mk_injective
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed[inst_1] s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image (Sigma.fst (β := fun (b : β) ↦ γ b)) u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∏ b ∈ b, f b ∈ s
b : β
h : b ∈ bs
⊢ Tendsto
    (fun (t : Finset (Sigma γ)) ↦
      (fun (t : Finset (γ b)) ↦ (∏ s ∈ t, f (Sigma.mk (β := fun (b : β) ↦ γ b) b s) : α))
        (t.preimage (Sigma.mk (β := γ) b) ⋯))
    atTop (𝓝 (g b))

Tactic:
exact (hf b).comp (tendsto_finset_preimage_atTop_atTop (sigma_mk_injective))

Premises used: Filter.tendsto_finset_preimage_atTop_atTop, Filter.Tendsto.comp, sigma_mk_injective
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed[inst_1] s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image (Sigma.fst (β := fun (b : β) ↦ γ b)) u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∏ b ∈ b, f b ∈ s
⊢ Tendsto (β := α) (fun (t : Finset ((b : β) × γ b)) ↦ ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ bs, f p) atTop
    (𝓝 (∏ b ∈ bs, g b))

Tactic:
have : Tendsto (fun t : Finset (Σ b, γ b) ↦ ∏ p ∈ t with p.1 ∈ bs, f p) atTop
      (𝓝 <| ∏ b ∈ bs, g b) := by
    simp only [← sigma_preimage_mk, prod_sigma]
    refine tendsto_finsetProd _ fun b _ ↦ ?_
    change
      Tendsto (fun t ↦ (fun t ↦ ∏ s ∈ t, f ⟨b, s⟩) (preimage t (Sigma.mk b) _)) atTop (𝓝 (g b))
    exact (hf b).comp (tendsto_finset_preimage_atTop_atTop (sigma_mk_injective))
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed[inst_1] s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image (Sigma.fst (β := fun (b : β) ↦ γ b)) u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∏ b ∈ b, f b ∈ s
this :
  Tendsto (β := α) (fun (t : Finset ((b : β) × γ b)) ↦ ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ bs, f p) atTop
    (𝓝 (∏ b ∈ bs, g b))
⊢ ∏ b ∈ bs, g b ∈ id s

Tactic:
hsc.mem_of_tendsto this (eventually_atTop.2 ⟨u, fun t ht ↦ hu _ fun x hx ↦ ?_⟩)

Premises used: Iff.mpr, Set.Mem, Membership.mem, IsClosed.mem_of_tendsto, Sigma.fst, Exists.intro, Filter.eventually_atTop, Finset.filter
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed[inst_1] s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image (Sigma.fst (β := fun (b : β) ↦ γ b)) u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∏ b ∈ b, f b ∈ s
this :
  Tendsto (β := α) (fun (t : Finset ((b : β) × γ b)) ↦ ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ bs, f p) atTop
    (𝓝 (∏ b ∈ bs, g b))
right :
  ∀ (t : Finset ((b : β) × γ b)) (ht : t ≥ u) (x : (b : β) × γ b) (hx : x ∈ u),
    x ∈ {p ∈ t | p.fst (β := fun (b : β) ↦ γ b) ∈ bs}
⊢ ∏ b ∈ bs, g b ∈ id s

Tactic:
refine hsc.mem_of_tendsto this (eventually_atTop.2 ⟨u, fun t ht ↦ hu _ fun x hx ↦ ?_⟩)

Premises used: Iff.mpr, Membership.mem, IsClosed.mem_of_tendsto, Sigma.fst, Exists.intro, Filter.eventually_atTop, Finset.filter
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed[inst_1] s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image (Sigma.fst (β := fun (b : β) ↦ γ b)) u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∏ b ∈ b, f b ∈ s
this :
  Tendsto (β := α) (fun (t : Finset ((b : β) × γ b)) ↦ ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ bs, f p) atTop
    (𝓝 (∏ b ∈ bs, g b))
t : Finset ((b : β) × γ b)
ht : t ≥ u
x : (b : β) × γ b
hx : x ∈ u
⊢ x ∈ {p ∈ t | p.fst (β := fun (b : β) ↦ γ b) ∈ bs}

Tactic:
mem_filter.2 ⟨ht hx, hbs <| mem_image_of_mem _ hx⟩

Premises used: Iff.mpr, And.intro, Finset.mem_filter, Finset.mem_image_of_mem
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed[inst_1] s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image (Sigma.fst (β := fun (b : β) ↦ γ b)) u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∏ b ∈ b, f b ∈ s
this :
  Tendsto (β := α) (fun (t : Finset ((b : β) × γ b)) ↦ ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ bs, f p) atTop
    (𝓝 (∏ b ∈ bs, g b))
t : Finset ((b : β) × γ b)
ht : t ≥ u
x : (b : β) × γ b
hx : x ∈ u
⊢ x ∈ {p ∈ t | p.fst (β := fun (b : β) ↦ γ b) ∈ bs}

Tactic:
exact mem_filter.2 ⟨ht hx, hbs <| mem_image_of_mem _ hx⟩

Premises used: Iff.mpr, And.intro, Finset.mem_filter
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : RegularSpace α
f : β × γ → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun (c : γ) ↦ f (b, c)) (g b)
⊢ HasProd g a

Tactic:
HasProd.sigma ((Equiv.sigmaEquivProd β γ).hasProd_iff.2 ha) hf

Premises used: Iff.mpr, HasProd.sigma, Equiv.hasProd_iff, Equiv.sigmaEquivProd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
ha : Multipliable f
hf : ∀ (b : β), Multipliable.{u_1, u_4} (α := α) fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)
⊢ Multipliable.{u_1, u_2} (α := α) fun (b : β) ↦ ∏' (c : γ b), f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)

Tactic:
(ha.hasProd.sigma fun b ↦ (hf b).hasProd).multipliable

Premises used: HasProd.sigma, Multipliable.hasProd, HasProd.multipliable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : T3Space α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd g a
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hf' : Multipliable f
⊢ HasProd f a

Tactic:
simpa [(hf'.hasProd.sigma hf).unique ha] using hf'.hasProd

Premises used: HasProd.unique, HasProd.sigma, Multipliable.hasProd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : T3Space α
γ : β → Type u_4
f : (b : β) × γ b → α
h₁ : ∀ (b : β), Multipliable.{u_1, u_4} (α := α) fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)
h₂ : Multipliable f
⊢ Eq.{u_1 + 1} (α := α) (∏' (p : (b : β) × γ b), f p) (∏' (b : β) (c : γ b), f (Sigma.mk (β := fun (b : β) ↦ γ b) b c))

Tactic:
(h₂.hasProd.sigma fun b ↦ (h₁ b).hasProd).tprod_eq.symm

Premises used: HasProd.sigma, HasProd.tprod_eq, Multipliable.hasProd, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : T3Space α
f : β × γ → α
h : Multipliable f
h₁ : ∀ (b : β), Multipliable.{u_1, u_3} (α := α) fun (c : γ) ↦ f (b, c)
⊢ Eq.{u_1 + 1} (α := α) (∏' (p : β × γ), f p) (∏' (b : β) (c : γ), f (b, c))

Tactic:
(h.hasProd.prod_fiberwise fun b ↦ (h₁ b).hasProd).tprod_eq.symm

Premises used: HasProd.tprod_eq, Multipliable.hasProd, HasProd.prod_fiberwise, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : T3Space α
f : β → γ → α
h : Multipliable (uncurry f)
h₁ : ∀ (b : β), Multipliable.{u_1, u_3} (α := α) fun (c : γ) ↦ f b c
⊢ Eq.{u_1 + 1} (α := α) (∏' (p : β × γ), uncurry f p) (∏' (b : β) (c : γ), f b c)

Tactic:
(h.hasProd.prod_fiberwise fun b ↦ (h₁ b).hasProd).tprod_eq.symm

Premises used: HasProd.tprod_eq, Multipliable.hasProd, HasProd.prod_fiberwise, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : T3Space α
f : β → γ → α
h : Multipliable (uncurry f)
h₁ : ∀ (b : β), Multipliable (f b)
h₂ : ∀ (c : γ), Multipliable.{u_1, u_2} (α := α) fun (b : β) ↦ f b c
rw :
  Eq.{u_1 + 1} (α := α) (∏' (p : γ × β), uncurry (fun (b : γ) (c : β) ↦ f c b) p)
    (∏' (c : γ × β), uncurry f ((Equiv.prodComm γ β : (a : γ × β) → β × γ) c))
⊢ Eq.{u_1 + 1} (α := α) (∏' (c : γ) (b : β), f b c) (∏' (b : β) (c : γ), f b c)

Tactic:
rw [← h.tprod_prod_uncurry h₁, ← h.prod_symm.tprod_prod_uncurry h₂,
    ← (Equiv.prodComm γ β).tprod_eq (uncurry f)]

Premises used: Equiv.prodComm, Multipliable.tprod_prod_uncurry, Equiv.tprod_eq, Function.uncurry
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : T3Space α
f : β → γ → α
h : Multipliable (uncurry f)
h₁ : ∀ (b : β), Multipliable (f b)
h₂ : ∀ (c : γ), Multipliable.{u_1, u_2} (α := α) fun (b : β) ↦ f b c
⊢ Eq.{u_1 + 1} (α := α) (∏' (p : γ × β), uncurry (fun (b : γ) (c : β) ↦ f c b) p)
    (∏' (c : γ × β), uncurry f ((Equiv.prodComm γ β : (a : γ × β) → β × γ) c))

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
apply : ClusterPt a (Filter.map (fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i) atTop)
⊢ HasProd f a

Tactic:
apply le_nhds_of_cauchy_adhp h

Premises used: le_nhds_of_cauchy_adhp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
simp : ∀ s ∈ 𝓝 a, ∀ (a : Finset ((b : β) × γ b)), ∃ (b : Finset ((b : β) × γ b)), a ⊆ b ∧ ∏ i ∈ b, f i ∈ s
⊢ ClusterPt a (Filter.map (fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i) atTop)

Tactic:
simp only [← mapClusterPt_def, mapClusterPt_iff_frequently, frequently_atTop, ge_iff_le,
    le_eq_subset]

Premises used: mapClusterPt_def, ge_iff_le, Filter.frequently_atTop, mapClusterPt_iff_frequently, Finset.le_eq_subset
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
rcases :
  ∀ (v : Set α) (vu : v ⊆ u) (v_open : IsOpen[inst_1.toTopologicalSpace] v) (hv : a ∈ v),
    ∃ (b : Finset ((b : β) × γ b)), s ⊆ b ∧ ∏ i ∈ b, f i ∈ u
⊢ ∃ (b : Finset ((b : β) × γ b)), s ⊆ b ∧ ∏ i ∈ b, f i ∈ u

Tactic:
rcases mem_nhds_iff.1 hu with ⟨v, vu, v_open, hv⟩

Premises used: mem_nhds_iff, Iff.mp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen[inst_1.toTopologicalSpace] v
hv : a ∈ v
⊢ ∀ᶠ (t0 : Finset β) in atTop, ∏ i ∈ t0, g i ∈ v

Tactic:
have A : ∀ᶠ t0 in (atTop : Filter (Finset β)), ∏ i ∈ t0, g i ∈ v := hg (v_open.mem_nhds hv)
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen[inst_1.toTopologicalSpace] v
hv : a ∈ v
A : ∀ᶠ (t0 : Finset β) in atTop, ∏ i ∈ t0, g i ∈ v
⊢ ∃ (t0 : Finset β), ∏ i ∈ t0, g i ∈ v ∧ image (Sigma.fst (β := fun (b : β) ↦ γ b)) s ⊆ t0

Tactic:
(A.and (Ici_mem_atTop _)).exists

Premises used: Filter.Eventually.and, Filter.Eventually.exists, Filter.Ici_mem_atTop
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen[inst_1.toTopologicalSpace] v
hv : a ∈ v
A : ∀ᶠ (t0 : Finset β) in atTop, ∏ i ∈ t0, g i ∈ v
⊢ ∃ (t0 : Finset β), ∏ i ∈ t0, g i ∈ v ∧ image (Sigma.fst (β := fun (b : β) ↦ γ b)) s ⊆ t0

Tactic:
exact (A.and (Ici_mem_atTop _)).exists

Premises used: Filter.Eventually.and, Filter.Eventually.exists, Filter.Ici_mem_atTop
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen[inst_1.toTopologicalSpace] v
hv : a ∈ v
obtain :
  ∀ (t0 : Finset β) (st0 : ∏ i ∈ t0, g i ∈ v) (ht0 : image (Sigma.fst (β := fun (b : β) ↦ γ b)) s ⊆ t0),
    ∃ (b : Finset ((b : β) × γ b)), s ⊆ b ∧ ∏ i ∈ b, f i ∈ u
⊢ ∃ (b : Finset ((b : β) × γ b)), s ⊆ b ∧ ∏ i ∈ b, f i ∈ u

Tactic:
obtain ⟨t0, st0, ht0⟩ : ∃ t0, ∏ i ∈ t0, g i ∈ v ∧ s.image Sigma.fst ⊆ t0 := by
    have A : ∀ᶠ t0 in (atTop : Filter (Finset β)), ∏ i ∈ t0, g i ∈ v := hg (v_open.mem_nhds hv)
    exact (A.and (Ici_mem_atTop _)).exists

Premises used: Sigma.fst, Finset.image
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
hg : HasProd g a
h : CauchySeq (α := α) fun (s : Finset ((b : β) × γ b)) ↦ ∏ i ∈ s, f i
u : Set α
hu : u ∈ 𝓝 a
s : Finset ((b : β) × γ b)
v : Set α
vu : v ⊆ u
v_open : IsOpen[inst_1.toTopologicalSpace] v
hv : a ∈ v
t0 : Finset β
st0 : ∏ i ∈ t0, g i ∈ v
ht0 : image (Sigma.fst (β := fun (b : β) ↦ γ b)) s ⊆ t0
simp :
  Tendsto (β := α)
    (fun (t : Finset ((b : β) × γ b)) ↦
      ∏ a ∈ t0, ∏ s ∈ t.preimage (Sigma.mk (β := fun (a : β) ↦ γ a) a) ⋯, f (Sigma.mk (β := fun (a : β) ↦ γ a) a s))
    atTop (𝓝 (∏ b ∈ t0, g b))
⊢ Tendsto (β := α) (fun (t : Finset ((b : β) × γ b)) ↦ ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ t0, f p) atTop
    (𝓝 (∏ b ∈ t0, g b))

Tactic:
simp only [← sigma_preimage_mk, prod_sigma]

Premises used: Finset.prod_sigma, Finset.sigma_preimage_mk