-- Mathlib/Topology/Algebra/Module/Alternating/Topology.lean
theorem completeSpace (h : RestrictGenTopology {s : Set (ι → E) | IsVonNBounded 𝕜 s}) :
    CompleteSpace (E [⋀^ι]→L[𝕜] F)

Proof state:
case inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst✝¹⁰ : NormedField 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : UniformSpace F
inst✝³ : UniformAddGroup F
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
h : RestrictGenTopology {s | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_3} [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 (E [⋀^ι]→L[𝕜] F)
hF : ¬T2Space F
⊢ CompleteSpace (E [⋀^ι]→L[𝕜] SeparationQuotient F)

Tactic:
exact this inferInstance

Result:
no goals

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst✝¹⁰ : NormedField 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : UniformSpace F
inst✝³ : UniformAddGroup F
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
h : RestrictGenTopology {s | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_3} [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 (E [⋀^ι]→L[𝕜] F)
hF : ¬T2Space F
f : E [⋀^ι]→L[𝕜] SeparationQuotient F
⊢ (SeparationQuotient.mkCLM 𝕜 F).compContinuousAlternatingMap
      ((SeparationQuotient.outCLM 𝕜 F).compContinuousAlternatingMap f) =
    f

Tactic:
ext

Result:
case h.H
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst✝¹⁰ : NormedField 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : UniformSpace F
inst✝³ : UniformAddGroup F
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
h : RestrictGenTopology {s | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_3} [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 (E [⋀^ι]→L[𝕜] F)
hF : ¬T2Space F
f : E [⋀^ι]→L[𝕜] SeparationQuotient F
x✝ : ι → E
⊢ ((SeparationQuotient.mkCLM 𝕜 F).compContinuousAlternatingMap
        ((SeparationQuotient.outCLM 𝕜 F).compContinuousAlternatingMap f))
      x✝ =
    f x✝

Proof state:
case inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst✝¹⁰ : NormedField 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : UniformSpace F
inst✝³ : UniformAddGroup F
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
h : RestrictGenTopology {s | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_3} [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 (E [⋀^ι]→L[𝕜] F)
hF : ¬T2Space F
⊢ CompleteSpace (E [⋀^ι]→L[𝕜] F)

Tactic:
rw [(isUniformInducing_postcomp (SeparationQuotient.mkCLM _ _)
  SeparationQuotient.isUniformInducing_mk).completeSpace_congr]

Result:
case inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst✝¹⁰ : NormedField 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : UniformSpace F
inst✝³ : UniformAddGroup F
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
h : RestrictGenTopology {s | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_3} [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 (E [⋀^ι]→L[𝕜] F)
hF : ¬T2Space F
⊢ CompleteSpace (E [⋀^ι]→L[𝕜] SeparationQuotient F)

case inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst✝¹⁰ : NormedField 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : UniformSpace F
inst✝³ : UniformAddGroup F
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
h : RestrictGenTopology {s | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_3} [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 (E [⋀^ι]→L[𝕜] F)
hF : ¬T2Space F
⊢ Surjective (SeparationQuotient.mkCLM 𝕜 F).compContinuousAlternatingMap

Proof state:
case inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst✝¹⁰ : NormedField 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : UniformSpace F
inst✝³ : UniformAddGroup F
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
h : RestrictGenTopology {s | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_3} [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 (E [⋀^ι]→L[𝕜] F)
hF : ¬T2Space F
⊢ Surjective (SeparationQuotient.mkCLM 𝕜 F).compContinuousAlternatingMap

Tactic:
intro f

Result:
case inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst✝¹⁰ : NormedField 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : UniformSpace F
inst✝³ : UniformAddGroup F
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
h : RestrictGenTopology {s | IsVonNBounded 𝕜 s}
this :
  ∀ {F : Type u_3} [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 (E [⋀^ι]→L[𝕜] F)
hF : ¬T2Space F
f : E [⋀^ι]→L[𝕜] SeparationQuotient F
⊢ ∃ a, (SeparationQuotient.mkCLM 𝕜 F).compContinuousAlternatingMap a = f

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

Tactic:
have := ContinuousMultilinearMap.completeSpace (F := F) h

Result:
𝕜 : Type u_1
E : Type u_2
F✝ : Type u_3
ι : Type u_4
inst✝¹⁴ : NormedField 𝕜
inst✝¹³ : AddCommGroup E
inst✝¹² : Module 𝕜 E
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : AddCommGroup F✝
inst✝⁹ : Module 𝕜 F✝
inst✝⁸ : UniformSpace F✝
inst✝⁷ : UniformAddGroup F✝
inst✝⁶ : ContinuousSMul 𝕜 E
h : RestrictGenTopology {s | IsVonNBounded 𝕜 s}
F : Type u_3
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : UniformSpace F
inst✝² : UniformAddGroup F
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : CompleteSpace F
hF : T2Space F
this : CompleteSpace (ContinuousMultilinearMap 𝕜 (fun i => E) F)
⊢ CompleteSpace (E [⋀^ι]→L[𝕜] F)