-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
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)
apply₁ apply₂ :
  ∀ (u : Set α) (hu : u ∈ 𝓝 a) (s : Finset ((b : β) × γ b)), ∃ (b : Finset ((b : β) × γ b)), s ⊆ b ∧ ∏ i ∈ b, f i ∈ u
apply₃ :
  ∀ (u : Set α) (hu : u ∈ 𝓝 a) (s : Finset ((b : β) × γ b)) (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
apply₄ :
  ∀ (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), ∃ (b : Finset ((b : β) × γ b)), s ⊆ b ∧ ∏ i ∈ b, f i ∈ u
apply₅ :
  ∀ (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)
    (L :
      Tendsto (β := α) (fun (t : Finset ((b : β) × γ b)) ↦ ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ t0, f p) atTop
        (𝓝 (∏ b ∈ t0, g b))),
    ∃ (b : Finset ((b : β) × γ b)), s ⊆ b ∧ ∏ i ∈ b, f i ∈ u
⊢ HasProd f a
have apply₆ : ∀ (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)
  (L :
    Tendsto (β := α) (fun (t : Finset ((b : β) × γ b)) ↦ ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ t0, f p) atTop
      (𝓝 (∏ b ∈ t0, g b)))
  (this : ∃ (t : Finset ((b : β) × γ b)), ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ t0, f p ∈ v ∧ s ⊆ t),
  ∃ (b : Finset ((b : β) × γ b)), s ⊆ b ∧ ∏ i ∈ b, f i ∈ u
Tactic: classical
  apply le_nhds_of_cauchy_adhp h
  simp only [← mapClusterPt_def, mapClusterPt_iff_frequently, frequently_atTop, ge_iff_le,
    le_eq_subset]
  intro u hu s
  rcases mem_nhds_iff.1 hu with ⟨v, vu, v_open, hv⟩
  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
  have L : Tendsto (fun t : Finset (Σ b, γ b) ↦ ∏ p ∈ t with p.1 ∈ t0, f p) atTop
      (𝓝 <| ∏ b ∈ t0, 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))
  have : ∃ t, ∏ p ∈ t with p.1 ∈ t0, f p ∈ v ∧ s ⊆ t :=
    ((Tendsto.eventually_mem L (v_open.mem_nhds st0)).and (Ici_mem_atTop _)).exists
  obtain ⟨t, tv, st⟩ := this
  refine ⟨{p ∈ t | p.1 ∈ t0}, fun x hx ↦ ?_, vu tv⟩
  simpa only [mem_filter, st hx, true_and] using ht0 (mem_image_of_mem Sigma.fst hx)