awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
G : Type u_5
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
M : Type u_6
inst_7 : Monoid M
inst_8 : DistribMulAction M F
inst_9 : SMulCommClass 𝕜₂ M F
inst_10 : TopologicalSpace F
inst_11 : IsTopologicalAddGroup F
inst_12 : ContinuousConstSMul M F
𝔖 : Set (Set E)
⊢ ContinuousConstSMul M (UniformConvergenceCLM σ F 𝔖)

Tactic:
let _ := IsTopologicalAddGroup.rightUniformSpace F
  have _ : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
  have _ := uniformContinuousConstSMul_of_continuousConstSMul M F
  inferInstance

Premises used: inferInstance, uniformContinuousConstSMul_of_continuousConstSMul, isUniformAddGroup_of_addCommGroup, IsTopologicalAddGroup.rightUniformSpace
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
ι : Type u_6
p : Filter ι
inst_7 : UniformSpace F
inst_8 : IsUniformAddGroup F
𝔖 : Set (Set E)
a : ι → UniformConvergenceCLM σ F 𝔖
a₀ : UniformConvergenceCLM σ F 𝔖
rw :
  (∀ s ∈ 𝔖,
      TendstoUniformlyOn.{u_3, u_4, u_6} (β := F)
        (comp (β := E →ᵤ[𝔖] F) (⇑(UniformOnFun.toFun 𝔖) : (a : E →ᵤ[𝔖] F) → E → F)
          (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F)) ∘
            a))
        ((UniformOnFun.toFun 𝔖 : (a : E →ᵤ[𝔖] F) → E → F)
          (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F))
            a₀))
        p s) ↔
    ∀ s ∈ 𝔖,
      TendstoUniformlyOn.{u_3, u_4, u_6} (β := F) (fun (x1 : ι) (x2 : E) ↦ (a x1 : (a : E) → F) x2) (⇑a₀ : (a : E) → F)
        p s
⊢ Tendsto a p (𝓝 a₀) ↔
    ∀ s ∈ 𝔖,
      TendstoUniformlyOn.{u_3, u_4, u_6} (β := F) (fun (x1 : ι) (x2 : E) ↦ (a x1 : (a : E) → F) x2) (⇑a₀ : (a : E) → F)
        p s

Tactic:
rw [(isEmbedding_coeFn σ F 𝔖).tendsto_nhds_iff, UniformOnFun.tendsto_iff_tendstoUniformlyOn]

Premises used: UniformConvergenceCLM.isEmbedding_coeFn, UniformOnFun.tendsto_iff_tendstoUniformlyOn, Topology.IsEmbedding.tendsto_nhds_iff
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
ι : Type u_6
p : Filter ι
inst_7 : UniformSpace F
inst_8 : IsUniformAddGroup F
𝔖 : Set (Set E)
a : ι → UniformConvergenceCLM σ F 𝔖
a₀ : UniformConvergenceCLM σ F 𝔖
⊢ (∀ s ∈ 𝔖,
      TendstoUniformlyOn.{u_3, u_4, u_6} (β := F)
        (comp (β := E →ᵤ[𝔖] F) (⇑(UniformOnFun.toFun 𝔖) : (a : E →ᵤ[𝔖] F) → E → F)
          (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F)) ∘
            a))
        ((UniformOnFun.toFun 𝔖 : (a : E →ᵤ[𝔖] F) → E → F)
          (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F))
            a₀))
        p s) ↔
    ∀ s ∈ 𝔖,
      TendstoUniformlyOn.{u_3, u_4, u_6} (β := F) (fun (x1 : ι) (x2 : E) ↦ (a x1 : (a : E) → F) x2) (⇑a₀ : (a : E) → F)
        p s

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
G : Type u_5
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
inst_7 : AddCommGroup G
inst_8 : UniformSpace G
inst_9 : IsUniformAddGroup G
𝕜₃ : Type u_6
inst_10 : NormedField 𝕜₃
inst_11 : Module 𝕜₃ G
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_12 : RingHomCompTriple σ τ ρ
inst_13 : UniformSpace F
inst_14 : IsUniformAddGroup F
g : F →SL[τ] G
hg : IsUniformInducing.{u_4, u_5} (α := F) (β := G) (⇑g : (a : F) → G)
𝔖 : Set (Set E)
rw :
  IsUniformInducing (α := UniformConvergenceCLM σ F 𝔖) (β := E →ᵤ[𝔖] G)
    (comp (β := E → G) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → G) → E →ᵤ[𝔖] G) (DFunLike.coe (β := fun (a : E) ↦ G)) ∘
      g.comp)
⊢ IsUniformInducing (α := UniformConvergenceCLM σ F 𝔖) g.comp

Tactic:
rw [← (isUniformInducing_coeFn _ _ _).of_comp_iff]

Premises used: IsUniformInducing.of_comp_iff, UniformConvergenceCLM.isUniformInducing_coeFn
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
G : Type u_5
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
inst_7 : AddCommGroup G
inst_8 : UniformSpace G
inst_9 : IsUniformAddGroup G
𝕜₃ : Type u_6
inst_10 : NormedField 𝕜₃
inst_11 : Module 𝕜₃ G
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_12 : RingHomCompTriple σ τ ρ
inst_13 : UniformSpace F
inst_14 : IsUniformAddGroup F
g : F →SL[τ] G
hg : IsUniformInducing.{u_4, u_5} (α := F) (β := G) (⇑g : (a : F) → G)
𝔖 : Set (Set E)
⊢ IsUniformInducing (α := UniformConvergenceCLM σ F 𝔖) (β := E →ᵤ[𝔖] G)
    (comp (β := E → G) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → G) → E →ᵤ[𝔖] G) (DFunLike.coe (β := fun (a : E) ↦ G)) ∘
      g.comp)

Tactic:
(UniformOnFun.postcomp_isUniformInducing hg).comp (isUniformInducing_coeFn _ _ _)

Premises used: UniformOnFun.postcomp_isUniformInducing, UniformConvergenceCLM.isUniformInducing_coeFn, IsUniformInducing.comp
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
G : Type u_5
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
inst_7 : AddCommGroup G
inst_8 : UniformSpace G
inst_9 : IsUniformAddGroup G
𝕜₃ : Type u_6
inst_10 : NormedField 𝕜₃
inst_11 : Module 𝕜₃ G
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_12 : RingHomCompTriple σ τ ρ
inst_13 : UniformSpace F
inst_14 : IsUniformAddGroup F
g : F →SL[τ] G
hg : IsUniformInducing.{u_4, u_5} (α := F) (β := G) (⇑g : (a : F) → G)
𝔖 : Set (Set E)
⊢ IsUniformInducing (α := UniformConvergenceCLM σ F 𝔖) (β := E →ᵤ[𝔖] G)
    (comp (β := E → G) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → G) → E →ᵤ[𝔖] G) (DFunLike.coe (β := fun (a : E) ↦ G)) ∘
      g.comp)

Tactic:
exact (UniformOnFun.postcomp_isUniformInducing hg).comp (isUniformInducing_coeFn _ _ _)

Premises used: UniformOnFun.postcomp_isUniformInducing, UniformConvergenceCLM.isUniformInducing_coeFn, IsUniformInducing.comp
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
G : Type u_5
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
inst_7 : AddCommGroup G
inst_8 : UniformSpace G
inst_9 : IsUniformAddGroup G
𝕜₃ : Type u_6
inst_10 : NormedField 𝕜₃
inst_11 : Module 𝕜₃ G
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_12 : RingHomCompTriple σ τ ρ
inst_13 : UniformSpace F
inst_14 : IsUniformAddGroup F
g : F →SL[τ] G
hg : IsUniformEmbedding.{u_4, u_5} (α := F) (β := G) (⇑g : (a : F) → G)
𝔖 : Set (Set E)
⊢ IsUniformEmbedding (α := UniformConvergenceCLM σ F 𝔖) g.comp

Tactic:
.mk (isUniformInducing_postcomp _ g hg.isUniformInducing _) fun _ _ ↦ g.cancel_left hg.injective

Premises used: IsUniformEmbedding.injective, IsUniformEmbedding.isUniformInducing, IsUniformEmbedding.mk, UniformConvergenceCLM.isUniformInducing_postcomp, ContinuousLinearMap.cancel_left
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace F
inst_8 : IsUniformAddGroup F
inst_9 : ContinuousSMul 𝕜₂ F
inst_10 : CompleteSpace F
𝔖 : Set (Set E)
h𝔖 : IsCoherentWith 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
inr :
  ∀
    (this :
      ∀ (F : Type u_4) [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜₂ F] [inst_13 : UniformSpace F]
        [inst_14 : IsUniformAddGroup F] [ContinuousSMul 𝕜₂ F] [CompleteSpace F] (hF : T2Space F),
        CompleteSpace (UniformConvergenceCLM σ F 𝔖))
    (hF : ¬T2Space F), CompleteSpace (UniformConvergenceCLM σ F 𝔖)
wlog :
  ∀ (F : Type u_4) [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜₂ F] [inst_13 : UniformSpace F]
    [inst_14 : IsUniformAddGroup F] [ContinuousSMul 𝕜₂ F] [CompleteSpace F] (hF : T2Space F),
    CompleteSpace (UniformConvergenceCLM σ F 𝔖)
⊢ CompleteSpace (UniformConvergenceCLM σ F 𝔖)

Tactic:
wlog hF : T2Space F generalizing F

Premises used: T2Space
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace F
inst_8 : IsUniformAddGroup F
inst_9 : ContinuousSMul 𝕜₂ F
inst_10 : CompleteSpace F
𝔖 : Set (Set E)
h𝔖 : IsCoherentWith 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
this :
  ∀ (F : Type u_4) [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜₂ F] [inst_13 : UniformSpace F]
    [inst_14 : IsUniformAddGroup F] [ContinuousSMul 𝕜₂ F] [CompleteSpace F] (hF : T2Space F),
    CompleteSpace (UniformConvergenceCLM σ F 𝔖)
hF : ¬T2Space F
inr : CompleteSpace (UniformConvergenceCLM.{u_1, u_2, u_3, u_4} σ (SeparationQuotient F) 𝔖)
inr₁ :
  Surjective (α := UniformConvergenceCLM σ F 𝔖) (β :=
    UniformConvergenceCLM.{u_1, u_2, u_3, u_4} σ (SeparationQuotient F) 𝔖)
    (ContinuousLinearMap.comp (SeparationQuotient.mkCLM 𝕜₂ F))
⊢ CompleteSpace (UniformConvergenceCLM σ F 𝔖)

Tactic:
rw [(isUniformInducing_postcomp σ (SeparationQuotient.mkCLM 𝕜₂ F)
      SeparationQuotient.isUniformInducing_mk _).completeSpace_congr]

Premises used: SeparationQuotient.mkCLM, SeparationQuotient.isUniformInducing_mk, IsUniformInducing.completeSpace_congr, UniformConvergenceCLM.isUniformInducing_postcomp
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace F
inst_8 : IsUniformAddGroup F
inst_9 : ContinuousSMul 𝕜₂ F
inst_10 : CompleteSpace F
𝔖 : Set (Set E)
h𝔖 : IsCoherentWith 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
this :
  ∀ (F : Type u_4) [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜₂ F] [inst_13 : UniformSpace F]
    [inst_14 : IsUniformAddGroup F] [ContinuousSMul 𝕜₂ F] [CompleteSpace F] (hF : T2Space F),
    CompleteSpace (UniformConvergenceCLM σ F 𝔖)
hF : ¬T2Space F
⊢ CompleteSpace (UniformConvergenceCLM.{u_1, u_2, u_3, u_4} σ (SeparationQuotient F) 𝔖)

Tactic:
this _ inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace F
inst_8 : IsUniformAddGroup F
inst_9 : ContinuousSMul 𝕜₂ F
inst_10 : CompleteSpace F
𝔖 : Set (Set E)
h𝔖 : IsCoherentWith 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
this :
  ∀ (F : Type u_4) [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜₂ F] [inst_13 : UniformSpace F]
    [inst_14 : IsUniformAddGroup F] [ContinuousSMul 𝕜₂ F] [CompleteSpace F] (hF : T2Space F),
    CompleteSpace (UniformConvergenceCLM σ F 𝔖)
hF : ¬T2Space F
⊢ Surjective (α := UniformConvergenceCLM σ F 𝔖) (β :=
    UniformConvergenceCLM.{u_1, u_2, u_3, u_4} σ (SeparationQuotient F) 𝔖)
    (ContinuousLinearMap.comp (SeparationQuotient.mkCLM 𝕜₂ F))

Tactic:
SeparationQuotient.postcomp_mkCLM_surjective F σ E

Premises used: SeparationQuotient.postcomp_mkCLM_surjective, UniformConvergenceCLM
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
inst_7 : UniformSpace F
inst_8 : IsUniformAddGroup F
inst_9 : ContinuousSMul 𝕜₂ F
inst_10 : CompleteSpace F
𝔖 : Set (Set E)
h𝔖 : IsCoherentWith 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
this :
  ∀ (F : Type u_4) [inst_11 : AddCommGroup F] [inst_12 : Module 𝕜₂ F] [inst_13 : UniformSpace F]
    [inst_14 : IsUniformAddGroup F] [ContinuousSMul 𝕜₂ F] [CompleteSpace F] (hF : T2Space F),
    CompleteSpace (UniformConvergenceCLM σ F 𝔖)
hF : ¬T2Space F
⊢ CompleteSpace (UniformConvergenceCLM.{u_1, u_2, u_3, u_4} σ (SeparationQuotient F) 𝔖)

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

Premises used: inferInstance, SeparationQuotient.postcomp_mkCLM_surjective
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F_1 : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂ F_1
𝔖 : Set (Set E)
h𝔖 : IsCoherentWith 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
F : Type u_4
inst_7 : AddCommGroup F
inst_8 : Module 𝕜₂ F
inst_9 : UniformSpace F
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₂ F
inst_12 : CompleteSpace F
hF : T2Space F
rw :
  IsComplete (α := E →ᵤ[𝔖] F)
    (range (ι := UniformConvergenceCLM σ F 𝔖)
      (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F))))
⊢ CompleteSpace (UniformConvergenceCLM σ F 𝔖)

Tactic:
rw [completeSpace_iff_isComplete_range (isUniformInducing_coeFn _ _ _)]

Premises used: UniformConvergenceCLM.isUniformInducing_coeFn, completeSpace_iff_isComplete_range
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F_1 : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂ F_1
𝔖 : Set (Set E)
h𝔖 : IsCoherentWith 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
F : Type u_4
inst_7 : AddCommGroup F
inst_8 : Module 𝕜₂ F
inst_9 : UniformSpace F
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₂ F
inst_12 : CompleteSpace F
hF : T2Space F
h :
  IsClosed[(UniformOnFun.uniformSpace E F 𝔖).toTopologicalSpace]
    (range (ι := UniformConvergenceCLM σ F 𝔖)
      (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F))))
⊢ IsComplete (α := E →ᵤ[𝔖] F)
    (range (ι := UniformConvergenceCLM σ F 𝔖)
      (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F))))

Tactic:
apply IsClosed.isComplete

Premises used: IsClosed.isComplete
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F_1 : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂ F_1
𝔖 : Set (Set E)
h𝔖 : IsCoherentWith 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
F : Type u_4
inst_7 : AddCommGroup F
inst_8 : Module 𝕜₂ F
inst_9 : UniformSpace F
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₂ F
inst_12 : CompleteSpace F
hF : T2Space F
⊢ IsClosed[UniformOnFun.topologicalSpace E F 𝔖]
    {f : E →ᵤ[𝔖] F | Continuous[inst_4, inst_9.toTopologicalSpace] ((UniformOnFun.toFun 𝔖 : (a : E →ᵤ[𝔖] F) → E → F) f)}

Tactic:
have H₁ : IsClosed {f : E →ᵤ[𝔖] F | Continuous ((UniformOnFun.toFun 𝔖) f)} :=
    UniformOnFun.isClosed_setOf_continuous h𝔖
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F_1 : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂ F_1
𝔖 : Set (Set E)
h𝔖 : IsCoherentWith 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
F : Type u_4
inst_7 : AddCommGroup F
inst_8 : Module 𝕜₂ F
inst_9 : UniformSpace F
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₂ F
inst_12 : CompleteSpace F
hF : T2Space F
H₁ :
  IsClosed[UniformOnFun.topologicalSpace E F 𝔖]
    {f : E →ᵤ[𝔖] F | Continuous[inst_4, inst_9.toTopologicalSpace] ((UniformOnFun.toFun 𝔖 : (a : E →ᵤ[𝔖] F) → E → F) f)}
⊢ IsClosed[UniformOnFun.topologicalSpace E F 𝔖]
    ({f : E →ᵤ[𝔖] F |
        Continuous[inst_4, inst_9.toTopologicalSpace] ((UniformOnFun.toFun 𝔖 : (a : E →ᵤ[𝔖] F) → E → F) f)} ∩
      preimage (β := E → F) (⇑(UniformOnFun.toFun 𝔖) : (a : E →ᵤ[𝔖] F) → E → F)
        (range (ι := E →ₛₗ[σ] F) (DFunLike.coe (β := fun (x : E) ↦ F))))

Tactic:
H₁.inter <|
      (LinearMap.isClosed_range_coe E F σ).preimage
        (UniformOnFun.uniformContinuous_toFun h𝔖U).continuous

Premises used: LinearMap.isClosed_range_coe, UniformOnFun.uniformContinuous_toFun, UniformContinuous.continuous, IsClosed.preimage, IsClosed.inter
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F_1 : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂ F_1
𝔖 : Set (Set E)
h𝔖 : IsCoherentWith 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
F : Type u_4
inst_7 : AddCommGroup F
inst_8 : Module 𝕜₂ F
inst_9 : UniformSpace F
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₂ F
inst_12 : CompleteSpace F
hF : T2Space F
H₁ :
  IsClosed[UniformOnFun.topologicalSpace E F 𝔖]
    {f : E →ᵤ[𝔖] F | Continuous[inst_4, inst_9.toTopologicalSpace] ((UniformOnFun.toFun 𝔖 : (a : E →ᵤ[𝔖] F) → E → F) f)}
h :
  Eq (α := Set (E →ᵤ[𝔖] F))
    (range (ι := UniformConvergenceCLM σ F 𝔖)
      (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F))))
    ({f : E →ᵤ[𝔖] F |
        Continuous[inst_4, inst_9.toTopologicalSpace] ((UniformOnFun.toFun 𝔖 : (a : E →ᵤ[𝔖] F) → E → F) f)} ∩
      preimage (β := E → F) (⇑(UniformOnFun.toFun 𝔖) : (a : E →ᵤ[𝔖] F) → E → F)
        (range (ι := E →ₛₗ[σ] F) (DFunLike.coe (β := fun (x : E) ↦ F))))
⊢ IsClosed[(UniformOnFun.uniformSpace E F 𝔖).toTopologicalSpace]
    (range (ι := UniformConvergenceCLM σ F 𝔖)
      (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F))))

Tactic:
convert!
    H₁.inter <|
      (LinearMap.isClosed_range_coe E F σ).preimage
        (UniformOnFun.uniformContinuous_toFun h𝔖U).continuous

Premises used: LinearMap.isClosed_range_coe, UniformOnFun.uniformContinuous_toFun, UniformContinuous.continuous, IsClosed.preimage, IsClosed.inter
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F_1 : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂ F_1
𝔖 : Set (Set E)
h𝔖 : IsCoherentWith 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
F : Type u_4
inst_7 : AddCommGroup F
inst_8 : Module 𝕜₂ F
inst_9 : UniformSpace F
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₂ F
inst_12 : CompleteSpace F
hF : T2Space F
H₁ :
  IsClosed[UniformOnFun.topologicalSpace E F 𝔖]
    {f : E →ᵤ[𝔖] F | Continuous[inst_4, inst_9.toTopologicalSpace] ((UniformOnFun.toFun 𝔖 : (a : E →ᵤ[𝔖] F) → E → F) f)}
⊢ Eq (α := Set (E →ᵤ[𝔖] F))
    (range (ι := UniformConvergenceCLM σ F 𝔖)
      (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F))))
    ({f : E →ᵤ[𝔖] F |
        Continuous[inst_4, inst_9.toTopologicalSpace] ((UniformOnFun.toFun 𝔖 : (a : E →ᵤ[𝔖] F) → E → F) f)} ∩
      preimage (β := E → F) (⇑(UniformOnFun.toFun 𝔖) : (a : E →ᵤ[𝔖] F) → E → F)
        (range (ι := E →ₛₗ[σ] F) (DFunLike.coe (β := fun (x : E) ↦ F))))

Tactic:
ContinuousLinearMap.range_coeFn_eq

Premises used: Set.Mem, setOf, ContinuousLinearMap.range_coeFn_eq, Set.preimage, UniformOnFun, Set.range, UniformConvergenceCLM
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F_1 : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂ F_1
𝔖 : Set (Set E)
h𝔖 : IsCoherentWith 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
F : Type u_4
inst_7 : AddCommGroup F
inst_8 : Module 𝕜₂ F
inst_9 : UniformSpace F
inst_10 : IsUniformAddGroup F
inst_11 : ContinuousSMul 𝕜₂ F
inst_12 : CompleteSpace F
hF : T2Space F
H₁ :
  IsClosed[UniformOnFun.topologicalSpace E F 𝔖]
    {f : E →ᵤ[𝔖] F | Continuous[inst_4, inst_9.toTopologicalSpace] ((UniformOnFun.toFun 𝔖 : (a : E →ᵤ[𝔖] F) → E → F) f)}
⊢ Eq (α := Set (E →ᵤ[𝔖] F))
    (range (ι := UniformConvergenceCLM σ F 𝔖)
      (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F))))
    ({f : E →ᵤ[𝔖] F |
        Continuous[inst_4, inst_9.toTopologicalSpace] ((UniformOnFun.toFun 𝔖 : (a : E →ᵤ[𝔖] F) → E → F) f)} ∩
      preimage (β := E → F) (⇑(UniformOnFun.toFun 𝔖) : (a : E →ᵤ[𝔖] F) → E → F)
        (range (ι := E →ₛₗ[σ] F) (DFunLike.coe (β := fun (x : E) ↦ F))))

Tactic:
exact ContinuousLinearMap.range_coeFn_eq

Premises used: ContinuousLinearMap.range_coeFn_eq
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
𝔖₁ 𝔖₂ : Set (Set E)
inst_7 : UniformSpace F
inst_8 : IsUniformAddGroup F
h : 𝔖₂ ⊆ 𝔖₁
simp_rw :
  LE.le (α := UniformSpace (UniformConvergenceCLM σ F 𝔖₁))
    (UniformSpace.comap
      (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖₁) : (a : E → F) → E →ᵤ[𝔖₁] F) (DFunLike.coe (β := fun (a : E) ↦ F)))
      (UniformOnFun.uniformSpace E F 𝔖₁))
    (UniformSpace.comap
      (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖₂) : (a : E → F) → E →ᵤ[𝔖₂] F) (DFunLike.coe (β := fun (a : E) ↦ F)))
      (UniformOnFun.uniformSpace E F 𝔖₂))
⊢ LE.le (α := UniformSpace (UniformConvergenceCLM σ F 𝔖₁)) (instUniformSpace σ F 𝔖₁) (instUniformSpace σ F 𝔖₂)

Tactic:
simp_rw [uniformSpace_eq]

Premises used: UniformConvergenceCLM.uniformSpace_eq
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
𝔖₁ 𝔖₂ : Set (Set E)
inst_7 : UniformSpace F
inst_8 : IsUniformAddGroup F
h : 𝔖₂ ⊆ 𝔖₁
⊢ LE.le (α := UniformSpace (UniformConvergenceCLM σ F 𝔖₁))
    (UniformSpace.comap
      (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖₁) : (a : E → F) → E →ᵤ[𝔖₁] F) (DFunLike.coe (β := fun (a : E) ↦ F)))
      (UniformOnFun.uniformSpace E F 𝔖₁))
    (UniformSpace.comap
      (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖₂) : (a : E → F) → E →ᵤ[𝔖₂] F) (DFunLike.coe (β := fun (a : E) ↦ F)))
      (UniformOnFun.uniformSpace E F 𝔖₂))

Tactic:
UniformSpace.comap_mono (UniformOnFun.mono (le_refl _) h)

Premises used: le_refl, UniformOnFun.mono, Set.Mem, setOf, UniformSpace.comap_mono, UniformOnFun, UniformConvergenceCLM