-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
G : Type u_5
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
inst_8 : ContinuousConstSMul 𝕜 F
inst_9 : AddCommGroup G
inst_10 : Module 𝕜 G
inst_11 : TopologicalSpace G
inst_12 : IsTopologicalAddGroup G
inst_13 : ContinuousConstSMul 𝕜 G
aux : (F →L[𝕜] G) →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G :=
  {
    toFun := fun (g : F →L[𝕜] G) ↦
      { toFun := g.compContinuousMultilinearMap (M₁ := E), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ },
    map_add' := ⋯, map_smul' := ⋯ }
U : Set (ContinuousMultilinearMap 𝕜 E F)
V : Set ((i : ι) → E i)
W : Set G
hU : IsVonNBounded 𝕜 (U, V, W).1
hV : IsVonNBounded 𝕜 (U, V, W).2.1
hW : Membership.mem (γ := Filter G) (𝓝 0) (U, V, W).2.2
refine_1 :
  IsVonNBounded.{u_1, u_4} 𝕜 (E := F)
    (image2 (fun (f : ContinuousMultilinearMap 𝕜 E F) (v : (i : ι) → E i) ↦ (f : (a : (i : ι) → E i) → F) v) U V, W).1
⊢ ∃ (ia : Prod.{u_4, u_5} (Set F) (Set G)),
    (IsVonNBounded 𝕜 ia.1 ∧ Membership.mem (γ := Filter G) (𝓝 0) ia.2) ∧
      ∀ (x : F →L[𝕜] G),
        Membership.mem (γ := Set (F →L[𝕜] G))
            {f : F →L[𝕜] G | ∀ x ∈ ia.1, Membership.mem (α := G) ia.2 ((f : (a : F) → G) x : G)} x →
          Membership.mem (α := ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G) (γ :=
            Set (ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G))
            {f : ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G |
              ∀ x ∈ (U, V, W).1,
                Membership.mem (α := ContinuousMultilinearMap 𝕜 E G) (γ := Set (ContinuousMultilinearMap 𝕜 E G))
                  {f : ContinuousMultilinearMap 𝕜 E G |
                    MapsTo (⇑f : (a : (i : ι) → E i) → G) (U, V, W).2.1 (U, V, W).2.2}
                  ((f : (a : ContinuousMultilinearMap 𝕜 E F) → ContinuousMultilinearMap 𝕜 E G) x :
                    ContinuousMultilinearMap 𝕜 E G)}
            ((aux : (a : F →L[𝕜] G) → ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G) x :
              ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G)
have refine_2 : ∀ (x : F →L[𝕜] G),
  Membership.mem (γ := Set (F →L[𝕜] G))
      {f : F →L[𝕜] G |
        ∀ (x : F),
          Membership.mem (γ := Set F)
              (image2 (fun (f : ContinuousMultilinearMap 𝕜 E F) (v : (i : ι) → E i) ↦ (f : (a : (i : ι) → E i) → F) v) U
                    V,
                  W).1
              x →
            Membership.mem (α := G)
              (image2 (fun (f : ContinuousMultilinearMap 𝕜 E F) (v : (i : ι) → E i) ↦ (f : (a : (i : ι) → E i) → F) v) U
                    V,
                  W).2
              ((f : (a : F) → G) x : G)}
      x →
    Membership.mem (α := ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G) (γ :=
      Set (ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G))
      {f : ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G |
        ∀ x ∈ (U, V, W).1,
          Membership.mem (α := ContinuousMultilinearMap 𝕜 E G) (γ := Set (ContinuousMultilinearMap 𝕜 E G))
            {f : ContinuousMultilinearMap 𝕜 E G | MapsTo (⇑f : (a : (i : ι) → E i) → G) (U, V, W).2.1 (U, V, W).2.2}
            ((f : (a : ContinuousMultilinearMap 𝕜 E F) → ContinuousMultilinearMap 𝕜 E G) x :
              ContinuousMultilinearMap 𝕜 E G)}
      ((aux : (a : F →L[𝕜] G) → ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G) x :
        ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G)
Tactic: refine ⟨(.image2 (fun f v ↦ f v) U V, W), ⟨?_, hW⟩, ?_⟩