-- 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
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 : DecidableEq ι
inst_7 : TopologicalSpace F
f : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F
h :
  Membership.mem (γ := Set (((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F))
      (range (ι := ContinuousMultilinearMap 𝕜 E F) (toUniformOnFun (E := E))) f →
    Membership.mem (γ := Set (((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F))
      {f : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F |
        Continuous[Pi.topologicalSpace, inst_7]
            ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
              f) ∧
          (∀ (m : (i : ι) → E i) (i : ι) (x y : E i),
              (toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                    (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
                  f (update (β := E) m i (x + y)) =
                HAdd.hAdd (α := F) (β := F)
                  ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                        (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
                      f (update (β := E) m i x) :
                    F)
                  ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                        (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
                      f (update (β := E) m i y) :
                    F)) ∧
            ∀ (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i),
              (toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                    (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
                  f (update (β := E) m i (c • x)) =
                HSMul.hSMul (β := F) c
                  ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                        (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
                      f (update (β := E) m i x) :
                    F)}
      f
⊢ Membership.mem (γ := Set (((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F))
      (range (ι := ContinuousMultilinearMap 𝕜 E F) (toUniformOnFun (E := E))) f ↔
    Membership.mem (γ := Set (((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F))
      {f : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F |
        Continuous[Pi.topologicalSpace, inst_7]
            ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
              f) ∧
          (∀ (m : (i : ι) → E i) (i : ι) (x y : E i),
              (toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                    (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
                  f (update (β := E) m i (x + y)) =
                HAdd.hAdd (α := F) (β := F)
                  ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                        (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
                      f (update (β := E) m i x) :
                    F)
                  ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                        (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
                      f (update (β := E) m i y) :
                    F)) ∧
            ∀ (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i),
              (toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                    (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
                  f (update (β := E) m i (c • x)) =
                HSMul.hSMul (β := F) c
                  ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                        (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
                      f (update (β := E) m i x) :
                    F)}
      f
have h₁ : Membership.mem (γ := Set (((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F))
    {f : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F |
      Continuous[Pi.topologicalSpace, inst_7]
          ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
              (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
            f) ∧
        (∀ (m : (i : ι) → E i) (i : ι) (x y : E i),
            (toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                  (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
                f (update (β := E) m i (x + y)) =
              HAdd.hAdd (α := F) (β := F)
                ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                      (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
                    f (update (β := E) m i x) :
                  F)
                ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                      (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
                    f (update (β := E) m i y) :
                  F)) ∧
          ∀ (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i),
            (toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                  (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
                f (update (β := E) m i (c • x)) =
              HSMul.hSMul (β := F) c
                ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                      (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
                    f (update (β := E) m i x) :
                  F)}
    f →
  Membership.mem (γ := Set (((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F))
    (range (ι := ContinuousMultilinearMap 𝕜 E F) (toUniformOnFun (E := E))) f
Tactic: constructor