awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
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 : AddCommMonoid 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
c : R
x : E
y : F
rw :
  (HSMul.hSMul (α := 𝕜₃) (β := F →SL[σ₂₃] G) ((σ₁₃ : (a : R) → 𝕜₃) c : 𝕜₃)
          ((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) :
        (a : F) → G)
      y =
    HSMul.hSMul.{u_4, u_7, u_7} (α := 𝕜₃) (β := G) ((σ₁₃ : (a : R) → 𝕜₃) c : 𝕜₃)
      ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
rw₁ rw₂ :
  HSMul.hSMul.{u_4, u_7, u_7} (α := 𝕜₃) (β := G) ((σ₁₃ : (a : R) → 𝕜₃) c : 𝕜₃)
      ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G) =
    HSMul.hSMul.{u_4, u_7, u_7} (α := 𝕜₃) (β := G) ((σ₁₃ : (a : R) → 𝕜₃) c : 𝕜₃)
      ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
⊢ (((f : (a : E) → F →SL[σ₂₃] G) (c • x) : F →SL[σ₂₃] G) : (a : F) → G) y =
    HSMul.hSMul.{u_4, u_7, u_7} (α := 𝕜₃) (β := G) ((σ₁₃ : (a : R) → 𝕜₃) c : 𝕜₃)
      ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)

Tactic:
rw [f.map_smulₛₗ, smul_apply]

Premises used: ContinuousLinearMap.smul_apply, ContinuousLinearMap.map_smulₛₗ
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
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 : AddCommMonoid 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 →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
L : E →SL[σ₁₃] F →SL[σ₂₃] G
v : E
w : F
⊢ Eq.{u_7 + 1} (α := G) ((((L.toLinearMap₁₂ : (a : E) → F →ₛₗ[σ₂₃] G) v : F →ₛₗ[σ₂₃] G) : (a : F) → G) w : G)
    ((((L : (a : E) → F →SL[σ₂₃] G) v : F →SL[σ₂₃] G) : (a : F) → G) w : G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
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 : AddCommMonoid 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 →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
⊢ Injective (α := E →SL[σ₁₃] F →SL[σ₂₃] G) toLinearMap₁₂

Tactic:
simp [Function.Injective, LinearMap.ext_iff, ← ContinuousLinearMap.ext_iff]

Premises used: LinearMap.ext_iff, ContinuousLinearMap.ext_iff, Function.Injective
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
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 : AddCommMonoid 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 →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
L₁ L₂ : E →SL[σ₁₃] F →SL[σ₂₃] G
⊢ L₁.toLinearMap₁₂ = L₂.toLinearMap₁₂ ↔ L₁ = L₂

Tactic:
toLinearMap₁₂_injective.eq_iff

Premises used: ContinuousLinearMap.toLinearMap₁₂_injective, Function.Injective.eq_iff
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜₂ : Type u_3
𝕜₃ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : NormedField 𝕜₂
inst_1 : NormedField 𝕜₃
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜₃ E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace F
inst_8 : AddCommGroup G
inst_9 : Module 𝕜₃ G
inst_10 : TopologicalSpace G
inst_11 : IsTopologicalAddGroup G
inst_12 : ContinuousConstSMul 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
f : E →L[𝕜₃] F →SL[σ₂₃] G
c : 𝕜₃
x : E
y : F
rw :
  (HSMul.hSMul (β := F →SL[σ₂₃] G) c ((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y =
    HSMul.hSMul (β := G) c ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
rw₁ rw₂ :
  HSMul.hSMul (β := G) c ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G) =
    HSMul.hSMul (β := G) c ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)
⊢ (((f : (a : E) → F →SL[σ₂₃] G) (c • x) : F →SL[σ₂₃] G) : (a : F) → G) y =
    HSMul.hSMul (β := G) c ((((f : (a : E) → F →SL[σ₂₃] G) x : F →SL[σ₂₃] G) : (a : F) → G) y : G)

Tactic:
rw [f.map_smul, smul_apply]

Premises used: ContinuousLinearMap.smul_apply, ContinuousLinearMap.map_smul
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
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)
rw₁ 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)
⊢ (((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)

Tactic:
rw [map_sub, sub_apply]

Premises used: map_sub, ContinuousLinearMap.sub_apply
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
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)
rw₁ 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)

Tactic:
rw [map_neg, neg_apply]

Premises used: map_neg, ContinuousLinearMap.neg_apply
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜 : Type u_2
E : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
L : E →L[𝕜] E →L[𝕜] 𝕜
v w : E
⊢ Eq.{u_2 + 1} (α := 𝕜) ((((L.toBilinForm : (a : E) → E →ₗ[𝕜] 𝕜) v : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) w : 𝕜)
    ((((L : (a : E) → E →L[𝕜] 𝕜) v : E →L[𝕜] 𝕜) : (a : E) → 𝕜) w : 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜 : Type u_2
E : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
⊢ Injective (α := E →L[𝕜] E →L[𝕜] 𝕜) toBilinForm

Tactic:
toLinearMap₁₂_injective

Premises used: ContinuousLinearMap.toBilinForm, ContinuousLinearMap.toLinearMap₁₂_injective
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Goal:
𝕜 : Type u_2
E : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
L₁ L₂ : E →L[𝕜] E →L[𝕜] 𝕜
⊢ L₁.toBilinForm = L₂.toBilinForm ↔ L₁ = L₂

Tactic:
toBilinForm_injective.eq_iff

Premises used: Function.Injective.eq_iff, ContinuousLinearMap.toBilinForm_injective
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
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
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 𝕜')
⊢ IsUniformEmbedding (α := E →L[𝕜] F) (β := E →L[𝕜'] F) (restrictScalars 𝕜')

Tactic:
rw [← isUniformEmbedding_toUniformOnFun.of_comp_iff]

Premises used: IsUniformEmbedding.of_comp_iff, ContinuousLinearMap.isUniformEmbedding_toUniformOnFun
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
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 →ᵤ[{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)

Tactic:
isUniformEmbedding_toUniformOnFun

Premises used: ContinuousLinearMap.isUniformEmbedding_toUniformOnFun
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
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
h : ∀ (s : Set E), IsVonNBounded 𝕜' s ↔ IsVonNBounded 𝕜 s
⊢ 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:
convert! isUniformEmbedding_toUniformOnFun using 4 with s

Premises used: ContinuousLinearMap.isUniformEmbedding_toUniformOnFun
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
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
s : Set E
⊢ IsVonNBounded 𝕜' s ↔ IsVonNBounded 𝕜 s

Tactic:
⟨fun h ↦ h.extend_scalars _, fun h ↦ h.restrict_scalars _⟩

Premises used: Bornology.IsVonNBounded.restrict_scalars, Bornology.IsVonNBounded.extend_scalars, Iff.intro
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
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
s : Set E
⊢ IsVonNBounded 𝕜' s ↔ IsVonNBounded 𝕜 s

Tactic:
exact ⟨fun h ↦ h.extend_scalars _, fun h ↦ h.restrict_scalars _⟩
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
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
⊢ UniformContinuous (α := E →L[𝕜] F) (β := E →L[𝕜'] F) (restrictScalars 𝕜')

Tactic:
(isUniformEmbedding_restrictScalars 𝕜').uniformContinuous

Premises used: ContinuousLinearMap.isUniformEmbedding_restrictScalars, IsUniformEmbedding.toIsUniformInducing, IsUniformInducing.uniformContinuous
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
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 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup 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
⊢ IsEmbedding (X := E →L[𝕜] F) (Y := E →L[𝕜'] F) (restrictScalars 𝕜')

Tactic:
letI : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
  haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
  (isUniformEmbedding_restrictScalars _).isEmbedding

Premises used: ContinuousLinearMap.isUniformEmbedding_restrictScalars, IsUniformEmbedding.isEmbedding
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
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 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup 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
⊢ Continuous[topologicalSpace, topologicalSpace] (restrictScalars 𝕜')

Tactic:
(isEmbedding_restrictScalars _).continuous

Premises used: ContinuousLinearMap.isEmbedding_restrictScalars, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
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 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup 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
𝕜'' : Type u_5
inst_15 : Ring 𝕜''
inst_16 : Module 𝕜'' F
inst_17 : ContinuousConstSMul 𝕜'' F
inst_18 : SMulCommClass 𝕜 𝕜'' F
inst_19 : SMulCommClass 𝕜' 𝕜'' F
⊢ Eq (α := (E →L[𝕜] F) →ₗ[𝕜''] E →L[𝕜'] F)
    ((↑(restrictScalarsL 𝕜 E F 𝕜' 𝕜'') : (E →L[𝕜] F) →ₗ[𝕜''] E →L[𝕜'] F) : (E →L[𝕜] F) →ₗ[𝕜''] E →L[𝕜'] F)
    (restrictScalarsₗ 𝕜 E F 𝕜' 𝕜'' : (E →L[𝕜] F) →ₗ[𝕜''] E →L[𝕜'] F)

Tactic:
rfl

Premises used: ContinuousLinearMap.restrictScalarsₗ, rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
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 : TopologicalSpace F
inst_7 : IsTopologicalAddGroup 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
𝕜'' : Type u_5
inst_15 : Ring 𝕜''
inst_16 : Module 𝕜'' F
inst_17 : ContinuousConstSMul 𝕜'' F
inst_18 : SMulCommClass 𝕜 𝕜'' F
inst_19 : SMulCommClass 𝕜' 𝕜'' F
⊢ Eq (α := (a : E →L[𝕜] F) → E →L[𝕜'] F) (⇑(restrictScalarsL 𝕜 E F 𝕜' 𝕜'') : (a : E →L[𝕜] F) → E →L[𝕜'] F)
    (restrictScalars 𝕜')

Tactic:
rfl

Premises used: ContinuousLinearMap.restrictScalars, rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
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
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)
⊢ 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)

Tactic:
simp_rw [← coprod_inl_inr]

Premises used: ContinuousLinearMap.coprod_inl_inr
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
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 𝕜) (coprod (inl 𝕜 F G) (inr 𝕜 F G))
      ((prodₗ S : (a : (E →L[𝕜] F) × (E →L[𝕜] G)) → E →L[𝕜] F × G) x)

Tactic:
(((inl 𝕜 F G).postcomp E).coprod ((inr 𝕜 F G).postcomp E)).continuous

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.postcomp, ContinuousLinearMap.inr, ContinuousLinearMap.continuous, ContinuousLinearMap.coprod, ContinuousLinearMap.inl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
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 𝕜) (coprod (inl 𝕜 F G) (inr 𝕜 F G))
      ((prodₗ S : (a : (E →L[𝕜] F) × (E →L[𝕜] G)) → E →L[𝕜] F × G) x)

Tactic:
exact (((inl 𝕜 F G).postcomp E).coprod ((inr 𝕜 F G).postcomp E)).continuous

Premises used: ContinuousLinearMap.postcomp, ContinuousLinearMap.inr, ContinuousLinearMap.continuous, ContinuousLinearMap.coprod, ContinuousLinearMap.inl
-- 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₁ : E ≃L[𝕜] F
e₂ : H ≃L[𝕜] G
f : E →L[𝕜] H
x : F
⊢ Eq.{u_4 + 1} (α := G) ((((e₁.arrowCongr e₂ : (a : E →L[𝕜] H) → F →L[𝕜] G) f : F →L[𝕜] G) : (a : F) → G) x : G)
    ((e₂ : (a : H) → G) ((f : (a : E) → H) ((e₁.symm : (a : F) → E) x : E) : H) : G)

Tactic:
rfl

Premises used: rfl
-- 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₁ : E ≃L[𝕜] F
e₂ : H ≃L[𝕜] G
⊢ Eq (α := (F →L[𝕜] G) ≃L[𝕜] E →L[𝕜] H) (ContinuousLinearEquiv.symm (e₁.arrowCongr e₂)) (e₁.symm.arrowCongr e₂.symm)

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, ContinuousLinearEquiv.symm, LinearEquiv.symm, ContinuousLinearEquiv.arrowCongr, ContinuousLinearEquiv.arrowCongrSL, rfl