-- 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
refine₁ :
  ∀ (s : Set α) (hs : s ∈ 𝓝 a) (hsc : IsClosed[inst_1] s),
    ∃ (ia : Finset β), True ∧ ∀ x ∈ Set.Ici ia, ∏ b ∈ x, g b ∈ id s
refine₂ :
  ∀ (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),
    ∃ (ia : Finset β), True ∧ ∀ x ∈ Set.Ici ia, ∏ b ∈ x, g b ∈ id s
right right₁ :
  ∀ (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 ∈ bs, g b ∈ id s
right₂ :
  ∀ (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 ∈ bs, g b ∈ id s
right₃ :
  ∀ (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
right₄ :
  ∀ (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}
⊢ HasProd g a

Tactic:
classical
  refine (atTop_basis.tendsto_iff (closed_nhds_basis a)).mpr ?_
  rintro s ⟨hs, hsc⟩
  rcases mem_atTop_sets.mp (ha hs) with ⟨u, hu⟩
  use u.image Sigma.fst, trivial
  intro bs hbs
  simp only [Set.mem_preimage, Finset.le_iff_subset] at hu
  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))
  refine hsc.mem_of_tendsto this (eventually_atTop.2 ⟨u, fun t ht ↦ hu _ fun x hx ↦ ?_⟩)
  exact mem_filter.2 ⟨ht hx, hbs <| mem_image_of_mem _ hx⟩

Premises used: Iff.mpr, Filter.atTop_basis, trivial, Filter.HasBasis.tendsto_iff, closed_nhds_basis, Finset.le_iff_subset, Set.mem_preimage