awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst : AddCommGroup E
inst_1 : AddCommGroup F
inst_2 : AddCommGroup G
inst_3 : AddCommGroup H
inst_4 : NormedField 𝕜
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜 F
inst_7 : Module 𝕜 G
inst_8 : Module 𝕜 H
inst_9 : TopologicalSpace E
inst_10 : TopologicalSpace F
inst_11 : TopologicalSpace G
inst_12 : TopologicalSpace H
inst_13 : IsTopologicalAddGroup G
inst_14 : IsTopologicalAddGroup H
inst_15 : ContinuousConstSMul 𝕜 G
inst_16 : ContinuousConstSMul 𝕜 H
e : G ≃L[𝕜] H
x x_1 : G →L[𝕜] G
h :
  ∀ (x_2 : H),
    Eq (α := H)
      ((AddHom.toFun
              (LinearMap.toAddHom
                  ((↑(↑(e.arrowCongr e) : (G →L[𝕜] G) ≃ₗ[𝕜] H →L[𝕜] H) :
                      LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (G →L[𝕜] G) (H →L[𝕜] H)) :
                    LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (G →L[𝕜] G) (H →L[𝕜] H)) :
                AddHom.{u_4, u_5} (G →L[𝕜] G) (H →L[𝕜] H))
              (x * x_1) :
            (a : H) → H)
          x_2 :
        H)
      ((AddHom.toFun
                (LinearMap.toAddHom
                    ((↑(↑(e.arrowCongr e) : (G →L[𝕜] G) ≃ₗ[𝕜] H →L[𝕜] H) :
                        LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (G →L[𝕜] G) (H →L[𝕜] H)) :
                      LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (G →L[𝕜] G) (H →L[𝕜] H)) :
                  AddHom.{u_4, u_5} (G →L[𝕜] G) (H →L[𝕜] H))
                x *
              AddHom.toFun
                (LinearMap.toAddHom
                    ((↑(↑(e.arrowCongr e) : (G →L[𝕜] G) ≃ₗ[𝕜] H →L[𝕜] H) :
                        LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (G →L[𝕜] G) (H →L[𝕜] H)) :
                      LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (G →L[𝕜] G) (H →L[𝕜] H)) :
                  AddHom.{u_4, u_5} (G →L[𝕜] G) (H →L[𝕜] H))
                x_1 :
            (a : H) → H)
          x_2 :
        H)
⊢ AddHom.toFun
      (LinearMap.toAddHom
          ((↑(↑(e.arrowCongr e) : (G →L[𝕜] G) ≃ₗ[𝕜] H →L[𝕜] H) :
              LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (G →L[𝕜] G) (H →L[𝕜] H)) :
            LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (G →L[𝕜] G) (H →L[𝕜] H)) :
        AddHom.{u_4, u_5} (G →L[𝕜] G) (H →L[𝕜] H))
      (x * x_1) =
    AddHom.toFun
        (LinearMap.toAddHom
            ((↑(↑(e.arrowCongr e) : (G →L[𝕜] G) ≃ₗ[𝕜] H →L[𝕜] H) :
                LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (G →L[𝕜] G) (H →L[𝕜] H)) :
              LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (G →L[𝕜] G) (H →L[𝕜] H)) :
          AddHom.{u_4, u_5} (G →L[𝕜] G) (H →L[𝕜] H))
        x *
      AddHom.toFun
        (LinearMap.toAddHom
            ((↑(↑(e.arrowCongr e) : (G →L[𝕜] G) ≃ₗ[𝕜] H →L[𝕜] H) :
                LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (G →L[𝕜] G) (H →L[𝕜] H)) :
              LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (G →L[𝕜] G) (H →L[𝕜] H)) :
          AddHom.{u_4, u_5} (G →L[𝕜] G) (H →L[𝕜] H))
        x_1

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst : AddCommGroup E
inst_1 : AddCommGroup F
inst_2 : AddCommGroup G
inst_3 : AddCommGroup H
inst_4 : NormedField 𝕜
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜 F
inst_7 : Module 𝕜 G
inst_8 : Module 𝕜 H
inst_9 : TopologicalSpace E
inst_10 : TopologicalSpace F
inst_11 : TopologicalSpace G
inst_12 : TopologicalSpace H
inst_13 : IsTopologicalAddGroup G
inst_14 : IsTopologicalAddGroup H
inst_15 : ContinuousConstSMul 𝕜 G
inst_16 : ContinuousConstSMul 𝕜 H
e : G ≃L[𝕜] H
x x_1 : G →L[𝕜] G
x_2 : H
⊢ Eq (α := H)
    ((AddHom.toFun
            (LinearMap.toAddHom
                ((↑(↑(e.arrowCongr e) : (G →L[𝕜] G) ≃ₗ[𝕜] H →L[𝕜] H) :
                    LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (G →L[𝕜] G) (H →L[𝕜] H)) :
                  LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (G →L[𝕜] G) (H →L[𝕜] H)) :
              AddHom.{u_4, u_5} (G →L[𝕜] G) (H →L[𝕜] H))
            (x * x_1) :
          (a : H) → H)
        x_2 :
      H)
    ((AddHom.toFun
              (LinearMap.toAddHom
                  ((↑(↑(e.arrowCongr e) : (G →L[𝕜] G) ≃ₗ[𝕜] H →L[𝕜] H) :
                      LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (G →L[𝕜] G) (H →L[𝕜] H)) :
                    LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (G →L[𝕜] G) (H →L[𝕜] H)) :
                AddHom.{u_4, u_5} (G →L[𝕜] G) (H →L[𝕜] H))
              x *
            AddHom.toFun
              (LinearMap.toAddHom
                  ((↑(↑(e.arrowCongr e) : (G →L[𝕜] G) ≃ₗ[𝕜] H →L[𝕜] H) :
                      LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (G →L[𝕜] G) (H →L[𝕜] H)) :
                    LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (G →L[𝕜] G) (H →L[𝕜] H)) :
                AddHom.{u_4, u_5} (G →L[𝕜] G) (H →L[𝕜] H))
              x_1 :
          (a : H) → H)
        x_2 :
      H)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst : AddCommGroup E
inst_1 : AddCommGroup F
inst_2 : AddCommGroup G
inst_3 : AddCommGroup H
inst_4 : NormedField 𝕜
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜 F
inst_7 : Module 𝕜 G
inst_8 : Module 𝕜 H
inst_9 : TopologicalSpace E
inst_10 : TopologicalSpace F
inst_11 : TopologicalSpace G
inst_12 : TopologicalSpace H
inst_13 : IsTopologicalAddGroup G
inst_14 : IsTopologicalAddGroup H
inst_15 : ContinuousConstSMul 𝕜 G
inst_16 : ContinuousConstSMul 𝕜 H
e : G ≃L[𝕜] H
x : 𝕜
h :
  ∀ (x_1 : H),
    Eq (α := H)
      ((AddHom.toFun
              (LinearMap.toAddHom
                  ((↑(↑(e.arrowCongr e) : (G →L[𝕜] G) ≃ₗ[𝕜] H →L[𝕜] H) :
                      LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (G →L[𝕜] G) (H →L[𝕜] H)) :
                    LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (G →L[𝕜] G) (H →L[𝕜] H)) :
                AddHom.{u_4, u_5} (G →L[𝕜] G) (H →L[𝕜] H))
              ((algebraMap 𝕜 (G →L[𝕜] G) : (a : 𝕜) → G →L[𝕜] G) x) :
            (a : H) → H)
          x_1 :
        H)
      ((((algebraMap 𝕜 (H →L[𝕜] H) : (a : 𝕜) → H →L[𝕜] H) x : H →L[𝕜] H) : (a : H) → H) x_1 : H)
⊢ AddHom.toFun
      (LinearMap.toAddHom
          ((↑(↑(e.arrowCongr e) : (G →L[𝕜] G) ≃ₗ[𝕜] H →L[𝕜] H) :
              LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (G →L[𝕜] G) (H →L[𝕜] H)) :
            LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (G →L[𝕜] G) (H →L[𝕜] H)) :
        AddHom.{u_4, u_5} (G →L[𝕜] G) (H →L[𝕜] H))
      ((algebraMap 𝕜 (G →L[𝕜] G) : (a : 𝕜) → G →L[𝕜] G) x) =
    (algebraMap 𝕜 (H →L[𝕜] H) : (a : 𝕜) → H →L[𝕜] H) x

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst : AddCommGroup E
inst_1 : AddCommGroup F
inst_2 : AddCommGroup G
inst_3 : AddCommGroup H
inst_4 : NormedField 𝕜
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜 F
inst_7 : Module 𝕜 G
inst_8 : Module 𝕜 H
inst_9 : TopologicalSpace E
inst_10 : TopologicalSpace F
inst_11 : TopologicalSpace G
inst_12 : TopologicalSpace H
inst_13 : IsTopologicalAddGroup G
inst_14 : IsTopologicalAddGroup H
inst_15 : ContinuousConstSMul 𝕜 G
inst_16 : ContinuousConstSMul 𝕜 H
e : G ≃L[𝕜] H
x : 𝕜
x_1 : H
⊢ Eq (α := H)
    ((AddHom.toFun
            (LinearMap.toAddHom
                ((↑(↑(e.arrowCongr e) : (G →L[𝕜] G) ≃ₗ[𝕜] H →L[𝕜] H) :
                    LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (G →L[𝕜] G) (H →L[𝕜] H)) :
                  LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (G →L[𝕜] G) (H →L[𝕜] H)) :
              AddHom.{u_4, u_5} (G →L[𝕜] G) (H →L[𝕜] H))
            ((algebraMap 𝕜 (G →L[𝕜] G) : (a : 𝕜) → G →L[𝕜] G) x) :
          (a : H) → H)
        x_1 :
      H)
    ((((algebraMap 𝕜 (H →L[𝕜] H) : (a : 𝕜) → H →L[𝕜] H) x : H →L[𝕜] H) : (a : H) → H) x_1 : H)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜 : Type u_1
G : Type u_4
H : Type u_5
inst : AddCommGroup G
inst_1 : AddCommGroup H
inst_2 : NormedField 𝕜
inst_3 : Module 𝕜 G
inst_4 : Module 𝕜 H
inst_5 : TopologicalSpace G
inst_6 : TopologicalSpace H
inst_7 : IsTopologicalAddGroup G
inst_8 : IsTopologicalAddGroup H
inst_9 : ContinuousConstSMul 𝕜 G
inst_10 : ContinuousConstSMul 𝕜 H
e : G ≃L[𝕜] H
f : G →L[𝕜] G
x : H
⊢ Eq (α := H)
    (((((e.conjContinuousAlgEquiv : ContinuousAlgEquiv.{u_1, u_4, u_5} 𝕜 (G →L[𝕜] G) (H →L[𝕜] H)) :
                (a : G →L[𝕜] G) → H →L[𝕜] H)
              f :
            H →L[𝕜] H) :
          (a : H) → H)
        x :
      H)
    ((e : (a : G) → H) ((f : (a : G) → G) ((e.symm : (a : H) → G) x : G) : G) : H)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜 : Type u_1
G : Type u_4
H : Type u_5
inst : AddCommGroup G
inst_1 : AddCommGroup H
inst_2 : NormedField 𝕜
inst_3 : Module 𝕜 G
inst_4 : Module 𝕜 H
inst_5 : TopologicalSpace G
inst_6 : TopologicalSpace H
inst_7 : IsTopologicalAddGroup G
inst_8 : IsTopologicalAddGroup H
inst_9 : ContinuousConstSMul 𝕜 G
inst_10 : ContinuousConstSMul 𝕜 H
e : G ≃L[𝕜] H
f : H →L[𝕜] H
x : G
⊢ Eq (α := G)
    (((((ContinuousAlgEquiv.symm e.conjContinuousAlgEquiv :
                  ContinuousAlgEquiv.{u_1, u_5, u_4} 𝕜 (H →L[𝕜] H) (G →L[𝕜] G)) :
                (a : H →L[𝕜] H) → G →L[𝕜] G)
              f :
            G →L[𝕜] G) :
          (a : G) → G)
        x :
      G)
    ((e.symm : (a : H) → G) ((f : (a : H) → H) ((e : (a : G) → H) x : H) : H) : G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜 : Type u_1
G : Type u_4
H : Type u_5
inst : AddCommGroup G
inst_1 : AddCommGroup H
inst_2 : NormedField 𝕜
inst_3 : Module 𝕜 G
inst_4 : Module 𝕜 H
inst_5 : TopologicalSpace G
inst_6 : TopologicalSpace H
inst_7 : IsTopologicalAddGroup G
inst_8 : IsTopologicalAddGroup H
inst_9 : ContinuousConstSMul 𝕜 G
inst_10 : ContinuousConstSMul 𝕜 H
e : G ≃L[𝕜] H
f : G →L[𝕜] G
⊢ ((e.conjContinuousAlgEquiv : ContinuousAlgEquiv.{u_1, u_4, u_5} 𝕜 (G →L[𝕜] G) (H →L[𝕜] H)) :
        (a : G →L[𝕜] G) → H →L[𝕜] H)
      f =
    (↑e : G →L[𝕜] H) ∘SL f ∘SL (↑e.symm : H →L[𝕜] G)

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜 : Type u_1
G : Type u_4
H : Type u_5
inst : AddCommGroup G
inst_1 : AddCommGroup H
inst_2 : NormedField 𝕜
inst_3 : Module 𝕜 G
inst_4 : Module 𝕜 H
inst_5 : TopologicalSpace G
inst_6 : TopologicalSpace H
inst_7 : IsTopologicalAddGroup G
inst_8 : IsTopologicalAddGroup H
inst_9 : ContinuousConstSMul 𝕜 G
inst_10 : ContinuousConstSMul 𝕜 H
e : G ≃L[𝕜] H
⊢ Eq (α := ContinuousAlgEquiv.{u_1, u_5, u_4} 𝕜 (H →L[𝕜] H) (G →L[𝕜] G))
    (ContinuousAlgEquiv.symm e.conjContinuousAlgEquiv) e.symm.conjContinuousAlgEquiv

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, ContinuousLinearEquiv.symm, LinearEquiv.symm, AlgEquiv.symm, ContinuousAlgEquiv.symm, ContinuousLinearEquiv.conjContinuousAlgEquiv, Equiv.symm, rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜 : Type u_1
G : Type u_4
inst : AddCommGroup G
inst_1 : NormedField 𝕜
inst_2 : Module 𝕜 G
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalAddGroup G
inst_5 : ContinuousConstSMul 𝕜 G
⊢ Eq (α := (G →L[𝕜] G) ≃A[𝕜] G →L[𝕜] G) (conjContinuousAlgEquiv (ContinuousLinearEquiv.refl 𝕜 G))
    (ContinuousAlgEquiv.refl 𝕜 (G →L[𝕜] G))

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, ContinuousAlgEquiv.refl, ContinuousLinearEquiv.conjContinuousAlgEquiv, AlgEquiv.refl, Equiv.refl, rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
G : Type u_4
H : Type u_5
inst : AddCommGroup E
inst_1 : AddCommGroup G
inst_2 : AddCommGroup H
inst_3 : NormedField 𝕜
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 G
inst_6 : Module 𝕜 H
inst_7 : TopologicalSpace E
inst_8 : TopologicalSpace G
inst_9 : TopologicalSpace H
inst_10 : IsTopologicalAddGroup G
inst_11 : IsTopologicalAddGroup H
inst_12 : ContinuousConstSMul 𝕜 G
inst_13 : ContinuousConstSMul 𝕜 H
inst_14 : IsTopologicalAddGroup E
inst_15 : ContinuousConstSMul 𝕜 E
e : E ≃L[𝕜] G
f : G ≃L[𝕜] H
⊢ Eq (α := ContinuousAlgEquiv.{u_1, u_2, u_5} 𝕜 (E →L[𝕜] E) (H →L[𝕜] H)) (conjContinuousAlgEquiv (e.trans f))
    (ContinuousAlgEquiv.trans e.conjContinuousAlgEquiv f.conjContinuousAlgEquiv)

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, ContinuousLinearEquiv.symm, LinearEquiv.symm, Equiv.trans, ContinuousLinearEquiv.trans, ContinuousAlgEquiv.trans, AlgEquiv.trans, ContinuousLinearEquiv.conjContinuousAlgEquiv, LinearEquiv.trans, rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
Goal:
α : Type u_1
ι : Type u_2
inst : TopologicalSpace α
𝕜 : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
𝕜₃ : Type u_6
inst_1 : NormedField 𝕜
inst_2 : NormedField 𝕜₁
inst_3 : NormedField 𝕜₂
inst_4 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_5 : RingHomCompTriple σ τ ρ
E : Type u_7
F : Type u_8
Fᵤ : Type u_9
G : Type u_10
inst_6 : AddCommGroup E
inst_7 : TopologicalSpace E
inst_8 : AddCommGroup F
inst_9 : TopologicalSpace F
inst_10 : IsTopologicalAddGroup F
inst_11 : AddCommGroup G
inst_12 : TopologicalSpace G
inst_13 : IsTopologicalAddGroup G
inst_14 : AddCommGroup Fᵤ
inst_15 : UniformSpace Fᵤ
inst_16 : IsUniformAddGroup Fᵤ
inst_17 : Module 𝕜 E
inst_18 : Module 𝕜 F
inst_19 : Module 𝕜 Fᵤ
inst_20 : Module 𝕜₁ E
inst_21 : Module 𝕜₂ F
inst_22 : Module 𝕜₂ Fᵤ
inst_23 : Module 𝕜₃ G
inst_24 : T2Space F
⊢ T2Space (E →SLₚₜ[σ] F)

Tactic:
UniformConvergenceCLM.t2Space _ _ _ Set.sUnion_finite_eq_univ

Premises used: Set.sUnion_finite_eq_univ, UniformConvergenceCLM.t2Space
-- Module: Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
Goal:
α : Type u_1
ι : Type u_2
inst : TopologicalSpace α
𝕜 : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
𝕜₃ : Type u_6
inst_1 : NormedField 𝕜
inst_2 : NormedField 𝕜₁
inst_3 : NormedField 𝕜₂
inst_4 : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst_5 : RingHomCompTriple σ τ ρ
E : Type u_7
F : Type u_8
Fᵤ : Type u_9
G : Type u_10
inst_6 : AddCommGroup E
inst_7 : TopologicalSpace E
inst_8 : AddCommGroup F
inst_9 : TopologicalSpace F
inst_10 : IsTopologicalAddGroup F
inst_11 : AddCommGroup G
inst_12 : TopologicalSpace G
inst_13 : IsTopologicalAddGroup G
inst_14 : AddCommGroup Fᵤ
inst_15 : UniformSpace Fᵤ
inst_16 : IsUniformAddGroup Fᵤ
inst_17 : Module 𝕜 E
inst_18 : Module 𝕜 F
inst_19 : Module 𝕜 Fᵤ
inst_20 : Module 𝕜₁ E
inst_21 : Module 𝕜₂ F
inst_22 : Module 𝕜₂ Fᵤ
inst_23 : Module 𝕜₃ G
⊢ ContinuousEvalConst (E →SLₚₜ[σ] F) E F

Tactic:
UniformConvergenceCLM.continuousEvalConst _ _ _ Set.sUnion_finite_eq_univ

Premises used: Set.sUnion_finite_eq_univ, UniformConvergenceCLM.continuousEvalConst
-- Module: Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
Goal:
𝕜₁ : Type u_4
𝕜₂ : Type u_5
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_7
F : Type u_8
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup F
inst_5 : TopologicalSpace F
inst_6 : IsTopologicalAddGroup F
inst_7 : Module 𝕜₁ E
inst_8 : Module 𝕜₂ F
ι : Type u_11
p : ι → Prop
b : ι → Set F
h : Filter.HasBasis (𝓝 0) p b
⊢ Filter.HasBasis (α := E →SLₚₜ[σ] F) (𝓝 0)
    (fun (Si : Prod.{u_7, u_11} (Set E) ι) ↦ Finite.{u_7 + 1} (↑Si.1 : Type u_7) ∧ p Si.2)
    fun (Si : Prod.{u_7, u_11} (Set E) ι) ↦
    {f : E →SLₚₜ[σ] F | ∀ x ∈ Si.1, Membership.mem (α := F) (b Si.2) ((f : (a : E) → F) x : F)}

Tactic:
UniformConvergenceCLM.hasBasis_nhds_zero_of_basis σ F { S | Finite S }
    ⟨∅, Set.finite_empty⟩ (directedOn_of_sup_mem fun _ _ => Set.Finite.union) h

Premises used: Set.Finite.union, Set.finite_empty, Set.Mem, Finite, setOf, Set.Elem, directedOn_of_sup_mem, UniformConvergenceCLM.hasBasis_nhds_zero_of_basis, Exists.intro, EmptyCollection.emptyCollection
-- Module: Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
Goal:
𝕜₁ : Type u_4
𝕜₂ : Type u_5
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_7
F : Type u_8
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup F
inst_5 : TopologicalSpace F
inst_6 : IsTopologicalAddGroup F
inst_7 : Module 𝕜₁ E
inst_8 : Module 𝕜₂ F
⊢ Filter.HasBasis (α := E →SLₚₜ[σ] F) (𝓝 0)
    (fun (SV : Prod.{u_7, u_8} (Set E) (Set F)) ↦
      Finite.{u_7 + 1} (↑SV.1 : Type u_7) ∧ Membership.mem (γ := Filter F) (𝓝 0) SV.2)
    fun (SV : Prod.{u_7, u_8} (Set E) (Set F)) ↦
    {f : E →SLₚₜ[σ] F | ∀ x ∈ SV.1, Membership.mem (α := F) SV.2 ((f : (a : E) → F) x : F)}

Tactic:
PointwiseConvergenceCLM.hasBasis_nhds_zero_of_basis (𝓝 0).basis_sets

Premises used: Set.Mem, setOf, nhds, Filter.basis_sets, OfNat.ofNat, PointwiseConvergenceCLM.hasBasis_nhds_zero_of_basis
-- Module: Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
Goal:
𝕜₁ : Type u_4
𝕜₂ : Type u_5
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_7
Fᵤ : Type u_9
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup Fᵤ
inst_5 : UniformSpace Fᵤ
inst_6 : IsUniformAddGroup Fᵤ
inst_7 : Module 𝕜₁ E
inst_8 : Module 𝕜₂ Fᵤ
⊢ IsUniformEmbedding (α := E →SLₚₜ[σ] Fᵤ) (β := (a : E) → Fᵤ) (DFunLike.coe (β := fun (x : E) ↦ Fᵤ))

Tactic:
(UniformOnFun.isUniformEmbedding_toFun_finite E Fᵤ).comp
    (UniformConvergenceCLM.isUniformEmbedding_coeFn σ Fᵤ _)

Premises used: IsUniformEmbedding.comp, UniformOnFun.isUniformEmbedding_toFun_finite, UniformConvergenceCLM.isUniformEmbedding_coeFn
-- Module: Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
Goal:
𝕜₁ : Type u_4
𝕜₂ : Type u_5
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_7
F : Type u_8
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup F
inst_5 : TopologicalSpace F
inst_6 : IsTopologicalAddGroup F
inst_7 : Module 𝕜₁ E
inst_8 : Module 𝕜₂ F
⊢ IsEmbedding (X := E →SLₚₜ[σ] F) (Y := (a : E) → F) (DFunLike.coe (β := fun (x : E) ↦ F))

Tactic:
let _ : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
  have _ : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
  PointwiseConvergenceCLM.isUniformEmbedding_coeFn σ E F |>.isEmbedding

Premises used: isUniformAddGroup_of_addCommGroup, IsUniformEmbedding.isEmbedding, PointwiseConvergenceCLM.isUniformEmbedding_coeFn, IsTopologicalAddGroup.rightUniformSpace
-- Module: Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
Goal:
ι : Type u_2
𝕜₁ : Type u_4
𝕜₂ : Type u_5
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_7
F : Type u_8
inst_2 : AddCommGroup E
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup F
inst_5 : TopologicalSpace F
inst_6 : IsTopologicalAddGroup F
inst_7 : Module 𝕜₁ E
inst_8 : Module 𝕜₂ F
p : Filter ι
a : ι → E →SLₚₜ[σ] F
a₀ : E →SLₚₜ[σ] F
⊢ Filter.Tendsto a p (𝓝 a₀) ↔
    ∀ (x : E),
      Filter.Tendsto.{u_2, u_8} (β := F) (fun (x_1 : ι) ↦ ((a x_1 : (a : E) → F) x : F)) p
        (𝓝 ((a₀ : (a : E) → F) x) : Filter F)

Tactic:
simp [(PointwiseConvergenceCLM.isEmbedding_coeFn σ E F).tendsto_nhds_iff, tendsto_pi_nhds]

Premises used: PointwiseConvergenceCLM.isEmbedding_coeFn, tendsto_pi_nhds, Topology.IsEmbedding.tendsto_nhds_iff
-- Module: Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
Goal:
α : Type u_1
inst : TopologicalSpace α
𝕜₁ : Type u_4
𝕜₂ : Type u_5
inst_1 : NormedField 𝕜₁
inst_2 : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_7
F : Type u_8
inst_3 : AddCommGroup E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup F
inst_8 : Module 𝕜₁ E
inst_9 : Module 𝕜₂ F
g : α → E →SLₚₜ[σ] F
h : ∀ (x : E), Continuous[inst, inst_6] fun (x_1 : α) ↦ (g x_1 : (a : E) → F) x
⊢ Continuous[inst, UniformConvergenceCLM.instTopologicalSpace σ F {s : Set E | Finite (↑s : Type u_7)}] g

Tactic:
simp [(PointwiseConvergenceCLM.isEmbedding_coeFn σ E F).continuous_iff, continuous_pi_iff, h]

Premises used: PointwiseConvergenceCLM.isEmbedding_coeFn, continuous_pi_iff, Topology.IsEmbedding.continuous_iff
-- Module: Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
Goal:
𝕜 : Type u_3
inst : NormedField 𝕜
E : Type u_7
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
ι : Type u_11
F : ι → Type u_12
inst_4 : (i : ι) → AddCommGroup (F i)
inst_5 : (i : ι) → Module.{u_3, u_12} 𝕜 (F i)
inst_6 : (i : ι) → TopologicalSpace (F i)
inst_7 : ∀ (i : ι), IsTopologicalAddGroup.{u_12} (F i)
inst_8 : ∀ (i : ι), ContinuousConstSMul.{u_3, u_12} 𝕜 (F i)
T : (i : ι) → PointwiseConvergenceCLM.{u_3, u_3, u_7, u_12} (RingHom.id 𝕜) E (F i)
e : E
i : ι
⊢ Eq.{u_12 + 1} (α := F i)
    ((((piEquivL 𝕜 E F : (a : (i : ι) → E →Lₚₜ[𝕜] F i) → E →Lₚₜ[𝕜] (i : ι) → F i) T : E →Lₚₜ[𝕜] (i : ι) → F i) :
          (a : E) → (i : ι) → F i)
        e i :
      F i)
    ((T i : (a : E) → F i) e : F i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
Goal:
𝕜 : Type u_3
inst : NormedField 𝕜
E : Type u_7
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
ι : Type u_11
F : ι → Type u_12
inst_4 : (i : ι) → AddCommGroup (F i)
inst_5 : (i : ι) → Module.{u_3, u_12} 𝕜 (F i)
inst_6 : (i : ι) → TopologicalSpace (F i)
inst_7 : ∀ (i : ι), IsTopologicalAddGroup.{u_12} (F i)
inst_8 : ∀ (i : ι), ContinuousConstSMul.{u_3, u_12} 𝕜 (F i)
T : E →Lₚₜ[𝕜] (i : ι) → F i
e : E
i : ι
⊢ Eq.{u_12 + 1} (α := F i)
    ((((ContinuousLinearEquiv.symm (piEquivL 𝕜 E F) : (a : E →Lₚₜ[𝕜] (i : ι) → F i) → (i : ι) → E →Lₚₜ[𝕜] F i) T i :
            PointwiseConvergenceCLM.{u_3, u_3, u_7, u_12} (RingHom.id 𝕜) E (F i)) :
          (a : E) → F i)
        e :
      F i)
    ((T : (a : E) → (i : ι) → F i) e i : F i)

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
𝔖 : Set (Set E)
f g : UniformConvergenceCLM σ F 𝔖
h : ∀ (x : E), Eq.{u_4 + 1} (α := F) ((f : (a : E) → F) x : F) ((g : (a : E) → F) x : F)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- 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
𝔖 : Set (Set E)
⊢ ContinuousSemilinearMapClass (UniformConvergenceCLM σ F 𝔖) σ E F

Tactic:
inferInstanceAs <| ContinuousSemilinearMapClass (E →SL[σ] F) σ E F

Premises used: _private.0.UniformConvergenceCLM.instContinuousSemilinearMapClass._proof_1
-- 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)
e_t : IsTopologicalAddGroup.rightUniformSpace F = inst_7
⊢ Eq (α := TopologicalSpace (UniformConvergenceCLM σ F 𝔖))
    (TopologicalSpace.induced (DFunLike.coe (β := fun (a : E) ↦ F)) (UniformOnFun.topologicalSpace E F 𝔖))
    (TopologicalSpace.induced
      (comp (β := E → F) (⇑(UniformOnFun.ofFun 𝔖) : (a : E → F) → E →ᵤ[𝔖] F) (DFunLike.coe (β := fun (a : E) ↦ F)))
      (UniformOnFun.topologicalSpace E F 𝔖))

Tactic:
congr
-- 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:
IsUniformAddGroup.rightUniformSpace_eq

Premises used: IsUniformAddGroup.rightUniformSpace_eq