awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Matrix (goal)
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
norm_sum : HPow.hPow (β := ℕ) ‖U i j‖ 2 ≤ ∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2
⊢ (U * Uᴴ) i i = (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜)
have simp : Eq.{u_1 + 1} (α := 𝕜) (∑ x : n, HPow.hPow (α := 𝕜) (β := ℕ) (↑‖U i x‖ : 𝕜) 2)
  (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜)
Tactic: simp only [Matrix.mul_apply, Matrix.conjTranspose_apply, ← starRingEnd_apply, RCLike.mul_conj]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Matrix (goal)
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
norm_sum : HPow.hPow (β := ℕ) ‖U i j‖ 2 ≤ ∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ x : n, HPow.hPow (α := 𝕜) (β := ℕ) (↑‖U i x‖ : 𝕜) 2)
    (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜)
have norm_cast : Eq (α := ℝ) (∑ i_1 : n, HPow.hPow (β := ℕ) ‖U i i_1‖ 2) (∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Matrix (hypothesis)
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
norm_sum : HPow.hPow (β := ℕ) ‖U i j‖ 2 ≤ ∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2
⊢ ‖U i j‖ ≤ 1
have diag_eq_norm_sum : (U * Uᴴ) i i = (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜)
Tactic: have diag_eq_norm_sum : (U * Uᴴ) i i = (∑ x : n, ‖U i x‖ ^ 2 : ℝ) := by
    simp only [Matrix.mul_apply, Matrix.conjTranspose_apply, ← starRingEnd_apply, RCLike.mul_conj]
    norm_cast
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Matrix (hypothesis)
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
norm_sum : HPow.hPow (β := ℕ) ‖U i j‖ 2 ≤ ∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2
diag_eq_norm_sum : (U * Uᴴ) i i = (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜)
⊢ Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ((U * Uᴴ) i i) : ℝ) (∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2 : ℝ)
have diag_eq_norm_sum₁ : Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ((U * Uᴴ) i i) : ℝ)
    ((RCLike.re : (a : 𝕜) → ℝ) (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜) : ℝ) ∧
  Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) ((U * Uᴴ) i i) : ℝ)
    ((RCLike.im : (a : 𝕜) → ℝ) (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜) : ℝ)
Tactic: rw [RCLike.ext_iff] at diag_eq_norm_sum
Cleared hypotheses: diag_eq_norm_sum
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Matrix (goal)
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
norm_sum : HPow.hPow (β := ℕ) ‖U i j‖ 2 ≤ ∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2
diag_eq_norm_sum :
  Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ((U * Uᴴ) i i) : ℝ)
      ((RCLike.re : (a : 𝕜) → ℝ) (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜) : ℝ) ∧
    Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) ((U * Uᴴ) i i) : ℝ)
      ((RCLike.im : (a : 𝕜) → ℝ) (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜) : ℝ)
⊢ Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ((U * Uᴴ) i i) : ℝ) (∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2 : ℝ)
have rw : Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜) : ℝ)
  (∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2 : ℝ)
Tactic: rw [diag_eq_norm_sum.1]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Matrix (goal)
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
norm_sum : HPow.hPow (β := ℕ) ‖U i j‖ 2 ≤ ∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2
diag_eq_norm_sum :
  Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ((U * Uᴴ) i i) : ℝ)
      ((RCLike.re : (a : 𝕜) → ℝ) (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜) : ℝ) ∧
    Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) ((U * Uᴴ) i i) : ℝ)
      ((RCLike.im : (a : 𝕜) → ℝ) (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜) : ℝ)
⊢ Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜) : ℝ)
    (∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2 : ℝ)
have norm_cast : Eq (α := ℝ) (∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) (∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Matrix (hypothesis)
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
norm_sum : HPow.hPow (β := ℕ) ‖U i j‖ 2 ≤ ∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2
diag_eq_norm_sum : (U * Uᴴ) i i = (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜)
⊢ ‖U i j‖ ≤ 1
have re_diag_eq_norm_sum : Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ((U * Uᴴ) i i) : ℝ) (∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2 : ℝ)
Tactic: have re_diag_eq_norm_sum : RCLike.re ((U * Uᴴ) i i) = ∑ x : n, ‖U i x‖ ^ 2 := by
    rw [RCLike.ext_iff] at diag_eq_norm_sum
    rw [diag_eq_norm_sum.1]
    norm_cast
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Matrix (hypothesis)
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
norm_sum : HPow.hPow (β := ℕ) ‖U i j‖ 2 ≤ ∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2
diag_eq_norm_sum : (U * Uᴴ) i i = (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜)
re_diag_eq_norm_sum :
  Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ((U * Uᴴ) i i) : ℝ) (∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2 : ℝ)
⊢ ‖U i j‖ ≤ 1
have mul_eq_one : U * Uᴴ = 1
Tactic: have mul_eq_one : U * Uᴴ = 1 := Unitary.mul_star_self_of_mem hU
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Matrix (hypothesis)
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
norm_sum : HPow.hPow (β := ℕ) ‖U i j‖ 2 ≤ ∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2
diag_eq_norm_sum : (U * Uᴴ) i i = (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜)
re_diag_eq_norm_sum :
  Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ((U * Uᴴ) i i) : ℝ) (∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2 : ℝ)
mul_eq_one : U * Uᴴ = 1
⊢ ‖U i j‖ ≤ 1
have diag_eq_one : Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ((U * Uᴴ) i i) : ℝ) (1 : ℝ)
Tactic: have diag_eq_one : RCLike.re ((U * Uᴴ) i i) = 1 := by
    simp only [mul_eq_one, Matrix.one_apply_eq, RCLike.one_re]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Matrix (goal)
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
⊢ ‖U‖ ≤ 1
have simp_rw : ∀ (i i_1 : n), ‖U i i_1‖ ≤ 1
Tactic: simp_rw [pi_norm_le_iff_of_nonneg zero_le_one]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Matrix (goal)
Goal:
n : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
A : Matrix n n ℝ
x y : EuclideanSpace ℝ n
⊢ ⟪x,
      (((toEuclideanCLM : (a : Matrix n n ℝ) → EuclideanSpace ℝ n →L[ℝ] EuclideanSpace ℝ n) A :
            EuclideanSpace ℝ n →L[ℝ] EuclideanSpace ℝ n) :
          (a : EuclideanSpace ℝ n) → EuclideanSpace ℝ n)
        y⟫ =
    x.ofLp ⬝ᵥ A *ᵥ y.ofLp
have simp : Eq (α := ℝ)
  (∑ x_1 : n,
    (∑ x : n,
        HMul.hMul (α := ℝ) (β := ℝ) (∑ x_2 : n, y.ofLp x_2 * A x x_2 : ℝ)
          (Pi.single (M := fun (x : n) ↦ ℝ) x 1 x_1 : ℝ)) *
      x.ofLp x_1)
  (∑ x_1 : n, x.ofLp x_1 * ∑ x : n, y.ofLp x * A x_1 x)
Tactic: simp only [toEuclideanCLM, AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearEquiv.coe_coe,
    LinearEquiv.invFun_eq_symm, LinearMap.coe_toContinuousLinearMap_symm, StarAlgEquiv.trans_apply,
    LinearMap.toMatrixOrthonormal_symm_apply, LinearMap.toMatrix_symm, StarAlgEquiv.coe_mk,
    StarRingEquiv.coe_mk, RingEquiv.coe_mk, Equiv.coe_fn_mk, LinearMap.coe_toContinuousLinearMap',
    toLin_apply, mulVec_eq_sum, OrthonormalBasis.coe_toBasis_repr_apply,
    EuclideanSpace.basisFun_repr, op_smul_eq_smul, Finset.sum_apply, Pi.smul_apply, transpose_apply,
    smul_eq_mul, OrthonormalBasis.coe_toBasis, EuclideanSpace.basisFun_apply, PiLp.inner_apply,
    ofLp_sum, ofLp_smul, PiLp.ofLp_single, RCLike.inner_apply, conj_trivial, dotProduct]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Matrix (goal)
Goal:
n : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
A : Matrix n n ℝ
x y : EuclideanSpace ℝ n
⊢ Eq (α := ℝ)
    (∑ x_1 : n,
      (∑ x : n,
          HMul.hMul (α := ℝ) (β := ℝ) (∑ x_2 : n, y.ofLp x_2 * A x x_2 : ℝ)
            (Pi.single (M := fun (x : n) ↦ ℝ) x 1 x_1 : ℝ)) *
        x.ofLp x_1)
    (∑ x_1 : n, x.ofLp x_1 * ∑ x : n, y.ofLp x * A x_1 x)
have e_f : ∀ (i : n),
  (∑ x : n,
        HMul.hMul (α := ℝ) (β := ℝ) (∑ x_1 : n, y.ofLp x_1 * A x x_1 : ℝ)
          (Pi.single (M := fun (x : n) ↦ ℝ) x 1 i : ℝ)) *
      x.ofLp i =
    x.ofLp i * ∑ x : n, y.ofLp x * A i x
Tactic: congr with i
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Matrix (goal)
Goal:
n : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
A : Matrix n n ℝ
x y : EuclideanSpace ℝ n
i : n
⊢ (∑ x : n,
        HMul.hMul (α := ℝ) (β := ℝ) (∑ x_1 : n, y.ofLp x_1 * A x x_1 : ℝ)
          (Pi.single (M := fun (x : n) ↦ ℝ) x 1 i : ℝ)) *
      x.ofLp i =
    x.ofLp i * ∑ x : n, y.ofLp x * A i x
have e_f : (∑ x : n,
      HMul.hMul (α := ℝ) (β := ℝ) (∑ x_1 : n, y.ofLp x_1 * A x x_1 : ℝ) (Pi.single (M := fun (x : n) ↦ ℝ) x 1 i : ℝ)) *
    x.ofLp i =
  (∑ x : n, y.ofLp x * A i x) * x.ofLp i
Tactic: rw [mul_comm (x.ofLp i)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Matrix (goal)
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 := ⋯ }
⊢ Eq (α := Filter (Matrix m n 𝕜 × Matrix m n 𝕜)) (𝓤 (Matrix m n 𝕜)) (𝓤 (Matrix m n 𝕜))
have h : instUniformSpace m n 𝕜 = PseudoEMetricSpace.toUniformSpace
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Matrix (goal)
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 := ⋯ }
⊢ instUniformSpace m n 𝕜 = PseudoEMetricSpace.toUniformSpace
have h : Eq (α := UniformSpace (Matrix m n 𝕜)) (IsTopologicalAddGroup.rightUniformSpace (Matrix m n 𝕜))
  PseudoEMetricSpace.toUniformSpace
Tactic: rw [← @IsUniformAddGroup.rightUniformSpace_eq _ (Matrix.instUniformSpace m n 𝕜) _ _]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Matrix (goal)
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 := ⋯ }
⊢ Eq (α := UniformSpace (Matrix m n 𝕜)) (IsTopologicalAddGroup.rightUniformSpace (Matrix m n 𝕜))
    PseudoEMetricSpace.toUniformSpace
have h : Eq (α := UniformSpace (Matrix m n 𝕜)) PseudoEMetricSpace.toUniformSpace PseudoEMetricSpace.toUniformSpace
Tactic: rw [@IsUniformAddGroup.rightUniformSpace_eq _ PseudoEMetricSpace.toUniformSpace _ _]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Matrix (goal)
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‖
have 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‖
Tactic: rw [l2_opNorm_def, toEuclideanLin_eq_toLin_orthonormal, LinearEquiv.trans_apply,
    toLin_conjTranspose, adjoint_toContinuousLinearMap]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Matrix (goal)
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‖
have 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‖
Tactic: rw [l2_opNorm_def, toEuclideanLin_eq_toLin_orthonormal, LinearEquiv.trans_apply,
    Matrix.toLin_mul (v₂ := (EuclideanSpace.basisFun m 𝕜).toBasis), toLin_conjTranspose]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Matrix (goal)
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‖
have rw : norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
    ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
        (Aᴴ * A) :
      EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) =
  ‖A‖ * ‖A‖
Tactic: classical
  rw [l2_opNorm_def, toEuclideanLin_eq_toLin_orthonormal, LinearEquiv.trans_apply,
    Matrix.toLin_mul (v₂ := (EuclideanSpace.basisFun m 𝕜).toBasis), toLin_conjTranspose]
  exact ContinuousLinearMap.norm_adjoint_comp_self _
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Matrix (goal)
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)
      ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
          (Aᴴ * A) :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) =
    ‖A‖ * ‖A‖
⊢ ‖Aᴴ * A‖ = ‖A‖ * ‖A‖
have rw₁ : norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
    (((toLin (OrthonormalBasis.toBasis (EuclideanSpace.basisFun n 𝕜))
                (OrthonormalBasis.toBasis (EuclideanSpace.basisFun n 𝕜)) :
              Matrix n n 𝕜 ≃ₗ[𝕜] EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) ≪≫ₗ
            toContinuousLinearMap :
          (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
        (Aᴴ * A) :
      EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) =
  ‖A‖ * ‖A‖
Tactic: classical
  rw [l2_opNorm_def, toEuclideanLin_eq_toLin_orthonormal, LinearEquiv.trans_apply,
    Matrix.toLin_mul (v₂ := (EuclideanSpace.basisFun m 𝕜).toBasis), toLin_conjTranspose]
  exact ContinuousLinearMap.norm_adjoint_comp_self _
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Matrix (goal)
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)
      ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
          (Aᴴ * A) :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) =
    ‖A‖ * ‖A‖
rw₁ :
  norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
      (((toLin (OrthonormalBasis.toBasis (EuclideanSpace.basisFun n 𝕜))
                  (OrthonormalBasis.toBasis (EuclideanSpace.basisFun n 𝕜)) :
                Matrix n n 𝕜 ≃ₗ[𝕜] EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) ≪≫ₗ
              toContinuousLinearMap :
            (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
          (Aᴴ * A) :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) =
    ‖A‖ * ‖A‖
⊢ ‖Aᴴ * A‖ = ‖A‖ * ‖A‖
have 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)
        (((toLin (OrthonormalBasis.toBasis (EuclideanSpace.basisFun n 𝕜))
                (OrthonormalBasis.toBasis (EuclideanSpace.basisFun n 𝕜)) :
              Matrix n n 𝕜 ≃ₗ[𝕜] EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) :
            (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n)
          (Aᴴ * A)) :
      EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) =
  ‖A‖ * ‖A‖
Tactic: classical
  rw [l2_opNorm_def, toEuclideanLin_eq_toLin_orthonormal, LinearEquiv.trans_apply,
    Matrix.toLin_mul (v₂ := (EuclideanSpace.basisFun m 𝕜).toBasis), toLin_conjTranspose]
  exact ContinuousLinearMap.norm_adjoint_comp_self _
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Matrix (goal)
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)
      ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
          (Aᴴ * A) :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) =
    ‖A‖ * ‖A‖
rw₁ :
  norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
      (((toLin (OrthonormalBasis.toBasis (EuclideanSpace.basisFun n 𝕜))
                  (OrthonormalBasis.toBasis (EuclideanSpace.basisFun n 𝕜)) :
                Matrix n n 𝕜 ≃ₗ[𝕜] EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) ≪≫ₗ
              toContinuousLinearMap :
            (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
          (Aᴴ * A) :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) =
    ‖A‖ * ‖A‖
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)
          (((toLin (OrthonormalBasis.toBasis (EuclideanSpace.basisFun n 𝕜))
                  (OrthonormalBasis.toBasis (EuclideanSpace.basisFun n 𝕜)) :
                Matrix n n 𝕜 ≃ₗ[𝕜] EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) :
              (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n)
            (Aᴴ * A)) :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) =
    ‖A‖ * ‖A‖
⊢ ‖Aᴴ * A‖ = ‖A‖ * ‖A‖
have 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)
        (((toLin (OrthonormalBasis.toBasis (EuclideanSpace.basisFun m 𝕜))
                  (OrthonormalBasis.toBasis (EuclideanSpace.basisFun n 𝕜)) :
                Matrix n m 𝕜 ≃ₗ[𝕜] EuclideanSpace 𝕜 m →ₗ[𝕜] EuclideanSpace 𝕜 n) :
              (a : Matrix n m 𝕜) → EuclideanSpace 𝕜 m →ₗ[𝕜] EuclideanSpace 𝕜 n)
            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: classical
  rw [l2_opNorm_def, toEuclideanLin_eq_toLin_orthonormal, LinearEquiv.trans_apply,
    Matrix.toLin_mul (v₂ := (EuclideanSpace.basisFun m 𝕜).toBasis), toLin_conjTranspose]
  exact ContinuousLinearMap.norm_adjoint_comp_self _
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Matrix (goal)
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 𝕜
⊢ ‖A * B‖ ≤ ‖A‖ * ‖B‖
have 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)
Tactic: simp only [l2_opNorm_def]