-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : TopologicalSpace α
f : α →ᵤ[𝔖] β
x : α
hc : ContinuousAt.{u_1, u_2} (Y := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f) x
U : Set (β × β)
hU : U ∈ 𝓤 β
V : Set α
hV : V ∈ 𝔖
hVx : V ∈ 𝓝 x
h :
  ∀ (a : (α →ᵤ[𝔖] β) × α),
    Membership.mem (γ := Set ((α →ᵤ[𝔖] β) × α))
      {x_1 : (α →ᵤ[𝔖] β) × α |
        x_1 ∈
            SProd.sprod (α := Set (α →ᵤ[𝔖] β))
              {g : α →ᵤ[𝔖] β |
                ∀ x ∈ V,
                  Membership.mem (α := β × β) U
                    (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)}
              (V ∩
                preimage.{u_1, u_2} (β := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f : α → β)
                  (UniformSpace.ball ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x) U : Set β)) →
          Membership.mem (γ := Set ((α →ᵤ[𝔖] β) × α))
            {x_2 : (α →ᵤ[𝔖] β) × α |
              (fun (a : (α →ᵤ[𝔖] β) × α) ↦
                  Membership.mem (α := β × β) (SetRel.comp U U)
                    (Function.comp (β := β) (Prod.mk ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f, x).1 (f, x).2))
                        (fun (fx : (α →ᵤ[𝔖] β) × α) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) fx.1 fx.2) a :
                      β × β))
                x_2}
            x_1}
      a
h₁ :
  ∀
    a ∈
      SProd.sprod (α := Set (α →ᵤ[𝔖] β))
        {g : α →ᵤ[𝔖] β |
          ∀ x ∈ V,
            Membership.mem (α := β × β) U
              (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)}
        (V ∩
          preimage.{u_1, u_2} (β := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f : α → β)
            (UniformSpace.ball ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x) U : Set β)),
    Membership.mem (α := β × β) (SetRel.comp U U)
      (Function.comp (β := β) (Prod.mk ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x))
          (fun (fx : (α →ᵤ[𝔖] β) × α) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) fx.1 fx.2) a :
        β × β)
h₂ :
  ∀ (g : α →ᵤ[𝔖] β) (y : α)
    (hg :
      Membership.mem (γ := Set (α →ᵤ[𝔖] β))
        {g : α →ᵤ[𝔖] β |
          ∀ x ∈ V,
            Membership.mem (α := β × β) U
              (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)}
        (g, y).1)
    (hyV : (g, y).2 ∈ V)
    (hy :
      Membership.mem (γ := Set α)
        (preimage.{u_1, u_2} (β := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f : α → β)
          (UniformSpace.ball ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x) U : Set β))
        (g, y).2),
    Membership.mem (α := β × β) (SetRel.comp U U)
      (Function.comp (β := β) (Prod.mk ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x))
          (fun (fx : (α →ᵤ[𝔖] β) × α) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) fx.1 fx.2) (g, y) :
        β × β)
⊢ ∀ᶠ (a : (α →ᵤ[𝔖] β) × α) in 𝓝 (f, x),
    Membership.mem (α := β × β) (SetRel.comp U U)
      (Function.comp (β := β) (Prod.mk ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f, x).1 (f, x).2))
          (fun (fx : (α →ᵤ[𝔖] β) × α) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) fx.1 fx.2) a :
        β × β)

Tactic:
filter_upwards [prod_mem_nhds (UniformOnFun.gen_mem_nhds _ _ _ hV hU)
    (inter_mem hVx <| hc <| UniformSpace.ball_mem_nhds _ hU)]
    with ⟨g, y⟩ ⟨hg, hyV, hy⟩ using ⟨toFun 𝔖 f y, hy, hg y hyV⟩

Premises used: prod_mem_nhds, UniformSpace.ball_mem_nhds, Filter.inter_mem, UniformOnFun.gen_mem_nhds