-- 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
h₁ :
  IsClosed[(uniformSpace ((i : ι) → E i) F {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}).toTopologicalSpace]
    {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)}
⊢ 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)}))
have h₂ : IsClosed[(uniformSpace ((i : ι) → E i) F {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}).toTopologicalSpace]
  (⋂ (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)})
Tactic: apply_rules [IsClosed.isComplete, IsClosed.inter]