awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : Fintype l
inst_5 : DecidableEq l
normed_add_comm_group : NormedAddCommGroup (Matrix m n 𝕜) :=
  let __src : MetricSpace (Matrix m n 𝕜) := MetricSpace.replaceTopology NormedAddCommGroup.toMetricSpace ⋯;
  { toNorm := l2OpNormedAddCommGroupAux.toNorm, toAddCommGroup := addCommGroup, toMetricSpace := __src, dist_eq := ⋯ }
h : instUniformSpace m n 𝕜 = PseudoEMetricSpace.toUniformSpace
⊢ Eq (α := Filter (Matrix m n 𝕜 × Matrix m n 𝕜)) (𝓤 (Matrix m n 𝕜)) (𝓤 (Matrix m n 𝕜))

Tactic:
congr
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : Fintype l
inst_5 : DecidableEq l
normed_add_comm_group : NormedAddCommGroup (Matrix m n 𝕜) :=
  let __src : MetricSpace (Matrix m n 𝕜) := MetricSpace.replaceTopology NormedAddCommGroup.toMetricSpace ⋯;
  { toNorm := l2OpNormedAddCommGroupAux.toNorm, toAddCommGroup := addCommGroup, toMetricSpace := __src, dist_eq := ⋯ }
h :
  Eq (α := UniformSpace (Matrix m n 𝕜)) (IsTopologicalAddGroup.rightUniformSpace (Matrix m n 𝕜))
    PseudoEMetricSpace.toUniformSpace
⊢ instUniformSpace m n 𝕜 = PseudoEMetricSpace.toUniformSpace

Tactic:
rw [← @IsUniformAddGroup.rightUniformSpace_eq _ (Matrix.instUniformSpace m n 𝕜) _ _]

Premises used: IsUniformAddGroup.rightUniformSpace_eq
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : Fintype l
inst_5 : DecidableEq l
normed_add_comm_group : NormedAddCommGroup (Matrix m n 𝕜) :=
  let __src : MetricSpace (Matrix m n 𝕜) := MetricSpace.replaceTopology NormedAddCommGroup.toMetricSpace ⋯;
  { toNorm := l2OpNormedAddCommGroupAux.toNorm, toAddCommGroup := addCommGroup, toMetricSpace := __src, dist_eq := ⋯ }
h h₁ : Eq (α := UniformSpace (Matrix m n 𝕜)) PseudoEMetricSpace.toUniformSpace PseudoEMetricSpace.toUniformSpace
⊢ Eq (α := UniformSpace (Matrix m n 𝕜)) (IsTopologicalAddGroup.rightUniformSpace (Matrix m n 𝕜))
    PseudoEMetricSpace.toUniformSpace

Tactic:
rw [@IsUniformAddGroup.rightUniformSpace_eq _ PseudoEMetricSpace.toUniformSpace _ _]

Premises used: IsUniformAddGroup.rightUniformSpace_eq
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : Fintype l
inst_5 : DecidableEq l
normed_add_comm_group : NormedAddCommGroup (Matrix m n 𝕜) :=
  let __src : MetricSpace (Matrix m n 𝕜) := MetricSpace.replaceTopology NormedAddCommGroup.toMetricSpace ⋯;
  { toNorm := l2OpNormedAddCommGroupAux.toNorm, toAddCommGroup := addCommGroup, toMetricSpace := __src, dist_eq := ⋯ }
⊢ MetricSpace (Matrix m n 𝕜)

Tactic:
exact normed_add_comm_group.replaceUniformity <| by
    congr
    rw [← @IsUniformAddGroup.rightUniformSpace_eq _ (Matrix.instUniformSpace m n 𝕜) _ _]
    rw [@IsUniformAddGroup.rightUniformSpace_eq _ PseudoEMetricSpace.toUniformSpace _ _]

Premises used: NormedAddCommGroup.toMetricSpace, MetricSpace.replaceUniformity
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq n
A : Matrix m n 𝕜
⊢ ‖A‖ =
    norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
      ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m) A :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq n
A : Matrix m n 𝕜
⊢ ‖A‖₊ =
    nnnorm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
      ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m) A :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : DecidableEq m
A : Matrix m n 𝕜
rw :
  norm (E := EuclideanSpace 𝕜 m →L[𝕜] EuclideanSpace 𝕜 n)
      ((ContinuousLinearMap.adjoint :
            (a : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m) → EuclideanSpace 𝕜 m →L[𝕜] EuclideanSpace 𝕜 n)
          (((toContinuousLinearMap :
                (EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m) ≃ₗ[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m) :
              (a : EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
            ((toLin (OrthonormalBasis.toBasis (EuclideanSpace.basisFun n 𝕜))
                  (OrthonormalBasis.toBasis (EuclideanSpace.basisFun m 𝕜)) :
                (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m)
              A)) :
        EuclideanSpace 𝕜 m →L[𝕜] EuclideanSpace 𝕜 n) =
    ‖A‖
⊢ ‖Aᴴ‖ = ‖A‖

Tactic:
rw [l2_opNorm_def, toEuclideanLin_eq_toLin_orthonormal, LinearEquiv.trans_apply,
    toLin_conjTranspose, adjoint_toContinuousLinearMap]

Premises used: LinearMap.adjoint_toContinuousLinearMap, LinearEquiv.trans_apply, Matrix.toLin_conjTranspose, Matrix.toEuclideanLin_eq_toLin_orthonormal, Matrix.l2_opNorm_def
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : DecidableEq m
A : Matrix m n 𝕜
⊢ norm (E := EuclideanSpace 𝕜 m →L[𝕜] EuclideanSpace 𝕜 n)
      ((ContinuousLinearMap.adjoint :
            (a : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m) → EuclideanSpace 𝕜 m →L[𝕜] EuclideanSpace 𝕜 n)
          (((toContinuousLinearMap :
                (EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m) ≃ₗ[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m) :
              (a : EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
            ((toLin (OrthonormalBasis.toBasis (EuclideanSpace.basisFun n 𝕜))
                  (OrthonormalBasis.toBasis (EuclideanSpace.basisFun m 𝕜)) :
                (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m)
              A)) :
        EuclideanSpace 𝕜 m →L[𝕜] EuclideanSpace 𝕜 n) =
    ‖A‖

Tactic:
ContinuousLinearMap.adjoint.norm_map _

Premises used: Multiset.sum, Multiset.foldr, LinearIsometryEquiv.norm_map, dotProduct, ContinuousLinearMap.adjoint, Matrix.mulVec, Finset.sum
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : DecidableEq m
A : Matrix m n 𝕜
⊢ norm (E := EuclideanSpace 𝕜 m →L[𝕜] EuclideanSpace 𝕜 n)
      ((ContinuousLinearMap.adjoint :
            (a : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m) → EuclideanSpace 𝕜 m →L[𝕜] EuclideanSpace 𝕜 n)
          (((toContinuousLinearMap :
                (EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m) ≃ₗ[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m) :
              (a : EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
            ((toLin (OrthonormalBasis.toBasis (EuclideanSpace.basisFun n 𝕜))
                  (OrthonormalBasis.toBasis (EuclideanSpace.basisFun m 𝕜)) :
                (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m)
              A)) :
        EuclideanSpace 𝕜 m →L[𝕜] EuclideanSpace 𝕜 n) =
    ‖A‖

Tactic:
exact ContinuousLinearMap.adjoint.norm_map _

Premises used: LinearIsometryEquiv.norm_map, ContinuousLinearMap.adjoint
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : DecidableEq m
A : Matrix m n 𝕜
⊢ ‖Aᴴ‖₊ = ‖A‖₊

Tactic:
Subtype.ext <| l2_opNorm_conjTranspose _

Premises used: Matrix.l2_opNorm_conjTranspose, NNReal, Subtype.ext
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq n
A : Matrix m n 𝕜
rw :
  norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
      (((toContinuousLinearMap :
              (EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) ≃ₗ[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) :
            (a : EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
          ((adjoint : (a : EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m) → EuclideanSpace 𝕜 m →ₗ[𝕜] EuclideanSpace 𝕜 n)
              ((toLin (OrthonormalBasis.toBasis (EuclideanSpace.basisFun n 𝕜))
                    (OrthonormalBasis.toBasis (EuclideanSpace.basisFun m 𝕜)) :
                  (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m)
                A) ∘ₗ
            (toLin (OrthonormalBasis.toBasis (EuclideanSpace.basisFun n 𝕜))
                  (OrthonormalBasis.toBasis (EuclideanSpace.basisFun m 𝕜)) :
                (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m)
              A) :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) =
    ‖A‖ * ‖A‖
⊢ ‖Aᴴ * A‖ = ‖A‖ * ‖A‖

Tactic:
rw [l2_opNorm_def, toEuclideanLin_eq_toLin_orthonormal, LinearEquiv.trans_apply,
    Matrix.toLin_mul (v₂ := (EuclideanSpace.basisFun m 𝕜).toBasis), toLin_conjTranspose]

Premises used: Matrix.toLin_mul, LinearEquiv.trans_apply, EuclideanSpace.basisFun, Matrix.toLin_conjTranspose, Matrix.toEuclideanLin_eq_toLin_orthonormal, Matrix.l2_opNorm_def, OrthonormalBasis.toBasis
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq n
A : Matrix m n 𝕜
⊢ norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
      (((toContinuousLinearMap :
              (EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) ≃ₗ[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) :
            (a : EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
          ((adjoint : (a : EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m) → EuclideanSpace 𝕜 m →ₗ[𝕜] EuclideanSpace 𝕜 n)
              ((toLin (OrthonormalBasis.toBasis (EuclideanSpace.basisFun n 𝕜))
                    (OrthonormalBasis.toBasis (EuclideanSpace.basisFun m 𝕜)) :
                  (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m)
                A) ∘ₗ
            (toLin (OrthonormalBasis.toBasis (EuclideanSpace.basisFun n 𝕜))
                  (OrthonormalBasis.toBasis (EuclideanSpace.basisFun m 𝕜)) :
                (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m)
              A) :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) =
    ‖A‖ * ‖A‖

Tactic:
ContinuousLinearMap.norm_adjoint_comp_self _

Premises used: ContinuousLinearMap.comp, Multiset.sum, Multiset.foldr, dotProduct, ContinuousLinearMap.norm_adjoint_comp_self, Matrix.mulVec, Finset.sum
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq n
A : Matrix m n 𝕜
⊢ norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
      (((toContinuousLinearMap :
              (EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) ≃ₗ[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) :
            (a : EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
          ((adjoint : (a : EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m) → EuclideanSpace 𝕜 m →ₗ[𝕜] EuclideanSpace 𝕜 n)
              ((toLin (OrthonormalBasis.toBasis (EuclideanSpace.basisFun n 𝕜))
                    (OrthonormalBasis.toBasis (EuclideanSpace.basisFun m 𝕜)) :
                  (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m)
                A) ∘ₗ
            (toLin (OrthonormalBasis.toBasis (EuclideanSpace.basisFun n 𝕜))
                  (OrthonormalBasis.toBasis (EuclideanSpace.basisFun m 𝕜)) :
                (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m)
              A) :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) =
    ‖A‖ * ‖A‖

Tactic:
exact ContinuousLinearMap.norm_adjoint_comp_self _

Premises used: ContinuousLinearMap.norm_adjoint_comp_self
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq n
A : Matrix m n 𝕜
⊢ ‖Aᴴ * A‖₊ = ‖A‖₊ * ‖A‖₊

Tactic:
Subtype.ext <| l2_opNorm_conjTranspose_mul_self _

Premises used: Matrix.l2_opNorm_conjTranspose_mul_self, NNReal, Subtype.ext
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq n
A : Matrix m n 𝕜
x : EuclideanSpace 𝕜 n
⊢ norm (E := EuclideanSpace 𝕜 m)
      ((ContinuousLinearEquiv.symm (EuclideanSpace.equiv m 𝕜) : (a : m → 𝕜) → EuclideanSpace 𝕜 m) (A *ᵥ x.ofLp) :
        EuclideanSpace 𝕜 m) ≤
    ‖A‖ * ‖x‖

Tactic:
toEuclideanLin (n := n) (m := m) (𝕜 := 𝕜) |>.trans toContinuousLinearMap A |>.le_opNorm x

Premises used: Multiset.sum, Multiset.foldr, dotProduct, ContinuousLinearMap.le_opNorm, Matrix.toEuclideanLin, setOf, Matrix.mulVec, LinearEquiv.trans, DFunLike.coe, Finset.sum, LinearMap.toContinuousLinearMap
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq n
A : Matrix m n 𝕜
x : EuclideanSpace 𝕜 n
⊢ nnnorm (E := EuclideanSpace 𝕜 m)
      ((ContinuousLinearEquiv.symm (EuclideanSpace.equiv m 𝕜) : (a : m → 𝕜) → EuclideanSpace 𝕜 m) (A *ᵥ x.ofLp) :
        EuclideanSpace 𝕜 m) ≤
    ‖A‖₊ * ‖x‖₊

Tactic:
A.l2_opNorm_mulVec x

Premises used: Matrix.l2_opNorm_mulVec, setOf
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
inst : RCLike 𝕜
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : Fintype l
inst_5 : DecidableEq l
A : Matrix m n 𝕜
B : Matrix n l 𝕜
simp :
  norm (E := EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 m)
      ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix m l 𝕜) → EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 m)
          (A * B) :
        EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 m) ≤
    norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
            A :
          EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m) *
      norm (E := EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix n l 𝕜) → EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
            B :
          EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
⊢ ‖A * B‖ ≤ ‖A‖ * ‖B‖

Tactic:
simp only [l2_opNorm_def]

Premises used: Matrix.l2_opNorm_def
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
inst : RCLike 𝕜
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : Fintype l
inst_5 : DecidableEq l
A : Matrix m n 𝕜
B : Matrix n l 𝕜
⊢ norm (E := EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 m)
      (ContinuousLinearMap.comp (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := EuclideanSpace 𝕜 n)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
          A)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix n l 𝕜) → EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
          B)) ≤
    norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
            A :
          EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m) *
      norm (E := EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix n l 𝕜) → EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
            B :
          EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)

Tactic:
have := (toEuclideanLin (n := n) (m := m) (𝕜 := 𝕜) ≪≫ₗ toContinuousLinearMap) A
    |>.opNorm_comp_le <| (toEuclideanLin (n := l) (m := n) (𝕜 := 𝕜) ≪≫ₗ toContinuousLinearMap) B
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
inst : RCLike 𝕜
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : Fintype l
inst_5 : DecidableEq l
A : Matrix m n 𝕜
B : Matrix n l 𝕜
this :
  norm (E := EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 m)
      (ContinuousLinearMap.comp (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := EuclideanSpace 𝕜 n)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
          A)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix n l 𝕜) → EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
          B)) ≤
    norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
            A :
          EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m) *
      norm (E := EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix n l 𝕜) → EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
            B :
          EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
⊢ norm (E := EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 m)
      (ContinuousLinearMap.comp (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := EuclideanSpace 𝕜 n)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
          A)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix n l 𝕜) → EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
          B)) ≤
    norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
            A :
          EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m) *
      norm (E := EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix n l 𝕜) → EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
            B :
          EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)

Tactic:
this
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
inst : RCLike 𝕜
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : Fintype l
inst_5 : DecidableEq l
A : Matrix m n 𝕜
B : Matrix n l 𝕜
this :
  norm (E := EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 m)
      (ContinuousLinearMap.comp (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := EuclideanSpace 𝕜 n)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
          A)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix n l 𝕜) → EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
          B)) ≤
    norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
            A :
          EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m) *
      norm (E := EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix n l 𝕜) → EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
            B :
          EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
h :
  Eq (α := EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 m)
    ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix m l 𝕜) → EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 m)
        (A * B) :
      EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 m)
    (ContinuousLinearMap.comp (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := EuclideanSpace 𝕜 n)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
          A)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix n l 𝕜) → EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
          B) :
      EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 m)
⊢ norm (E := EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 m)
      ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix m l 𝕜) → EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 m)
          (A * B) :
        EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 m) ≤
    norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
            A :
          EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m) *
      norm (E := EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix n l 𝕜) → EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
            B :
          EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)

Tactic:
convert! this
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
inst : RCLike 𝕜
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : Fintype l
inst_5 : DecidableEq l
A : Matrix m n 𝕜
B : Matrix n l 𝕜
this :
  norm (E := EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 m)
      (ContinuousLinearMap.comp (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := EuclideanSpace 𝕜 n)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
          A)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix n l 𝕜) → EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
          B)) ≤
    norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
            A :
          EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m) *
      norm (E := EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix n l 𝕜) → EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
            B :
          EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
h :
  ∀ (x : EuclideanSpace 𝕜 l),
    Eq (α := EuclideanSpace 𝕜 m)
      ((((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix m l 𝕜) → EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 m)
                (A * B) :
              EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 m) :
            (a : EuclideanSpace 𝕜 l) → EuclideanSpace 𝕜 m)
          x :
        EuclideanSpace 𝕜 m)
      ((ContinuousLinearMap.comp (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := EuclideanSpace 𝕜 n)
              ((toEuclideanLin ≪≫ₗ toContinuousLinearMap :
                  (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
                A)
              ((toEuclideanLin ≪≫ₗ toContinuousLinearMap :
                  (a : Matrix n l 𝕜) → EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
                B) :
            (a : EuclideanSpace 𝕜 l) → EuclideanSpace 𝕜 m)
          x :
        EuclideanSpace 𝕜 m)
⊢ Eq (α := EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 m)
    ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix m l 𝕜) → EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 m)
        (A * B) :
      EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 m)
    (ContinuousLinearMap.comp (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := EuclideanSpace 𝕜 n)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)
          A)
        ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix n l 𝕜) → EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 n)
          B) :
      EuclideanSpace 𝕜 l →L[𝕜] EuclideanSpace 𝕜 m)

Tactic:
ext1 x