-- 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 : UniformSpace F
inst_7 : IsUniformAddGroup F
inst_8 : ∀ (i : ι), ContinuousSMul.{u_1, u_3} 𝕜 (E i)
inst_9 : ContinuousConstSMul 𝕜 F
inst_10 : CompleteSpace F
h : IsCoherentWith (X := (i : ι) → E i) {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}
inr :
  ∀
    (this :
      ∀ {F : Type u_4} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F]
        [inst_14 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F),
        CompleteSpace (ContinuousMultilinearMap 𝕜 E F))
    (hF : ¬T2Space F), CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
wlog wlog₁ :
  ∀ {F : Type u_4} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F]
    [inst_14 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F),
    CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
wlog₂ :
  ∀ {F : Type u_4} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F]
    [inst_14 : IsUniformAddGroup F] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F)
    (H :
      ∀ {m : (i : ι) → E i},
        Continuous (Y := F) 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),
    CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
wlog₃ :
  ∀ {F : Type u_4} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F] [IsUniformAddGroup F]
    [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F)
    (H :
      ∀ {m : (i : ι) → E i},
        Continuous (Y := F) 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, _]
            ((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)}
wlog₄ :
  ∀ {F : Type u_4} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F] [IsUniformAddGroup F]
    [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F)
    (H :
      ∀ {m : (i : ι) → E i},
        Continuous (Y := F) 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)
      ({a : ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F |
          Continuous[Pi.topologicalSpace, _]
            ((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)}))
h₁ :
  ∀ {F : Type u_4} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F] [IsUniformAddGroup F]
    [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F)
    (H :
      ∀ {m : (i : ι) → E i},
        Continuous (Y := F) 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),
    IsClosed (X := ((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, _]
          ((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)}
h₂ :
  ∀ {F : Type u_4} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F] [IsUniformAddGroup F]
    [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F)
    (H :
      ∀ {m : (i : ι) → E i},
        Continuous (Y := F) 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),
    IsClosed (X := ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F)
      (⋂ (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)})
h₃ :
  ∀ {F : Type u_4} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F] [IsUniformAddGroup F]
    [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F)
    (H :
      ∀ {m : (i : ι) → E i},
        Continuous (Y := F) 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),
    IsClosed (X := ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] 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)})
h₄ :
  ∀ {F : Type u_4} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F] [IsUniformAddGroup F]
    [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F)
    (H :
      ∀ {m : (i : ι) → E i},
        Continuous (Y := F) 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),
    IsClosed (X := ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] F)
      (⋂ (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)})
h₅ h₆ :
  ∀ {F : Type u_4} [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜 F] [inst_13 : UniformSpace F] [IsUniformAddGroup F]
    [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (hF : T2Space F)
    (H :
      ∀ {m : (i : ι) → E i},
        Continuous (Y := F) 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),
    IsClosed (X := ((i : ι) → E i) →ᵤ[{s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}] 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)})
⊢ CompleteSpace (ContinuousMultilinearMap 𝕜 E F)

Tactic:
classical
  wlog hF : T2Space F generalizing F
  · rw [(isUniformInducing_postcomp (SeparationQuotient.mkCLM _ _)
      SeparationQuotient.isUniformInducing_mk).completeSpace_congr]
    · exact this inferInstance
    · intro f
      use (SeparationQuotient.outCLM _ _).compContinuousMultilinearMap f
      simp [DFunLike.ext_iff]
  have H : ∀ {m : Π i, E i},
      Continuous fun f : (Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F ↦ toFun _ f m :=
    (uniformContinuous_eval (sUnion_isVonNBounded_eq_univ) _).continuous
  rw [completeSpace_iff_isComplete_range isUniformInducing_toUniformOnFun, range_toUniformOnFun]
  simp only [setOf_and, setOf_forall]
  apply_rules [IsClosed.isComplete, IsClosed.inter]
  · exact UniformOnFun.isClosed_setOf_continuous h
  · exact isClosed_iInter fun m ↦ isClosed_iInter fun i ↦
      isClosed_iInter fun x ↦ isClosed_iInter fun y ↦ isClosed_eq H (H.add H)
  · exact isClosed_iInter fun m ↦ isClosed_iInter fun i ↦
      isClosed_iInter fun c ↦ isClosed_iInter fun x ↦ isClosed_eq H (H.const_smul _)

Premises used: Set.setOf_and, ContinuousMultilinearMap.range_toUniformOnFun, DFunLike.ext_iff, T2Space, UniformOnFun.isClosed_setOf_continuous, IsClosed.inter, IsClosed.isComplete, ContinuousMultilinearMap.isUniformInducing_postcomp, completeSpace_iff_isComplete_range, Set.setOf_forall, IsUniformInducing.completeSpace_congr, ContinuousMultilinearMap.isUniformInducing_toUniformOnFun