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
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
𝔖 : Set (Set E)
⊢ IsTopologicalAddGroup.rightUniformSpace F = inst_7

Tactic:
exact IsUniformAddGroup.rightUniformSpace_eq

Premises used: IsUniformAddGroup.rightUniformSpace_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
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 : UniformSpace F
inst_8 : IsUniformAddGroup F
𝔖 : Set (Set E)
rw :
  Eq (α := TopologicalSpace (UniformConvergenceCLM σ F 𝔖))
    (TopologicalSpace.induced (DFunLike.coe (β := fun (a : E) ↦ F)) (UniformOnFun.topologicalSpace E F 𝔖))
    UniformSpace.toTopologicalSpace
⊢ Eq (α := TopologicalSpace (UniformConvergenceCLM σ F 𝔖)) (instTopologicalSpace σ F 𝔖) UniformSpace.toTopologicalSpace

Tactic:
rw [UniformConvergenceCLM.instTopologicalSpace, IsUniformAddGroup.rightUniformSpace_eq]

Premises used: IsUniformAddGroup.rightUniformSpace_eq, UniformConvergenceCLM.instTopologicalSpace
-- 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 : UniformSpace F
inst_8 : IsUniformAddGroup F
𝔖 : Set (Set E)
⊢ Eq (α := TopologicalSpace (UniformConvergenceCLM σ F 𝔖))
    (TopologicalSpace.induced (DFunLike.coe (β := fun (a : E) ↦ F)) (UniformOnFun.topologicalSpace E F 𝔖))
    UniformSpace.toTopologicalSpace

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
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
𝔖 : Set (Set E)
rw :
  Eq (α := UniformSpace (UniformConvergenceCLM σ F 𝔖))
    (UniformSpace.replaceTopology
      (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 𝔖))
rw₁ rw₂ :
  Eq (α := 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 𝔖))
⊢ Eq (α := UniformSpace (UniformConvergenceCLM σ F 𝔖)) (instUniformSpace σ F 𝔖)
    (UniformSpace.comap
      (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F)))
      (UniformOnFun.uniformSpace E F 𝔖))

Tactic:
rw [instUniformSpace, UniformSpace.replaceTopology_eq]

Premises used: UniformConvergenceCLM.instUniformSpace, UniformSpace.replaceTopology_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
inst_7 : UniformSpace F
inst_8 : IsUniformAddGroup F
𝔖 : Set (Set E)
⊢ Eq (α := TopologicalSpace (UniformConvergenceCLM σ F 𝔖)) UniformSpace.toTopologicalSpace (instTopologicalSpace σ F 𝔖)

Tactic:
rfl

Premises used: 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
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
𝔖 : Set (Set E)
⊢ IsUniformInducing (α := UniformConvergenceCLM σ F 𝔖) (β := E →ᵤ[𝔖] F)
    (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F)))

Tactic:
⟨rfl⟩

Premises used: IsUniformInducing.mk, 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
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
𝔖 : Set (Set E)
⊢ IsUniformEmbedding (α := UniformConvergenceCLM σ F 𝔖) (β := E →ᵤ[𝔖] F)
    (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F)))

Tactic:
⟨isUniformInducing_coeFn .., DFunLike.coe_injective⟩

Premises used: UniformConvergenceCLM.isUniformInducing_coeFn, IsUniformEmbedding.mk, DFunLike.coe_injective
-- 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
𝔖 : Set (Set E)
⊢ IsEmbedding (X := UniformConvergenceCLM σ F 𝔖) (Y := E →ᵤ[𝔖] F)
    (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F)))

Tactic:
IsUniformEmbedding.isEmbedding (isUniformEmbedding_coeFn _ _ _)

Premises used: IsUniformEmbedding.isEmbedding, UniformConvergenceCLM.isUniformEmbedding_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
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
𝔖 : Set (Set E)
f : UniformConvergenceCLM σ F 𝔖
x : E
⊢ Eq.{u_4 + 1} (α := F) ((-f : (a : E) → F) x : F) (-(f : (a : E) → F) x : F)

Tactic:
rfl

Premises used: 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
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
𝔖 : Set (Set E)
f g : UniformConvergenceCLM σ F 𝔖
x : E
⊢ (f + g : (a : E) → F) x = HAdd.hAdd (α := F) (β := F) ((f : (a : E) → F) x : F) ((g : (a : E) → F) x : F)

Tactic:
rfl

Premises used: 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
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
ι : Type u_6
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
𝔖 : Set (Set E)
t : Finset ι
f : ι → UniformConvergenceCLM σ F 𝔖
x : E
⊢ Eq.{u_4 + 1} (α := F) ((∑ d ∈ t, f d : (a : E) → F) x : F) (∑ d ∈ t, (f d : (a : E) → F) x : F)

Tactic:
ContinuousLinearMap.sum_apply t f x

Premises used: ContinuousLinearMap.sum_apply, 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 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
𝔖 : Set (Set E)
f g : UniformConvergenceCLM σ F 𝔖
x : E
⊢ (f - g : (a : E) → F) x = HSub.hSub (α := F) (β := F) ((f : (a : E) → F) x : F) ((g : (a : E) → F) x : F)

Tactic:
rfl

Premises used: 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
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
𝔖 : Set (Set E)
⊢ Eq (α := (a : E) → F) (⇑0 : (a : E) → F) 0

Tactic:
rfl

Premises used: 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 : UniformSpace F
inst_8 : IsUniformAddGroup F
𝔖 : Set (Set E)
φ : UniformConvergenceCLM σ F 𝔖 →+ E →ᵤ[𝔖] F :=
  { toFun := DFunLike.coe (β := fun (a : E) ↦ F), map_zero' := ⋯, map_add' := ⋯ }
⊢ IsUniformAddGroup (UniformConvergenceCLM σ F 𝔖)

Tactic:
(isUniformEmbedding_coeFn _ _ _).isUniformAddGroup φ

Premises used: IsUniformInducing.isUniformAddGroup, IsUniformEmbedding.toIsUniformInducing, UniformConvergenceCLM.isUniformEmbedding_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 : UniformSpace F
inst_8 : IsUniformAddGroup F
𝔖 : Set (Set E)
φ : UniformConvergenceCLM σ F 𝔖 →+ E →ᵤ[𝔖] F :=
  { toFun := DFunLike.coe (β := fun (a : E) ↦ F), map_zero' := ⋯, map_add' := ⋯ }
⊢ IsUniformAddGroup (UniformConvergenceCLM σ F 𝔖)

Tactic:
exact (isUniformEmbedding_coeFn _ _ _).isUniformAddGroup φ

Premises used: IsUniformInducing.isUniformAddGroup, IsUniformEmbedding.toIsUniformInducing, UniformConvergenceCLM.isUniformEmbedding_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 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
𝔖 : Set (Set E)
this : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
⊢ IsUniformAddGroup F

Tactic:
haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
-- 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 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
𝔖 : Set (Set E)
this_1 : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ IsTopologicalAddGroup (UniformConvergenceCLM σ F 𝔖)

Tactic:
infer_instance
-- 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 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
𝔖 : Set (Set E)
h𝔖 : ⋃₀ 𝔖 = univ
x : E
this : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
⊢ IsUniformAddGroup F

Tactic:
haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
-- 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 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
𝔖 : Set (Set E)
h𝔖 : ⋃₀ 𝔖 = univ
x : E
this_1 : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ Continuous[instTopologicalSpace σ F 𝔖, inst_7] fun (f : UniformConvergenceCLM σ F 𝔖) ↦ (f : (a : E) → F) x

Tactic:
(UniformOnFun.uniformContinuous_eval h𝔖 x).continuous.comp
      (isEmbedding_coeFn σ F 𝔖).continuous

Premises used: UniformConvergenceCLM.isEmbedding_coeFn, UniformOnFun.uniformContinuous_eval, Continuous.comp, UniformContinuous.continuous, Topology.IsEmbedding.continuous
-- 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 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
𝔖 : Set (Set E)
h𝔖 : ⋃₀ 𝔖 = univ
x : E
this_1 : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ Continuous[instTopologicalSpace σ F 𝔖, inst_7] fun (f : UniformConvergenceCLM σ F 𝔖) ↦ (f : (a : E) → F) x

Tactic:
exact (UniformOnFun.uniformContinuous_eval h𝔖 x).continuous.comp
      (isEmbedding_coeFn σ F 𝔖).continuous

Premises used: UniformConvergenceCLM.isEmbedding_coeFn, UniformOnFun.uniformContinuous_eval, Continuous.comp, UniformContinuous.continuous, Topology.IsEmbedding.continuous
-- 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 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
inst_9 : T2Space F
𝔖 : Set (Set E)
h𝔖 : ⋃₀ 𝔖 = univ
this : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
⊢ IsUniformAddGroup F

Tactic:
haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
-- 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 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
inst_9 : T2Space F
𝔖 : Set (Set E)
h𝔖 : ⋃₀ 𝔖 = univ
this_1 : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ T2Space (E →ᵤ[𝔖] F)

Tactic:
haveI : T2Space (E →ᵤ[𝔖] F) := UniformOnFun.t2Space_of_covering 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 : 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 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
inst_9 : T2Space F
𝔖 : Set (Set E)
h𝔖 : ⋃₀ 𝔖 = univ
this_1 : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this_2 : IsUniformAddGroup F
this : T2Space (E →ᵤ[𝔖] F)
⊢ T2Space (UniformConvergenceCLM σ F 𝔖)

Tactic:
(isEmbedding_coeFn σ F 𝔖).t2Space

Premises used: UniformConvergenceCLM.isEmbedding_coeFn, Topology.IsEmbedding.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 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
inst_9 : T2Space F
𝔖 : Set (Set E)
h𝔖 : ⋃₀ 𝔖 = univ
this_1 : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this_2 : IsUniformAddGroup F
this : T2Space (E →ᵤ[𝔖] F)
⊢ T2Space (UniformConvergenceCLM σ F 𝔖)

Tactic:
exact (isEmbedding_coeFn σ F 𝔖).t2Space

Premises used: UniformConvergenceCLM.isEmbedding_coeFn, Topology.IsEmbedding.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
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)
c : M
f : UniformConvergenceCLM σ F 𝔖
x : E
⊢ (c • f : (a : E) → F) x = HSMul.hSMul (β := F) c ((f : (a : E) → F) x : F)

Tactic:
rfl

Premises used: 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
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
inst_7 : RingHomSurjective σ
inst_8 : RingHomIsometric σ
inst_9 : TopologicalSpace F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul 𝕜₂ F
𝔖 : Set (Set E)
h𝔖₃ : ∀ S ∈ 𝔖, IsVonNBounded 𝕜₁ S
this : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
⊢ IsUniformAddGroup F

Tactic:
haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
-- 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 : RingHomSurjective σ
inst_8 : RingHomIsometric σ
inst_9 : TopologicalSpace F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul 𝕜₂ F
𝔖 : Set (Set E)
h𝔖₃ : ∀ S ∈ 𝔖, IsVonNBounded 𝕜₁ S
this_1 : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
φ : UniformConvergenceCLM σ F 𝔖 →ₗ[𝕜₂] E → F :=
  { toFun := DFunLike.coe (β := fun (a : E) ↦ F), map_add' := ⋯, map_smul' := ⋯ }
⊢ ContinuousSMul 𝕜₂ (UniformConvergenceCLM σ F 𝔖)

Tactic:
UniformOnFun.continuousSMul_induced_of_image_bounded 𝕜₂ E F (E →SLᵤ[σ, 𝔖] F) φ
    ⟨rfl⟩ fun u s hs => (h𝔖₃ s hs).image u

Premises used: UniformOnFun.continuousSMul_induced_of_image_bounded, Topology.IsInducing.mk, Bornology.IsVonNBounded.image, UniformConvergenceCLM, 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
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
inst_7 : RingHomSurjective σ
inst_8 : RingHomIsometric σ
inst_9 : TopologicalSpace F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul 𝕜₂ F
𝔖 : Set (Set E)
h𝔖₃ : ∀ S ∈ 𝔖, IsVonNBounded 𝕜₁ S
this_1 : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
φ : UniformConvergenceCLM σ F 𝔖 →ₗ[𝕜₂] E → F :=
  { toFun := DFunLike.coe (β := fun (a : E) ↦ F), map_add' := ⋯, map_smul' := ⋯ }
⊢ ContinuousSMul 𝕜₂ (UniformConvergenceCLM σ F 𝔖)

Tactic:
exact UniformOnFun.continuousSMul_induced_of_image_bounded 𝕜₂ E F (E →SLᵤ[σ, 𝔖] F) φ
    ⟨rfl⟩ fun u s hs => (h𝔖₃ s hs).image u

Premises used: UniformOnFun.continuousSMul_induced_of_image_bounded, Topology.IsInducing.mk, Bornology.IsVonNBounded.image, UniformConvergenceCLM, 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
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
ι : Type u_6
𝔖 : Set (Set E)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) 𝔖
p : ι → Prop
b : ι → Set F
h : HasBasis (𝓝 0) p b
this : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
⊢ IsUniformAddGroup F

Tactic:
haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
-- 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 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
ι : Type u_6
𝔖 : Set (Set E)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) 𝔖
p : ι → Prop
b : ι → Set F
h : HasBasis (𝓝 0) p b
this_1 : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
rw :
  HasBasis (α := UniformConvergenceCLM σ F 𝔖)
    (comap (β := E →ᵤ[𝔖] F)
      (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F)))
      (𝓝
        (comp (α := UniformConvergenceCLM σ F 𝔖) (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F)
          (DFunLike.coe (β := fun (a : E) ↦ F)) 0)))
    (fun (Si : Prod.{u_3, u_6} (Set E) ι) ↦ Si.1 ∈ 𝔖 ∧ p Si.2) fun (Si : Prod.{u_3, u_6} (Set E) ι) ↦
    {f : UniformConvergenceCLM σ F 𝔖 | ∀ x ∈ Si.1, Membership.mem (α := F) (b Si.2) ((f : (a : E) → F) x : F)}
⊢ HasBasis (α := UniformConvergenceCLM σ F 𝔖) (𝓝 0) (fun (Si : Prod.{u_3, u_6} (Set E) ι) ↦ Si.1 ∈ 𝔖 ∧ p Si.2)
    fun (Si : Prod.{u_3, u_6} (Set E) ι) ↦
    {f : UniformConvergenceCLM σ F 𝔖 | ∀ x ∈ Si.1, Membership.mem (α := F) (b Si.2) ((f : (a : E) → F) x : F)}

Tactic:
rw [(isEmbedding_coeFn σ F 𝔖).isInducing.nhds_eq_comap]

Premises used: UniformConvergenceCLM.isEmbedding_coeFn, Topology.IsInducing.nhds_eq_comap, Topology.IsEmbedding.isInducing
-- 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 : TopologicalSpace F
inst_8 : IsTopologicalAddGroup F
ι : Type u_6
𝔖 : Set (Set E)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) 𝔖
p : ι → Prop
b : ι → Set F
h : HasBasis (𝓝 0) p b
this_1 : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ HasBasis (α := UniformConvergenceCLM σ F 𝔖)
    (comap (β := E →ᵤ[𝔖] F)
      (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F)))
      (𝓝
        (comp (α := UniformConvergenceCLM σ F 𝔖) (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F)
          (DFunLike.coe (β := fun (a : E) ↦ F)) 0)))
    (fun (Si : Prod.{u_3, u_6} (Set E) ι) ↦ Si.1 ∈ 𝔖 ∧ p Si.2) fun (Si : Prod.{u_3, u_6} (Set E) ι) ↦
    {f : UniformConvergenceCLM σ F 𝔖 | ∀ x ∈ Si.1, Membership.mem (α := F) (b Si.2) ((f : (a : E) → F) x : F)}

Tactic:
(UniformOnFun.hasBasis_nhds_zero_of_basis 𝔖 h𝔖₁ h𝔖₂ h).comap DFunLike.coe

Premises used: Set.Mem, setOf, instZeroUniformOnFun._aux_1, Filter.HasBasis.comap, Set.preimage, UniformOnFun.hasBasis_nhds_zero_of_basis, UniformOnFun, DFunLike.coe