-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology
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
h :
  ∀ (f : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] 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
⊢ Eq (α := Set (((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F))
    (range (ι := ContinuousMultilinearMap 𝕜 E F) (toUniformOnFun (E := E)))
    {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)}

Tactic:
ext f