awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₂ : Type u_2
inst : NormedField 𝕜₂
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜₂ F
𝕜₁ : Type u_6
inst_5 : NontriviallyNormedField 𝕜₁
σ : 𝕜₁ →+* 𝕜₂
inst_6 : Module 𝕜₁ E
inst_7 : AddCommGroup G
𝕜₃ : Type u_7
inst_8 : NormedField 𝕜₃
inst_9 : Module 𝕜₃ G
τ : 𝕜₃ →+* 𝕜₂
inst_10 : RingHomSurjective τ
inst_11 : TopologicalSpace F
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜₂ F
inst_14 : TopologicalSpace G
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜₃ G
𝔖 : Set (Set E)
h𝔖 : ∀ s ∈ 𝔖, IsVonNBounded 𝕜₁ s
B : G →ₛₗ[τ] UniformConvergenceCLM σ F 𝔖
hB :
  Continuous[instTopologicalSpaceProd, inst_11] fun (p : G × E) ↦
    (((B : (a : G) → UniformConvergenceCLM σ F 𝔖) p.1 : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) p.2
S : Set E
hS : S ∈ 𝔖
U : Set F
hU : Membership.mem (γ := Filter F) (𝓝 0) U
V : Set G
hV : Membership.mem (γ := Filter G) (𝓝 0) V
W : Set E
hW : Membership.mem (γ := Filter E) (𝓝 0) W
hVW :
  V ×ˢ W ⊆
    (fun (p : G × E) ↦
        (((B : (a : G) → UniformConvergenceCLM σ F 𝔖) p.1 : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) p.2) ⁻¹'
      U
c : 𝕜₁
hc : MapsTo (fun (x : E) ↦ c • x) S W
c_ne : c ≠ 0
d : 𝕜₃
hd : Eq.{u_2 + 1} (α := 𝕜₂) ((τ : (a : 𝕜₃) → 𝕜₂) d : 𝕜₂) ((σ : (a : 𝕜₁) → 𝕜₂) c : 𝕜₂)
d_ne : d ≠ 0
a : G
ha : a ∈ V
x : E
hx : x ∈ S
⊢ Membership.mem (α := F) U
    ((((B : (a : G) → UniformConvergenceCLM σ F 𝔖) a : UniformConvergenceCLM σ F 𝔖) : (a : E) → F) (c • x) : F)

Tactic:
exact @hVW ⟨_, _⟩ ⟨ha, hc hx⟩

Premises used: And.intro
-- 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 : ContinuousConstSMul 𝕜₂ F
𝔖 : Set (Set E)
A : E →SL[σ] F
x : E
⊢ Eq.{u_4 + 1} (α := F)
    ((((ContinuousLinearMap.toUniformConvergenceCLM σ F 𝔖 : (a : E →SL[σ] F) → UniformConvergenceCLM σ F 𝔖) A :
            UniformConvergenceCLM σ F 𝔖) :
          (a : E) → F)
        x :
      F)
    ((A : (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
inst_9 : ContinuousConstSMul 𝕜₂ F
𝔖 : Set (Set E)
A : UniformConvergenceCLM σ F 𝔖
x : E
⊢ Eq.{u_4 + 1} (α := F)
    ((((LinearEquiv.symm (ContinuousLinearMap.toUniformConvergenceCLM σ F 𝔖) :
                (a : UniformConvergenceCLM σ F 𝔖) → E →SL[σ] F)
              A :
            E →SL[σ] F) :
          (a : E) → F)
        x :
      F)
    ((A : (a : E) → F) x : F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁_1 : Type u_1
𝕜₂_1 : Type u_2
inst : NormedField 𝕜₁_1
inst_1 : NormedField 𝕜₂_1
σ_1 : 𝕜₁_1 →+* 𝕜₂_1
E_1 : Type u_3
F_1 : Type u_4
G_1 : Type u_5
inst_2 : AddCommGroup E_1
inst_3 : Module 𝕜₁_1 E_1
inst_4 : TopologicalSpace E_1
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂_1 F_1
𝕜₁ : Type u_6
𝕜₂ : Type u_7
𝕜₃ : Type u_8
inst_7 : NormedField 𝕜₁
inst_8 : NormedField 𝕜₂
inst_9 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_10 : RingHomCompTriple σ τ ρ
E : Type u_9
F : Type u_10
G : Type u_11
inst_11 : AddCommGroup E
inst_12 : Module 𝕜₁ E
inst_13 : AddCommGroup F
inst_14 : Module 𝕜₂ F
inst_15 : AddCommGroup G
inst_16 : Module 𝕜₃ G
inst_17 : TopologicalSpace E
inst_18 : TopologicalSpace F
inst_19 : TopologicalSpace G
𝔖 : Set (Set E)
𝔗 : Set (Set F)
inst_20 : IsTopologicalAddGroup G
inst_21 : ContinuousConstSMul 𝕜₃ G
L : E →SL[σ] F
hL : MapsTo (fun (x : Set E) ↦ (⇑L : (a : E) → F) '' x) 𝔖 𝔗
this : UniformSpace G := IsTopologicalAddGroup.rightUniformSpace G
⊢ IsUniformAddGroup G

Tactic:
haveI : IsUniformAddGroup G := isUniformAddGroup_of_addCommGroup
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁_1 : Type u_1
𝕜₂_1 : Type u_2
inst : NormedField 𝕜₁_1
inst_1 : NormedField 𝕜₂_1
σ_1 : 𝕜₁_1 →+* 𝕜₂_1
E_1 : Type u_3
F_1 : Type u_4
G_1 : Type u_5
inst_2 : AddCommGroup E_1
inst_3 : Module 𝕜₁_1 E_1
inst_4 : TopologicalSpace E_1
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂_1 F_1
𝕜₁ : Type u_6
𝕜₂ : Type u_7
𝕜₃ : Type u_8
inst_7 : NormedField 𝕜₁
inst_8 : NormedField 𝕜₂
inst_9 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_10 : RingHomCompTriple σ τ ρ
E : Type u_9
F : Type u_10
G : Type u_11
inst_11 : AddCommGroup E
inst_12 : Module 𝕜₁ E
inst_13 : AddCommGroup F
inst_14 : Module 𝕜₂ F
inst_15 : AddCommGroup G
inst_16 : Module 𝕜₃ G
inst_17 : TopologicalSpace E
inst_18 : TopologicalSpace F
inst_19 : TopologicalSpace G
𝔖 : Set (Set E)
𝔗 : Set (Set F)
inst_20 : IsTopologicalAddGroup G
inst_21 : ContinuousConstSMul 𝕜₃ G
L : E →SL[σ] F
hL : MapsTo (fun (x : Set E) ↦ (⇑L : (a : E) → F) '' x) 𝔖 𝔗
this_1 : UniformSpace G := IsTopologicalAddGroup.rightUniformSpace G
this : IsUniformAddGroup G
rw :
  Continuous[UniformConvergenceCLM.instTopologicalSpace τ G 𝔗, UniformOnFun.topologicalSpace E G 𝔖]
    (Function.comp (β := UniformConvergenceCLM ρ G 𝔖)
      (Function.comp (β := E → G) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → G) → E →ᵤ[𝔖] G)
        (DFunLike.coe (β := fun (a : E) ↦ G)))
      fun (f : UniformConvergenceCLM τ G 𝔗) ↦ f ∘SL L)
⊢ Continuous[UniformConvergenceCLM.instTopologicalSpace τ G 𝔗, UniformConvergenceCLM.instTopologicalSpace ρ G 𝔖]
    fun (f : UniformConvergenceCLM τ G 𝔗) ↦ f ∘SL L

Tactic:
rw [(UniformConvergenceCLM.isEmbedding_coeFn _ _ _).continuous_iff]

Premises used: UniformConvergenceCLM.isEmbedding_coeFn, Topology.IsEmbedding.continuous_iff
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁_1 : Type u_1
𝕜₂_1 : Type u_2
inst : NormedField 𝕜₁_1
inst_1 : NormedField 𝕜₂_1
σ_1 : 𝕜₁_1 →+* 𝕜₂_1
E_1 : Type u_3
F_1 : Type u_4
G_1 : Type u_5
inst_2 : AddCommGroup E_1
inst_3 : Module 𝕜₁_1 E_1
inst_4 : TopologicalSpace E_1
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂_1 F_1
𝕜₁ : Type u_6
𝕜₂ : Type u_7
𝕜₃ : Type u_8
inst_7 : NormedField 𝕜₁
inst_8 : NormedField 𝕜₂
inst_9 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_10 : RingHomCompTriple σ τ ρ
E : Type u_9
F : Type u_10
G : Type u_11
inst_11 : AddCommGroup E
inst_12 : Module 𝕜₁ E
inst_13 : AddCommGroup F
inst_14 : Module 𝕜₂ F
inst_15 : AddCommGroup G
inst_16 : Module 𝕜₃ G
inst_17 : TopologicalSpace E
inst_18 : TopologicalSpace F
inst_19 : TopologicalSpace G
𝔖 : Set (Set E)
𝔗 : Set (Set F)
inst_20 : IsTopologicalAddGroup G
inst_21 : ContinuousConstSMul 𝕜₃ G
L : E →SL[σ] F
hL : MapsTo (fun (x : Set E) ↦ (⇑L : (a : E) → F) '' x) 𝔖 𝔗
this_1 : UniformSpace G := IsTopologicalAddGroup.rightUniformSpace G
this : IsUniformAddGroup G
⊢ Continuous[UniformConvergenceCLM.instTopologicalSpace τ G 𝔗, UniformOnFun.topologicalSpace E G 𝔖]
    (Function.comp (β := UniformConvergenceCLM ρ G 𝔖)
      (Function.comp (β := E → G) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → G) → E →ᵤ[𝔖] G)
        (DFunLike.coe (β := fun (a : E) ↦ G)))
      fun (f : UniformConvergenceCLM τ G 𝔗) ↦ f ∘SL L)

Tactic:
(UniformOnFun.precomp_uniformContinuous hL).continuous.comp
        (UniformConvergenceCLM.isEmbedding_coeFn _ _ _).continuous

Premises used: UniformConvergenceCLM.isEmbedding_coeFn, Continuous.comp, UniformContinuous.continuous, UniformOnFun.precomp_uniformContinuous, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁_1 : Type u_1
𝕜₂_1 : Type u_2
inst : NormedField 𝕜₁_1
inst_1 : NormedField 𝕜₂_1
σ_1 : 𝕜₁_1 →+* 𝕜₂_1
E_1 : Type u_3
F_1 : Type u_4
G_1 : Type u_5
inst_2 : AddCommGroup E_1
inst_3 : Module 𝕜₁_1 E_1
inst_4 : TopologicalSpace E_1
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂_1 F_1
𝕜₁ : Type u_6
𝕜₂ : Type u_7
𝕜₃ : Type u_8
inst_7 : NormedField 𝕜₁
inst_8 : NormedField 𝕜₂
inst_9 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_10 : RingHomCompTriple σ τ ρ
E : Type u_9
F : Type u_10
G : Type u_11
inst_11 : AddCommGroup E
inst_12 : Module 𝕜₁ E
inst_13 : AddCommGroup F
inst_14 : Module 𝕜₂ F
inst_15 : AddCommGroup G
inst_16 : Module 𝕜₃ G
inst_17 : TopologicalSpace E
inst_18 : TopologicalSpace F
inst_19 : TopologicalSpace G
𝔖 : Set (Set E)
𝔗 : Set (Set F)
inst_20 : IsTopologicalAddGroup G
inst_21 : ContinuousConstSMul 𝕜₃ G
L : E →SL[σ] F
hL : MapsTo (fun (x : Set E) ↦ (⇑L : (a : E) → F) '' x) 𝔖 𝔗
this_1 : UniformSpace G := IsTopologicalAddGroup.rightUniformSpace G
this : IsUniformAddGroup G
⊢ Continuous[UniformConvergenceCLM.instTopologicalSpace τ G 𝔗, UniformOnFun.topologicalSpace E G 𝔖]
    (Function.comp (β := UniformConvergenceCLM ρ G 𝔖)
      (Function.comp (β := E → G) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → G) → E →ᵤ[𝔖] G)
        (DFunLike.coe (β := fun (a : E) ↦ G)))
      fun (f : UniformConvergenceCLM τ G 𝔗) ↦ f ∘SL L)

Tactic:
exact (UniformOnFun.precomp_uniformContinuous hL).continuous.comp
        (UniformConvergenceCLM.isEmbedding_coeFn _ _ _).continuous

Premises used: UniformConvergenceCLM.isEmbedding_coeFn, Continuous.comp, UniformContinuous.continuous, UniformOnFun.precomp_uniformContinuous, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁_1 : Type u_1
𝕜₂_1 : Type u_2
inst : NormedField 𝕜₁_1
inst_1 : NormedField 𝕜₂_1
σ_1 : 𝕜₁_1 →+* 𝕜₂_1
E_1 : Type u_3
F_1 : Type u_4
G_1 : Type u_5
inst_2 : AddCommGroup E_1
inst_3 : Module 𝕜₁_1 E_1
inst_4 : TopologicalSpace E_1
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂_1 F_1
𝕜₁ : Type u_6
𝕜₂ : Type u_7
𝕜₃ : Type u_8
inst_7 : NormedField 𝕜₁
inst_8 : NormedField 𝕜₂
inst_9 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_10 : RingHomCompTriple σ τ ρ
E : Type u_9
F : Type u_10
G : Type u_11
inst_11 : AddCommGroup E
inst_12 : Module 𝕜₁ E
inst_13 : AddCommGroup F
inst_14 : Module 𝕜₂ F
inst_15 : AddCommGroup G
inst_16 : Module 𝕜₃ G
inst_17 : TopologicalSpace E
inst_18 : TopologicalSpace F
inst_19 : TopologicalSpace G
𝔖 : Set (Set E)
𝔗 : Set (Set F)
inst_20 : IsTopologicalAddGroup F
inst_21 : IsTopologicalAddGroup G
inst_22 : ContinuousConstSMul 𝕜₃ G
inst_23 : ContinuousConstSMul 𝕜₂ F
L : F →SL[τ] G
this : UniformSpace G := IsTopologicalAddGroup.rightUniformSpace G
⊢ IsUniformAddGroup G

Tactic:
haveI : IsUniformAddGroup G := isUniformAddGroup_of_addCommGroup
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁_1 : Type u_1
𝕜₂_1 : Type u_2
inst : NormedField 𝕜₁_1
inst_1 : NormedField 𝕜₂_1
σ_1 : 𝕜₁_1 →+* 𝕜₂_1
E_1 : Type u_3
F_1 : Type u_4
G_1 : Type u_5
inst_2 : AddCommGroup E_1
inst_3 : Module 𝕜₁_1 E_1
inst_4 : TopologicalSpace E_1
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂_1 F_1
𝕜₁ : Type u_6
𝕜₂ : Type u_7
𝕜₃ : Type u_8
inst_7 : NormedField 𝕜₁
inst_8 : NormedField 𝕜₂
inst_9 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_10 : RingHomCompTriple σ τ ρ
E : Type u_9
F : Type u_10
G : Type u_11
inst_11 : AddCommGroup E
inst_12 : Module 𝕜₁ E
inst_13 : AddCommGroup F
inst_14 : Module 𝕜₂ F
inst_15 : AddCommGroup G
inst_16 : Module 𝕜₃ G
inst_17 : TopologicalSpace E
inst_18 : TopologicalSpace F
inst_19 : TopologicalSpace G
𝔖 : Set (Set E)
𝔗 : Set (Set F)
inst_20 : IsTopologicalAddGroup F
inst_21 : IsTopologicalAddGroup G
inst_22 : ContinuousConstSMul 𝕜₃ G
inst_23 : ContinuousConstSMul 𝕜₂ F
L : F →SL[τ] G
this_1 : UniformSpace G := IsTopologicalAddGroup.rightUniformSpace G
this_2 : IsUniformAddGroup G
this : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
⊢ IsUniformAddGroup F

Tactic:
haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁_1 : Type u_1
𝕜₂_1 : Type u_2
inst : NormedField 𝕜₁_1
inst_1 : NormedField 𝕜₂_1
σ_1 : 𝕜₁_1 →+* 𝕜₂_1
E_1 : Type u_3
F_1 : Type u_4
G_1 : Type u_5
inst_2 : AddCommGroup E_1
inst_3 : Module 𝕜₁_1 E_1
inst_4 : TopologicalSpace E_1
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂_1 F_1
𝕜₁ : Type u_6
𝕜₂ : Type u_7
𝕜₃ : Type u_8
inst_7 : NormedField 𝕜₁
inst_8 : NormedField 𝕜₂
inst_9 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_10 : RingHomCompTriple σ τ ρ
E : Type u_9
F : Type u_10
G : Type u_11
inst_11 : AddCommGroup E
inst_12 : Module 𝕜₁ E
inst_13 : AddCommGroup F
inst_14 : Module 𝕜₂ F
inst_15 : AddCommGroup G
inst_16 : Module 𝕜₃ G
inst_17 : TopologicalSpace E
inst_18 : TopologicalSpace F
inst_19 : TopologicalSpace G
𝔖 : Set (Set E)
𝔗 : Set (Set F)
inst_20 : IsTopologicalAddGroup F
inst_21 : IsTopologicalAddGroup G
inst_22 : ContinuousConstSMul 𝕜₃ G
inst_23 : ContinuousConstSMul 𝕜₂ F
L : F →SL[τ] G
this_1 : UniformSpace G := IsTopologicalAddGroup.rightUniformSpace G
this_2 : IsUniformAddGroup G
this_3 : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
rw :
  Continuous[UniformConvergenceCLM.instTopologicalSpace σ F 𝔖, UniformOnFun.topologicalSpace E G 𝔖]
    (Function.comp (β := UniformConvergenceCLM ρ G 𝔖)
      (Function.comp (β := E → G) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → G) → E →ᵤ[𝔖] G)
        (DFunLike.coe (β := fun (a : E) ↦ G)))
      fun (f : UniformConvergenceCLM σ F 𝔖) ↦ L ∘SL f)
⊢ Continuous[UniformConvergenceCLM.instTopologicalSpace σ F 𝔖, UniformConvergenceCLM.instTopologicalSpace ρ G 𝔖]
    fun (f : UniformConvergenceCLM σ F 𝔖) ↦ L ∘SL f

Tactic:
rw [(UniformConvergenceCLM.isEmbedding_coeFn _ _ _).continuous_iff]

Premises used: UniformConvergenceCLM.isEmbedding_coeFn, Topology.IsEmbedding.continuous_iff
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁_1 : Type u_1
𝕜₂_1 : Type u_2
inst : NormedField 𝕜₁_1
inst_1 : NormedField 𝕜₂_1
σ_1 : 𝕜₁_1 →+* 𝕜₂_1
E_1 : Type u_3
F_1 : Type u_4
G_1 : Type u_5
inst_2 : AddCommGroup E_1
inst_3 : Module 𝕜₁_1 E_1
inst_4 : TopologicalSpace E_1
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂_1 F_1
𝕜₁ : Type u_6
𝕜₂ : Type u_7
𝕜₃ : Type u_8
inst_7 : NormedField 𝕜₁
inst_8 : NormedField 𝕜₂
inst_9 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_10 : RingHomCompTriple σ τ ρ
E : Type u_9
F : Type u_10
G : Type u_11
inst_11 : AddCommGroup E
inst_12 : Module 𝕜₁ E
inst_13 : AddCommGroup F
inst_14 : Module 𝕜₂ F
inst_15 : AddCommGroup G
inst_16 : Module 𝕜₃ G
inst_17 : TopologicalSpace E
inst_18 : TopologicalSpace F
inst_19 : TopologicalSpace G
𝔖 : Set (Set E)
𝔗 : Set (Set F)
inst_20 : IsTopologicalAddGroup F
inst_21 : IsTopologicalAddGroup G
inst_22 : ContinuousConstSMul 𝕜₃ G
inst_23 : ContinuousConstSMul 𝕜₂ F
L : F →SL[τ] G
this_1 : UniformSpace G := IsTopologicalAddGroup.rightUniformSpace G
this_2 : IsUniformAddGroup G
this_3 : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ Continuous[UniformConvergenceCLM.instTopologicalSpace σ F 𝔖, UniformOnFun.topologicalSpace E G 𝔖]
    (Function.comp (β := UniformConvergenceCLM ρ G 𝔖)
      (Function.comp (β := E → G) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → G) → E →ᵤ[𝔖] G)
        (DFunLike.coe (β := fun (a : E) ↦ G)))
      fun (f : UniformConvergenceCLM σ F 𝔖) ↦ L ∘SL f)

Tactic:
(UniformOnFun.postcomp_uniformContinuous L.uniformContinuous).continuous.comp
        (UniformConvergenceCLM.isEmbedding_coeFn _ _ _).continuous

Premises used: UniformConvergenceCLM.isEmbedding_coeFn, Continuous.comp, UniformOnFun.postcomp_uniformContinuous, ContinuousLinearMap.uniformContinuous, UniformContinuous.continuous, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁_1 : Type u_1
𝕜₂_1 : Type u_2
inst : NormedField 𝕜₁_1
inst_1 : NormedField 𝕜₂_1
σ_1 : 𝕜₁_1 →+* 𝕜₂_1
E_1 : Type u_3
F_1 : Type u_4
G_1 : Type u_5
inst_2 : AddCommGroup E_1
inst_3 : Module 𝕜₁_1 E_1
inst_4 : TopologicalSpace E_1
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂_1 F_1
𝕜₁ : Type u_6
𝕜₂ : Type u_7
𝕜₃ : Type u_8
inst_7 : NormedField 𝕜₁
inst_8 : NormedField 𝕜₂
inst_9 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_10 : RingHomCompTriple σ τ ρ
E : Type u_9
F : Type u_10
G : Type u_11
inst_11 : AddCommGroup E
inst_12 : Module 𝕜₁ E
inst_13 : AddCommGroup F
inst_14 : Module 𝕜₂ F
inst_15 : AddCommGroup G
inst_16 : Module 𝕜₃ G
inst_17 : TopologicalSpace E
inst_18 : TopologicalSpace F
inst_19 : TopologicalSpace G
𝔖 : Set (Set E)
𝔗 : Set (Set F)
inst_20 : IsTopologicalAddGroup F
inst_21 : IsTopologicalAddGroup G
inst_22 : ContinuousConstSMul 𝕜₃ G
inst_23 : ContinuousConstSMul 𝕜₂ F
L : F →SL[τ] G
this_1 : UniformSpace G := IsTopologicalAddGroup.rightUniformSpace G
this_2 : IsUniformAddGroup G
this_3 : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ Continuous[UniformConvergenceCLM.instTopologicalSpace σ F 𝔖, UniformOnFun.topologicalSpace E G 𝔖]
    (Function.comp (β := UniformConvergenceCLM ρ G 𝔖)
      (Function.comp (β := E → G) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → G) → E →ᵤ[𝔖] G)
        (DFunLike.coe (β := fun (a : E) ↦ G)))
      fun (f : UniformConvergenceCLM σ F 𝔖) ↦ L ∘SL f)

Tactic:
exact
      (UniformOnFun.postcomp_uniformContinuous L.uniformContinuous).continuous.comp
        (UniformConvergenceCLM.isEmbedding_coeFn _ _ _).continuous

Premises used: UniformConvergenceCLM.isEmbedding_coeFn, Continuous.comp, UniformOnFun.postcomp_uniformContinuous, ContinuousLinearMap.uniformContinuous, 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_1 : Type u_3
F_1 : Type u_4
G : Type u_5
inst_2 : AddCommGroup E_1
inst_3 : Module 𝕜₁ E_1
inst_4 : TopologicalSpace E_1
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂ F_1
𝕜 : Type u_6
inst_7 : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst_8 : AddCommGroup E
inst_9 : Module 𝕜 E
inst_10 : TopologicalSpace E
inst_11 : (i : ι) → AddCommGroup (F i)
inst_12 : (i : ι) → Module.{u_6, u_9} 𝕜 (F i)
inst_13 : (i : ι) → TopologicalSpace (F i)
inst_14 : ∀ (i : ι), IsTopologicalAddGroup.{u_9} (F i)
inst_15 : ∀ (i : ι), ContinuousConstSMul.{u_6, u_9} 𝕜 (F i)
𝔖 : Set (Set E)
this_1 : (i : ι) → UniformSpace (F i) := fun (i : ι) ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup.{u_9} (F i)
x x_1 : (i : ι) → UniformConvergenceCLM.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) (F i) 𝔖
h :
  ∀ (x_2 : E) (x_3 : ι),
    Eq.{u_9 + 1} (α := F x_3) ((ContinuousLinearMap.pi (φ := F) (x + x_1) : (a : E) → (i : ι) → F i) x_2 x_3 : F x_3)
      ((ContinuousLinearMap.pi (φ := F) x + ContinuousLinearMap.pi (φ := F) x_1 : (a : E) → (i : ι) → F i) x_2 x_3 :
        F x_3)
⊢ ContinuousLinearMap.pi (φ := F) (x + x_1) = ContinuousLinearMap.pi (φ := F) x + ContinuousLinearMap.pi (φ := F) x_1

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E_1 : Type u_3
F_1 : Type u_4
G : Type u_5
inst_2 : AddCommGroup E_1
inst_3 : Module 𝕜₁ E_1
inst_4 : TopologicalSpace E_1
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂ F_1
𝕜 : Type u_6
inst_7 : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst_8 : AddCommGroup E
inst_9 : Module 𝕜 E
inst_10 : TopologicalSpace E
inst_11 : (i : ι) → AddCommGroup (F i)
inst_12 : (i : ι) → Module.{u_6, u_9} 𝕜 (F i)
inst_13 : (i : ι) → TopologicalSpace (F i)
inst_14 : ∀ (i : ι), IsTopologicalAddGroup.{u_9} (F i)
inst_15 : ∀ (i : ι), ContinuousConstSMul.{u_6, u_9} 𝕜 (F i)
𝔖 : Set (Set E)
this_1 : (i : ι) → UniformSpace (F i) := fun (i : ι) ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup.{u_9} (F i)
x x_1 : (i : ι) → UniformConvergenceCLM.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) (F i) 𝔖
x_2 : E
x_3 : ι
⊢ Eq.{u_9 + 1} (α := F x_3) ((ContinuousLinearMap.pi (φ := F) (x + x_1) : (a : E) → (i : ι) → F i) x_2 x_3 : F x_3)
    ((ContinuousLinearMap.pi (φ := F) x + ContinuousLinearMap.pi (φ := F) x_1 : (a : E) → (i : ι) → F i) x_2 x_3 :
      F x_3)

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E_1 : Type u_3
F_1 : Type u_4
G : Type u_5
inst_2 : AddCommGroup E_1
inst_3 : Module 𝕜₁ E_1
inst_4 : TopologicalSpace E_1
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂ F_1
𝕜 : Type u_6
inst_7 : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst_8 : AddCommGroup E
inst_9 : Module 𝕜 E
inst_10 : TopologicalSpace E
inst_11 : (i : ι) → AddCommGroup (F i)
inst_12 : (i : ι) → Module.{u_6, u_9} 𝕜 (F i)
inst_13 : (i : ι) → TopologicalSpace (F i)
inst_14 : ∀ (i : ι), IsTopologicalAddGroup.{u_9} (F i)
inst_15 : ∀ (i : ι), ContinuousConstSMul.{u_6, u_9} 𝕜 (F i)
𝔖 : Set (Set E)
this_1 : (i : ι) → UniformSpace (F i) := fun (i : ι) ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup.{u_9} (F i)
x : 𝕜
x_1 : (i : ι) → UniformConvergenceCLM.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) (F i) 𝔖
h :
  ∀ (x_2 : E) (x_3 : ι),
    Eq.{u_9 + 1} (α := F x_3) ((ContinuousLinearMap.pi (φ := F) (x • x_1) : (a : E) → (i : ι) → F i) x_2 x_3 : F x_3)
      ((HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) (ContinuousLinearMap.pi (φ := F) x_1) :
            (a : E) → (i : ι) → F i)
          x_2 x_3 :
        F x_3)
⊢ ContinuousLinearMap.pi (φ := F) (x • x_1) =
    HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) (ContinuousLinearMap.pi (φ := F) x_1)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Goal:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E_1 : Type u_3
F_1 : Type u_4
G : Type u_5
inst_2 : AddCommGroup E_1
inst_3 : Module 𝕜₁ E_1
inst_4 : TopologicalSpace E_1
inst_5 : AddCommGroup F_1
inst_6 : Module 𝕜₂ F_1
𝕜 : Type u_6
inst_7 : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst_8 : AddCommGroup E
inst_9 : Module 𝕜 E
inst_10 : TopologicalSpace E
inst_11 : (i : ι) → AddCommGroup (F i)
inst_12 : (i : ι) → Module.{u_6, u_9} 𝕜 (F i)
inst_13 : (i : ι) → TopologicalSpace (F i)
inst_14 : ∀ (i : ι), IsTopologicalAddGroup.{u_9} (F i)
inst_15 : ∀ (i : ι), ContinuousConstSMul.{u_6, u_9} 𝕜 (F i)
𝔖 : Set (Set E)
this_1 : (i : ι) → UniformSpace (F i) := fun (i : ι) ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup.{u_9} (F i)
x : 𝕜
x_1 : (i : ι) → UniformConvergenceCLM.{u_6, u_6, u_7, u_9} (RingHom.id 𝕜) (F i) 𝔖
x_2 : E
x_3 : ι
⊢ Eq.{u_9 + 1} (α := F x_3) ((ContinuousLinearMap.pi (φ := F) (x • x_1) : (a : E) → (i : ι) → F i) x_2 x_3 : F x_3)
    ((HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) (ContinuousLinearMap.pi (φ := F) x_1) :
          (a : E) → (i : ι) → F i)
        x_2 x_3 :
      F x_3)

Tactic:
rfl