awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap (goal)
Goal:
R : Type u_1
𝕜₂ : Type u_3
𝕜₃ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Semiring R
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
inst_3 : AddCommGroup E
inst_4 : Module R E
inst_5 : TopologicalSpace E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜₂ F
inst_8 : TopologicalSpace F
inst_9 : AddCommGroup G
inst_10 : Module 𝕜₃ G
inst_11 : TopologicalSpace G
inst_12 : IsTopologicalAddGroup G
inst_13 : ContinuousConstSMul 𝕜₃ G
σ₁₃ : R →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
x x' : E
y : F
rw :
  (HSub.hSub (α := F →SL[σ₂₃] G) (β := F →SL[σ₂₃] G) ((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G)
          ((f : (a : E) → F →SL[σ₂₃] G) x' : F →SL[σ₂₃] G) :
        (a : F) → G)
      y =
    HSub.hSub (α := G) (β := G) ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
      ((((f : (a : E) → F →SL[σ₂₃] G) x' : F →SL[σ₂₃] G) : (a : F) → G) y : G)
⊢ (((f : (a : E) → F →SL[σ₂₃] G) (x - x') : F →SL[σ₂₃] G) : (a : F) → G) y =
    HSub.hSub (α := G) (β := G) ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
      ((((f : (a : E) → F →SL[σ₂₃] G) x' : F →SL[σ₂₃] G) : (a : F) → G) y : G)
have rw₁ : HSub.hSub (α := G) (β := G) ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
    ((((f : (a : E) → F →SL[σ₂₃] G) x' : F →SL[σ₂₃] G) : (a : F) → G) y : G) =
  HSub.hSub (α := G) (β := G) ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
    ((((f : (a : E) → F →SL[σ₂₃] G) x' : F →SL[σ₂₃] G) : (a : F) → G) y : G)
Tactic: rw [map_sub, sub_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap (goal)
Goal:
R : Type u_1
𝕜₂ : Type u_3
𝕜₃ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Semiring R
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
inst_3 : AddCommGroup E
inst_4 : Module R E
inst_5 : TopologicalSpace E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜₂ F
inst_8 : TopologicalSpace F
inst_9 : AddCommGroup G
inst_10 : Module 𝕜₃ G
inst_11 : TopologicalSpace G
inst_12 : IsTopologicalAddGroup G
inst_13 : ContinuousConstSMul 𝕜₃ G
σ₁₃ : R →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
x : E
y : F
⊢ Eq.{u_7 + 1} (α := G) ((((f : (a : E) → F →SL[σ₂₃] G) (-x) : F →SL[σ₂₃] G) : (a : F) → G) y : G)
    (-(((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
have rw : Eq.{u_7 + 1} (α := G) (((-(f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
  (-(((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
Tactic: rw [map_neg, neg_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap (goal)
Goal:
R : Type u_1
𝕜₂ : Type u_3
𝕜₃ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Semiring R
inst_1 : NormedField 𝕜₂
inst_2 : NormedField 𝕜₃
inst_3 : AddCommGroup E
inst_4 : Module R E
inst_5 : TopologicalSpace E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜₂ F
inst_8 : TopologicalSpace F
inst_9 : AddCommGroup G
inst_10 : Module 𝕜₃ G
inst_11 : TopologicalSpace G
inst_12 : IsTopologicalAddGroup G
inst_13 : ContinuousConstSMul 𝕜₃ G
σ₁₃ : R →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
x : E
y : F
rw :
  Eq.{u_7 + 1} (α := G) (((-(f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
    (-(((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
⊢ Eq.{u_7 + 1} (α := G) ((((f : (a : E) → F →SL[σ₂₃] G) (-x) : F →SL[σ₂₃] G) : (a : F) → G) y : G)
    (-(((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
have rw₁ : Eq.{u_7 + 1} (α := G) (-(((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
  (-(((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
Tactic: rw [map_neg, neg_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : ContinuousSMul 𝕜 E
F : Type u_3
inst_5 : AddCommGroup F
inst_6 : UniformSpace F
inst_7 : IsUniformAddGroup F
inst_8 : Module 𝕜 F
𝕜' : Type u_4
inst_9 : NontriviallyNormedField 𝕜'
inst_10 : NormedAlgebra 𝕜' 𝕜
inst_11 : Module 𝕜' E
inst_12 : IsScalarTower 𝕜' 𝕜 E
inst_13 : Module 𝕜' F
inst_14 : IsScalarTower 𝕜' 𝕜 F
⊢ IsUniformEmbedding (α := E →L[𝕜] F) (β := E →L[𝕜'] F) (restrictScalars 𝕜')
have rw : IsUniformEmbedding (α := E →L[𝕜] F) (β := E →ᵤ[{s : Set E | IsVonNBounded 𝕜' s}] F)
  ((fun (f : E →L[𝕜'] F) ↦
      (UniformOnFun.ofFun {s : Set E | IsVonNBounded 𝕜' s} : (a : E → F) → E →ᵤ[{s : Set E | IsVonNBounded 𝕜' s}] F)
        (⇑f : (a : E) → F)) ∘
    restrictScalars 𝕜')
Tactic: rw [← isUniformEmbedding_toUniformOnFun.of_comp_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : ContinuousSMul 𝕜 E
F : Type u_3
inst_5 : AddCommGroup F
inst_6 : UniformSpace F
inst_7 : IsUniformAddGroup F
inst_8 : Module 𝕜 F
𝕜' : Type u_4
inst_9 : NontriviallyNormedField 𝕜'
inst_10 : NormedAlgebra 𝕜' 𝕜
inst_11 : Module 𝕜' E
inst_12 : IsScalarTower 𝕜' 𝕜 E
inst_13 : Module 𝕜' F
inst_14 : IsScalarTower 𝕜' 𝕜 F
⊢ IsUniformEmbedding (α := E →L[𝕜] F) (β := E →ᵤ[{s : Set E | IsVonNBounded 𝕜' s}] F)
    ((fun (f : E →L[𝕜'] F) ↦
        (UniformOnFun.ofFun {s : Set E | IsVonNBounded 𝕜' s} : (a : E → F) → E →ᵤ[{s : Set E | IsVonNBounded 𝕜' s}] F)
          (⇑f : (a : E) → F)) ∘
      restrictScalars 𝕜')
have h : ∀ (s : Set E), IsVonNBounded 𝕜' s ↔ IsVonNBounded 𝕜 s
Tactic: convert! isUniformEmbedding_toUniformOnFun using 4 with s
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
S : Type u_5
inst : NormedField 𝕜
inst_1 : Semiring S
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousConstSMul 𝕜 E
inst_7 : AddCommGroup F
inst_8 : Module 𝕜 F
inst_9 : TopologicalSpace F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousConstSMul 𝕜 F
inst_12 : AddCommGroup G
inst_13 : Module 𝕜 G
inst_14 : TopologicalSpace G
inst_15 : IsTopologicalAddGroup G
inst_16 : ContinuousConstSMul 𝕜 G
inst_17 : Module S G
inst_18 : SMulCommClass 𝕜 S G
inst_19 : ContinuousConstSMul S G
inst_20 : Module S F
inst_21 : SMulCommClass 𝕜 S F
inst_22 : ContinuousConstSMul S F
⊢ Continuous[instTopologicalSpaceProd, topologicalSpace] fun (x : (E →L[𝕜] F) × (E →L[𝕜] G)) ↦
    comp (σ₁₂ := RingHom.id 𝕜) (ContinuousLinearMap.id 𝕜 (F × G))
      ((prodₗ S : (a : (E →L[𝕜] F) × (E →L[𝕜] G)) → E →L[𝕜] F × G) x)
have simp_rw : Continuous[instTopologicalSpaceProd, topologicalSpace] fun (x : (E →L[𝕜] F) × (E →L[𝕜] G)) ↦
  comp (σ₁₂ := RingHom.id 𝕜) (coprod (inl 𝕜 F G) (inr 𝕜 F G))
    ((prodₗ S : (a : (E →L[𝕜] F) × (E →L[𝕜] G)) → E →L[𝕜] F × G) x)
Tactic: simp_rw [← coprod_inl_inr]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap (goal)
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
⊢ 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
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap (goal)
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 : 𝕜
⊢ 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
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
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 𝔖))
    (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 𝔖))
have e_t : IsTopologicalAddGroup.rightUniformSpace F = inst_7
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
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 𝔖)) (instTopologicalSpace σ F 𝔖) UniformSpace.toTopologicalSpace
have rw : Eq (α := TopologicalSpace (UniformConvergenceCLM σ F 𝔖))
  (TopologicalSpace.induced (DFunLike.coe (β := fun (a : E) ↦ F)) (UniformOnFun.topologicalSpace E F 𝔖))
  UniformSpace.toTopologicalSpace
Tactic: rw [UniformConvergenceCLM.instTopologicalSpace, IsUniformAddGroup.rightUniformSpace_eq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
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 (α := 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 𝔖))
have 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 𝔖))
    sorry)
  (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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
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 𝔖))
⊢ 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 𝔖))
have 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 𝔖))
Tactic: rw [instUniformSpace, UniformSpace.replaceTopology_eq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (hypothesis)
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
⊢ IsTopologicalAddGroup (UniformConvergenceCLM σ F 𝔖)
have this₁ : IsUniformAddGroup F
Tactic: haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (hypothesis)
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
⊢ Continuous[instTopologicalSpace σ F 𝔖, inst_7] fun (f : UniformConvergenceCLM σ F 𝔖) ↦ (f : (a : E) → F) x
have this₁ : IsUniformAddGroup F
Tactic: haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (hypothesis)
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
⊢ T2Space (UniformConvergenceCLM σ F 𝔖)
have this₁ : IsUniformAddGroup F
Tactic: haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (hypothesis)
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 (UniformConvergenceCLM σ F 𝔖)
have this₁ : T2Space (E →ᵤ[𝔖] F)
Tactic: haveI : T2Space (E →ᵤ[𝔖] F) := UniformOnFun.t2Space_of_covering h𝔖
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (hypothesis)
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
⊢ ContinuousSMul 𝕜₂ (UniformConvergenceCLM σ F 𝔖)
have this₁ : IsUniformAddGroup F
Tactic: haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (hypothesis)
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
⊢ 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)}
have this₁ : IsUniformAddGroup F
Tactic: haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (goal)
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 𝔖) (𝓝 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)}
have 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)}
Tactic: rw [(isEmbedding_coeFn σ F 𝔖).isInducing.nhds_eq_comap]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM (hypothesis)
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)
ι : Type u_6
p : ι → Prop
b : ι → Set F
h : HasBasis (𝓝 0) p b
this : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
⊢ Eq (α := Filter (UniformConvergenceCLM σ F 𝔖)) (𝓝 0)
    (⨅ s ∈ 𝔖, ⨅ (i : ι), ⨅ (_ : p i), 𝓟 {f : UniformConvergenceCLM σ F 𝔖 | MapsTo (⇑f : (a : E) → F) s (b i)})
have this₁ : IsUniformAddGroup F
Tactic: haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup