-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F_1 : 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_1
inst_5 : Module 𝕜 F_1
inst_6 : UniformSpace F_1
inst_7 : IsUniformAddGroup F_1
inst_8 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
h : IsCoherentWith (X := (i : ι) → E i) {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}
F : Type u_4
inst_9 : AddCommGroup F
inst_10 : Module 𝕜 F
inst_11 : UniformSpace F
inst_12 : IsUniformAddGroup F
inst_13 : ContinuousConstSMul 𝕜 F
inst_14 : CompleteSpace F
hF : T2Space F
H :
  ∀ {m : (i : ι) → E i},
    Continuous[topologicalSpace ((i : ι) → E i) F {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s},
        inst_11.toTopologicalSpace]
      fun (f : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] 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 m
⊢ IsComplete (α := ((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_11.toTopologicalSpace]
          ((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)}
have simp : IsComplete (α := ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F)
  ({a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F |
      Continuous[Pi.topologicalSpace, inst_11.toTopologicalSpace]
        ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
            (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) → ((i : ι) → E i) → F)
          a)} ∩
    ((⋂ (i : (i : ι) → E i),
        ⋂ (i_1 : ι),
          ⋂ (i_2 : E i_1),
            ⋂ (i_3 : E i_1),
              {x : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] 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)
                    x (update (β := E) i i_1 (i_2 + i_3)) =
                  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)
                        x (update (β := E) i i_1 i_2) :
                      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)
                        x (update (β := E) i i_1 i_3) :
                      F)}) ∩
      ⋂ (i : (i : ι) → E i),
        ⋂ (i_1 : ι),
          ⋂ (i_2 : 𝕜),
            ⋂ (i_3 : E i_1),
              {x : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] 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)
                    x (update (β := E) i i_1 (i_2 • i_3)) =
                  HSMul.hSMul (β := F) i_2
                    ((toFun {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s} :
                          (a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F) →
                            ((i : ι) → E i) → F)
                        x (update (β := E) i i_1 i_3) :
                      F)}))
Tactic: simp only [setOf_and, setOf_forall]