-- 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
⊢ CompleteSpace (ContinuousMultilinearMap 𝕜 E F)

Tactic:
have H : ∀ {m : Π i, E i},
    Continuous fun f : (Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F ↦ toFun _ f m :=
  (uniformContinuous_eval (isVonNBounded_covers) _).continuous

Result:
𝕜 : 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
⊢ 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
    {f |
      Continuous ((toFun {s | IsVonNBounded 𝕜 s}) f) ∧
        (∀ (m : (i : ι) → E i) (i : ι) (x y : E i),
            (toFun {s | IsVonNBounded 𝕜 s}) f (update m i (x + y)) =
              (toFun {s | IsVonNBounded 𝕜 s}) f (update m i x) + (toFun {s | IsVonNBounded 𝕜 s}) f (update m i y)) ∧
          ∀ (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i),
            (toFun {s | IsVonNBounded 𝕜 s}) f (update m i (c • x)) =
              c • (toFun {s | IsVonNBounded 𝕜 s}) f (update m i x)}

Tactic:
simp only [setOf_and, setOf_forall]

Result:
𝕜 : 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)}))

Proof state:
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)})

Tactic:
exact isClosed_iInter fun m ↦ isClosed_iInter fun i ↦
  isClosed_iInter fun x ↦ isClosed_iInter fun y ↦ isClosed_eq H (H.add H)

Result:
no goals

Proof state:
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 (SeparationQuotient F))

Tactic:
exact this inferInstance

Result:
no goals

Proof state:
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)})

Tactic:
exact isClosed_iInter fun m ↦ isClosed_iInter fun i ↦
  isClosed_iInter fun c ↦ isClosed_iInter fun x ↦ isClosed_eq H (H.const_smul _)

Result:
no goals