-- Mathlib/Topology/Algebra/Module/StrongTopology.lean
theorem completeSpace [UniformSpace F] [UniformAddGroup F] [ContinuousSMul 𝕜₂ F] [CompleteSpace F]
    {𝔖 : Set (Set E)} (h𝔖 : RestrictGenTopology 𝔖) (h𝔖U : ⋃₀ 𝔖 = univ) :
    CompleteSpace (UniformConvergenceCLM σ F 𝔖)

Proof state:
case inr
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜₁ E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : UniformSpace F
inst✝² : UniformAddGroup F
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : CompleteSpace F
𝔖 : Set (Set E)
h𝔖 : RestrictGenTopology 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
this :
  ∀ (F : Type u_4) [inst : AddCommGroup F] [inst_1 : Module 𝕜₂ F] [inst_2 : UniformSpace F] [inst_3 : UniformAddGroup F]
    [inst_4 : ContinuousSMul 𝕜₂ F] [inst_5 : CompleteSpace F], T2Space F → CompleteSpace (UniformConvergenceCLM σ F 𝔖)
hF : ¬T2Space F
⊢ CompleteSpace (UniformConvergenceCLM σ (SeparationQuotient F) 𝔖)

case inr
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜₁ E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : UniformSpace F
inst✝² : UniformAddGroup F
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : CompleteSpace F
𝔖 : Set (Set E)
h𝔖 : RestrictGenTopology 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
this :
  ∀ (F : Type u_4) [inst : AddCommGroup F] [inst_1 : Module 𝕜₂ F] [inst_2 : UniformSpace F] [inst_3 : UniformAddGroup F]
    [inst_4 : ContinuousSMul 𝕜₂ F] [inst_5 : CompleteSpace F], T2Space F → CompleteSpace (UniformConvergenceCLM σ F 𝔖)
hF : ¬T2Space F
⊢ Surjective (SeparationQuotient.mkCLM 𝕜₂ F).comp

Tactic:
exacts [this _ inferInstance, SeparationQuotient.postcomp_mkCLM_surjective F σ E]

Result:
no goals

Proof state:
case h
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NormedField 𝕜₁
inst✝¹¹ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F✝ : Type u_4
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜₁ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F✝
inst✝⁶ : Module 𝕜₂ F✝
𝔖 : Set (Set E)
h𝔖 : RestrictGenTopology 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
F : Type u_4
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : UniformSpace F
inst✝² : UniformAddGroup F
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : CompleteSpace F
hF : T2Space F
⊢ IsClosed (range (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe))

Tactic:
have H₁ : IsClosed {f : E →ᵤ[𝔖] F | Continuous ((UniformOnFun.toFun 𝔖) f)} :=
  UniformOnFun.isClosed_setOf_continuous h𝔖

Result:
case h
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NormedField 𝕜₁
inst✝¹¹ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F✝ : Type u_4
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜₁ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F✝
inst✝⁶ : Module 𝕜₂ F✝
𝔖 : Set (Set E)
h𝔖 : RestrictGenTopology 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
F : Type u_4
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : UniformSpace F
inst✝² : UniformAddGroup F
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : CompleteSpace F
hF : T2Space F
H₁ : IsClosed {f | Continuous ((UniformOnFun.toFun 𝔖) f)}
⊢ IsClosed (range (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe))

Proof state:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜₁ E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : UniformSpace F
inst✝² : UniformAddGroup F
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : CompleteSpace F
𝔖 : Set (Set E)
h𝔖 : RestrictGenTopology 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
⊢ CompleteSpace (UniformConvergenceCLM σ F 𝔖)

Tactic:
wlog hF : T2Space F generalizing F

Result:
case inr
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜₁ E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : UniformSpace F
inst✝² : UniformAddGroup F
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : CompleteSpace F
𝔖 : Set (Set E)
h𝔖 : RestrictGenTopology 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
this :
  ∀ (F : Type u_4) [inst : AddCommGroup F] [inst_1 : Module 𝕜₂ F] [inst_2 : UniformSpace F] [inst_3 : UniformAddGroup F]
    [inst_4 : ContinuousSMul 𝕜₂ F] [inst_5 : CompleteSpace F], T2Space F → CompleteSpace (UniformConvergenceCLM σ F 𝔖)
hF : ¬T2Space F
⊢ CompleteSpace (UniformConvergenceCLM σ F 𝔖)

𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NormedField 𝕜₁
inst✝¹¹ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F✝ : Type u_4
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜₁ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F✝
inst✝⁶ : Module 𝕜₂ F✝
𝔖 : Set (Set E)
h𝔖 : RestrictGenTopology 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
F : Type u_4
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : UniformSpace F
inst✝² : UniformAddGroup F
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : CompleteSpace F
hF : T2Space F
⊢ CompleteSpace (UniformConvergenceCLM σ F 𝔖)

Proof state:
case h.e'_3
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NormedField 𝕜₁
inst✝¹¹ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F✝ : Type u_4
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜₁ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F✝
inst✝⁶ : Module 𝕜₂ F✝
𝔖 : Set (Set E)
h𝔖 : RestrictGenTopology 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
F : Type u_4
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : UniformSpace F
inst✝² : UniformAddGroup F
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : CompleteSpace F
hF : T2Space F
H₁ : IsClosed {f | Continuous ((UniformOnFun.toFun 𝔖) f)}
⊢ range (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) =
    {f | Continuous ((UniformOnFun.toFun 𝔖) f)} ∩ ⇑(UniformOnFun.toFun 𝔖) ⁻¹' range DFunLike.coe

Tactic:
exact ContinuousLinearMap.range_coeFn_eq

Result:
no goals