-- Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean
theorem completeSpace (h : RestrictGenTopology {s : Set (Π i, E i) | IsVonNBounded 𝕜 s}) :
    CompleteSpace (ContinuousMultilinearMap 𝕜 E F)

Proof state:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F✝ : Type u_4
inst✝¹⁴ : NormedField 𝕜
inst✝¹³ : (i : ι) → TopologicalSpace (E i)
inst✝¹² : (i : ι) → AddCommGroup (E i)
inst✝¹¹ : (i : ι) → Module 𝕜 (E i)
inst✝¹⁰ : AddCommGroup F✝
inst✝⁹ : Module 𝕜 F✝
inst✝⁸ : UniformSpace F✝
inst✝⁷ : UniformAddGroup F✝
inst✝⁶ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
h : RestrictGenTopology {s | IsVonNBounded 𝕜 s}
F : Type u_4
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : UniformSpace F
inst✝² : UniformAddGroup F
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
hF : T2Space F
H : ∀ {m : (i : ι) → E i}, Continuous fun f => (toFun {s | IsVonNBounded 𝕜 s}) f m
⊢ IsComplete
    ({a | Continuous ((toFun {s | IsVonNBounded 𝕜 s}) a)} ∩
      ((⋂ i,
          ⋂ i_1,
            ⋂ i_2,
              ⋂ i_3,
                {x |
                  (toFun {s | IsVonNBounded 𝕜 s}) x (update i i_1 (i_2 + i_3)) =
                    (toFun {s | IsVonNBounded 𝕜 s}) x (update i i_1 i_2) +
                      (toFun {s | IsVonNBounded 𝕜 s}) x (update i i_1 i_3)}) ∩
        ⋂ i,
          ⋂ i_1,
            ⋂ i_2,
              ⋂ i_3,
                {x |
                  (toFun {s | IsVonNBounded 𝕜 s}) x (update i i_1 (i_2 • i_3)) =
                    i_2 • (toFun {s | IsVonNBounded 𝕜 s}) x (update i i_1 i_3)}))

Tactic:
apply_rules [IsClosed.isComplete, IsClosed.inter]

Result:
case h₁
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F✝ : Type u_4
inst✝¹⁴ : NormedField 𝕜
inst✝¹³ : (i : ι) → TopologicalSpace (E i)
inst✝¹² : (i : ι) → AddCommGroup (E i)
inst✝¹¹ : (i : ι) → Module 𝕜 (E i)
inst✝¹⁰ : AddCommGroup F✝
inst✝⁹ : Module 𝕜 F✝
inst✝⁸ : UniformSpace F✝
inst✝⁷ : UniformAddGroup F✝
inst✝⁶ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
h : RestrictGenTopology {s | IsVonNBounded 𝕜 s}
F : Type u_4
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : UniformSpace F
inst✝² : UniformAddGroup F
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
hF : T2Space F
H : ∀ {m : (i : ι) → E i}, Continuous fun f => (toFun {s | IsVonNBounded 𝕜 s}) f m
⊢ IsClosed {a | Continuous ((toFun {s | IsVonNBounded 𝕜 s}) a)}

case h₂.h₁
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F✝ : Type u_4
inst✝¹⁴ : NormedField 𝕜
inst✝¹³ : (i : ι) → TopologicalSpace (E i)
inst✝¹² : (i : ι) → AddCommGroup (E i)
inst✝¹¹ : (i : ι) → Module 𝕜 (E i)
inst✝¹⁰ : AddCommGroup F✝
inst✝⁹ : Module 𝕜 F✝
inst✝⁸ : UniformSpace F✝
inst✝⁷ : UniformAddGroup F✝
inst✝⁶ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
h : RestrictGenTopology {s | IsVonNBounded 𝕜 s}
F : Type u_4
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : UniformSpace F
inst✝² : UniformAddGroup F
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
hF : T2Space F
H : ∀ {m : (i : ι) → E i}, Continuous fun f => (toFun {s | IsVonNBounded 𝕜 s}) f m
⊢ IsClosed
    (⋂ i,
      ⋂ i_1,
        ⋂ i_2,
          ⋂ i_3,
            {x |
              (toFun {s | IsVonNBounded 𝕜 s}) x (update i i_1 (i_2 + i_3)) =
                (toFun {s | IsVonNBounded 𝕜 s}) x (update i i_1 i_2) +
                  (toFun {s | IsVonNBounded 𝕜 s}) x (update i i_1 i_3)})

case h₂.h₂
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F✝ : Type u_4
inst✝¹⁴ : NormedField 𝕜
inst✝¹³ : (i : ι) → TopologicalSpace (E i)
inst✝¹² : (i : ι) → AddCommGroup (E i)
inst✝¹¹ : (i : ι) → Module 𝕜 (E i)
inst✝¹⁰ : AddCommGroup F✝
inst✝⁹ : Module 𝕜 F✝
inst✝⁸ : UniformSpace F✝
inst✝⁷ : UniformAddGroup F✝
inst✝⁶ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
h : RestrictGenTopology {s | IsVonNBounded 𝕜 s}
F : Type u_4
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : UniformSpace F
inst✝² : UniformAddGroup F
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
hF : T2Space F
H : ∀ {m : (i : ι) → E i}, Continuous fun f => (toFun {s | IsVonNBounded 𝕜 s}) f m
⊢ IsClosed
    (⋂ i,
      ⋂ i_1,
        ⋂ i_2,
          ⋂ i_3,
            {x |
              (toFun {s | IsVonNBounded 𝕜 s}) x (update i i_1 (i_2 • i_3)) =
                i_2 • (toFun {s | IsVonNBounded 𝕜 s}) x (update i i_1 i_3)})

Proof state:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝¹⁰ : NormedField 𝕜
inst✝⁹ : (i : ι) → TopologicalSpace (E i)
inst✝⁸ : (i : ι) → AddCommGroup (E i)
inst✝⁷ : (i : ι) → Module 𝕜 (E i)
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : UniformSpace F
inst✝³ : UniformAddGroup F
inst✝² : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
h : RestrictGenTopology {s | IsVonNBounded 𝕜 s}
⊢ CompleteSpace (ContinuousMultilinearMap 𝕜 E F)

Tactic:
wlog hF : T2Space F generalizing F

Result:
case inr
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝¹⁰ : NormedField 𝕜
inst✝⁹ : (i : ι) → TopologicalSpace (E i)
inst✝⁸ : (i : ι) → AddCommGroup (E i)
inst✝⁷ : (i : ι) → Module 𝕜 (E i)
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : UniformSpace F
inst✝³ : UniformAddGroup F
inst✝² : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
h : RestrictGenTopology {s | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_4} [inst : AddCommGroup F] [inst_1 : Module 𝕜 F] [inst_2 : UniformSpace F] [inst_3 : UniformAddGroup F]
    [inst_4 : ContinuousConstSMul 𝕜 F] [inst_5 : CompleteSpace F],
    T2Space F → CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
hF : ¬T2Space F
⊢ CompleteSpace (ContinuousMultilinearMap 𝕜 E F)

𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F✝ : Type u_4
inst✝¹⁴ : NormedField 𝕜
inst✝¹³ : (i : ι) → TopologicalSpace (E i)
inst✝¹² : (i : ι) → AddCommGroup (E i)
inst✝¹¹ : (i : ι) → Module 𝕜 (E i)
inst✝¹⁰ : AddCommGroup F✝
inst✝⁹ : Module 𝕜 F✝
inst✝⁸ : UniformSpace F✝
inst✝⁷ : UniformAddGroup F✝
inst✝⁶ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
h : RestrictGenTopology {s | IsVonNBounded 𝕜 s}
F : Type u_4
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : UniformSpace F
inst✝² : UniformAddGroup F
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
hF : T2Space F
⊢ CompleteSpace (ContinuousMultilinearMap 𝕜 E F)

Proof state:
case h
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝¹⁰ : NormedField 𝕜
inst✝⁹ : (i : ι) → TopologicalSpace (E i)
inst✝⁸ : (i : ι) → AddCommGroup (E i)
inst✝⁷ : (i : ι) → Module 𝕜 (E i)
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : UniformSpace F
inst✝³ : UniformAddGroup F
inst✝² : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
h : RestrictGenTopology {s | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_4} [inst : AddCommGroup F] [inst_1 : Module 𝕜 F] [inst_2 : UniformSpace F] [inst_3 : UniformAddGroup F]
    [inst_4 : ContinuousConstSMul 𝕜 F] [inst_5 : CompleteSpace F],
    T2Space F → CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
hF : ¬T2Space F
f : ContinuousMultilinearMap 𝕜 E (SeparationQuotient F)
⊢ (SeparationQuotient.mkCLM 𝕜 F).compContinuousMultilinearMap
      ((SeparationQuotient.outCLM 𝕜 F).compContinuousMultilinearMap f) =
    f

Tactic:
simp [DFunLike.ext_iff]

Result:
no goals

Proof state:
case h₁
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F✝ : Type u_4
inst✝¹⁴ : NormedField 𝕜
inst✝¹³ : (i : ι) → TopologicalSpace (E i)
inst✝¹² : (i : ι) → AddCommGroup (E i)
inst✝¹¹ : (i : ι) → Module 𝕜 (E i)
inst✝¹⁰ : AddCommGroup F✝
inst✝⁹ : Module 𝕜 F✝
inst✝⁸ : UniformSpace F✝
inst✝⁷ : UniformAddGroup F✝
inst✝⁶ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
h : RestrictGenTopology {s | IsVonNBounded 𝕜 s}
F : Type u_4
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : UniformSpace F
inst✝² : UniformAddGroup F
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
hF : T2Space F
H : ∀ {m : (i : ι) → E i}, Continuous fun f => (toFun {s | IsVonNBounded 𝕜 s}) f m
⊢ IsClosed {a | Continuous ((toFun {s | IsVonNBounded 𝕜 s}) a)}

Tactic:
exact UniformOnFun.isClosed_setOf_continuous h

Result:
no goals