awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Matrix (hypothesis)
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)
      ((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)
have 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)
Tactic: have := (toEuclideanLin (n := n) (m := m) (𝕜 := 𝕜) ≪≫ₗ toContinuousLinearMap) A
    |>.opNorm_comp_le <| (toEuclideanLin (n := l) (m := n) (𝕜 := 𝕜) ≪≫ₗ toContinuousLinearMap) B
-- 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 𝕜
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)
      ((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)
have 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)
Tactic: convert! this
-- 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 𝕜
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)
⊢ 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)
have 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)
Tactic: ext1 x
-- 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
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n :=
  (toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v)
⊢ ‖diagonal v‖ = ‖v‖
have rw : norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
    ((toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v) :
      EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) =
  ‖v‖
Tactic: rw [← l2_opNorm_toEuclideanCLM]
-- 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
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n :=
  (toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v)
⊢ norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
      ((toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v) :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) =
    ‖v‖
have refine_1 : norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
    ((toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v) :
      EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) ≤
  ‖v‖
Tactic: refine le_antisymm ?_ ?_
-- 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
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n :=
  (toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v)
refine_1 :
  norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
      ((toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v) :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) ≤
    ‖v‖
⊢ norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
      ((toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v) :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) =
    ‖v‖
have refine_2 : ‖v‖ ≤
  norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
    ((toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v) :
      EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
Tactic: refine le_antisymm ?_ ?_
-- 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
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n :=
  (toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v)
⊢ norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
      ((toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v) :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) ≤
    ‖v‖
have refine_1 : ∀ (x : EuclideanSpace 𝕜 n),
  norm (E := EuclideanSpace 𝕜 n) ((T : (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n) x : EuclideanSpace 𝕜 n) ≤
    ‖v‖ * ‖x‖
Tactic: refine T.opNorm_le_bound (norm_nonneg _) fun x ↦ ?_
-- 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
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n :=
  (toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v)
x : EuclideanSpace 𝕜 n
⊢ norm (E := EuclideanSpace 𝕜 n) ((T : (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n) x : EuclideanSpace 𝕜 n) ≤
    ‖v‖ * ‖x‖
have refine_1 : HPow.hPow (β := ℕ)
    (norm (E := EuclideanSpace 𝕜 n) ((T : (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n) x : EuclideanSpace 𝕜 n)) 2 ≤
  HPow.hPow (β := ℕ) (‖v‖ * ‖x‖) 2
Tactic: refine (sq_le_sq₀ (by positivity) (by positivity)).mp ?_
-- 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
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n :=
  (toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v)
x : EuclideanSpace 𝕜 n
⊢ HPow.hPow (β := ℕ)
      (norm (E := EuclideanSpace 𝕜 n) ((T : (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n) x : EuclideanSpace 𝕜 n)) 2 ≤
    HPow.hPow (β := ℕ) (‖v‖ * ‖x‖) 2
have refine_1 : ∑ x_1 : n, HPow.hPow (β := ℕ) (‖v x_1‖ * ‖x.ofLp x_1‖) 2 ≤ HPow.hPow (β := ℕ) (‖v‖ * ‖x‖) 2
Tactic: simp only [(T x).norm_sq_eq, ofLp_toEuclideanCLM, mulVec_diagonal, norm_mul, T]
-- 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
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n :=
  (toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v)
x : EuclideanSpace 𝕜 n
i : n
h : Membership.mem (γ := Finset n) Finset.univ i
⊢ HPow.hPow (β := ℕ) (‖v i‖ * ‖x.ofLp i‖) 2 ≤ HPow.hPow (β := ℕ) ‖v‖ 2 * HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2
have grw : HPow.hPow (β := ℕ) ‖v i‖ 2 * HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2 ≤
  HPow.hPow (β := ℕ) ‖v‖ 2 * HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2
Tactic: grw [mul_pow, norm_le_pi_norm v i]
-- 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
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n :=
  (toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v)
x : EuclideanSpace 𝕜 n
i : n
h : Membership.mem (γ := Finset n) Finset.univ i
grw :
  HPow.hPow (β := ℕ) ‖v i‖ 2 * HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2 ≤
    HPow.hPow (β := ℕ) ‖v‖ 2 * HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2
⊢ HPow.hPow (β := ℕ) (‖v i‖ * ‖x.ofLp i‖) 2 ≤ HPow.hPow (β := ℕ) ‖v‖ 2 * HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2
have grw₁ : HPow.hPow (β := ℕ) ‖v‖ 2 * HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2 ≤ HPow.hPow (β := ℕ) ‖v‖ 2 * HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2
Tactic: grw [mul_pow, norm_le_pi_norm v i]
-- 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
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n :=
  (toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v)
x : EuclideanSpace 𝕜 n
⊢ ∑ x_1 : n, HPow.hPow (β := ℕ) (‖v x_1‖ * ‖x.ofLp x_1‖) 2 ≤ HPow.hPow (β := ℕ) (‖v‖ * ‖x‖) 2
have calc : ∑ i : n, HPow.hPow (β := ℕ) ‖v‖ 2 * HPow.hPow (β := ℕ) ‖x.ofLp i‖ 2 = HPow.hPow (β := ℕ) (‖v‖ * ‖x‖) 2
Tactic: calc _ ≤ _ := Finset.sum_le_sum fun i _ ↦ by grw [mul_pow, norm_le_pi_norm v i]
      _ = _ := by simp [mul_pow, EuclideanSpace.norm_sq_eq x, Finset.mul_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
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n :=
  (toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v)
⊢ ‖v‖ ≤
    norm (E := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
      ((toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v) :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
have refine_2 : ∀ (i : n), ‖v i‖ ≤ ‖T‖
Tactic: refine (pi_norm_le_iff_of_nonneg (norm_nonneg T)).mpr fun i ↦ ?_
-- 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
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n :=
  (toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v)
i : n
⊢ ‖v i‖ =
    norm (E := EuclideanSpace 𝕜 n)
      ((T : (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n) (toLp 2 (Pi.single (M := fun (x : n) ↦ 𝕜) i 1)) :
        EuclideanSpace 𝕜 n)
have rw : ‖v i‖ = norm (E := EuclideanSpace 𝕜 n) (toLp 2 (diagonal v *ᵥ Pi.single (M := fun (a : n) ↦ 𝕜) i 1))
Tactic: rw [toEuclideanCLM_toLp (diagonal v) (Pi.single i (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
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n :=
  (toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v)
i : n
⊢ norm (E := EuclideanSpace 𝕜 n)
      ((T : (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n) (toLp 2 (Pi.single (M := fun (x : n) ↦ 𝕜) i 1)) :
        EuclideanSpace 𝕜 n) ≤
    ‖T‖
have grw : ‖T‖ * norm (E := EuclideanSpace 𝕜 n) (toLp 2 (Pi.single (M := fun (x : n) ↦ 𝕜) i 1)) ≤ ‖T‖
Tactic: grw [T.le_opNorm]
-- 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
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n :=
  (toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v)
i : n
⊢ ‖v i‖ ≤ ‖T‖
have calc : ‖v i‖ =
  norm (E := EuclideanSpace 𝕜 n)
    ((T : (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n) (toLp 2 (Pi.single (M := fun (x : n) ↦ 𝕜) i 1)) :
      EuclideanSpace 𝕜 n)
Tactic: calc _ = ‖T (toLp 2 (Pi.single i (1 : 𝕜)))‖ := by
          rw [toEuclideanCLM_toLp (diagonal v) (Pi.single i (1 : 𝕜))]
          simp
      _ ≤ _ := by grw [T.le_opNorm]; simp
-- 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
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n :=
  (toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (diagonal v)
i : n
calc :
  ‖v i‖ =
    norm (E := EuclideanSpace 𝕜 n)
      ((T : (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n) (toLp 2 (Pi.single (M := fun (x : n) ↦ 𝕜) i 1)) :
        EuclideanSpace 𝕜 n)
⊢ ‖v i‖ ≤ ‖T‖
have calc₁ : norm (E := EuclideanSpace 𝕜 n)
    ((T : (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n) (toLp 2 (Pi.single (M := fun (x : n) ↦ 𝕜) i 1)) :
      EuclideanSpace 𝕜 n) ≤
  ‖T‖
Tactic: calc _ = ‖T (toLp 2 (Pi.single i (1 : 𝕜)))‖ := by
          rw [toEuclideanCLM_toLp (diagonal v) (Pi.single i (1 : 𝕜))]
          simp
      _ ≤ _ := by grw [T.le_opNorm]; simp
-- 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
r : 𝕜
x : Matrix m n 𝕜
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖
have rw : ‖HSMul.hSMul (β := EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m) r
      ((toEuclideanLin ≪≫ₗ toContinuousLinearMap : (a : Matrix m n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m) x :
        EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m)‖ ≤
  ‖r‖ * ‖x‖
Tactic: rw [l2_opNorm_def, map_smul]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
x : A
⊢ ‖x‖ = √‖x * star x‖
have rw : HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) (√‖x * star x‖) 2
Tactic: rw [← sq_eq_sq₀ (norm_nonneg _) (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ ‖x‖ ≤ ‖x.1‖ + ‖x.2‖
have refine : HPow.hPow (β := ℕ) ‖x‖ 2 ≤ HPow.hPow (β := ℕ) (‖x.1‖ + ‖x.2‖) 2
Tactic: refine abs_le_of_sq_le_sq' ?_ (by positivity) |>.2
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ HPow.hPow (β := ℕ) ‖x.1‖ 2 + 0 + HPow.hPow (β := ℕ) ‖x.2‖ 2 ≤
    HPow.hPow (β := ℕ) ‖x.1‖ 2 + 2 * ‖x.1‖ * ‖x.2‖ + HPow.hPow (β := ℕ) ‖x.2‖ 2
have bc : 0 ≤ 2 * ‖x.1‖ * ‖x.2‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 ≤ HPow.hPow (β := ℕ) (‖x.1‖ + ‖x.2‖) 2
have calc : ‖⟪x.1, x.1⟫_A‖ + ‖⟪x.2, x.2⟫_A‖ = HPow.hPow (β := ℕ) ‖x.1‖ 2 + 0 + HPow.hPow (β := ℕ) ‖x.2‖ 2
Tactic: calc ‖x‖ ^ 2 ≤ ‖⟪x.1, x.1⟫_A‖ + ‖⟪x.2, x.2⟫_A‖ := prod_norm_sq x ▸ norm_add_le _ _
    _ = ‖x.1‖ ^ 2 + 0 + ‖x.2‖ ^ 2 := by simp [norm_sq_eq A]
    _ ≤ ‖x.1‖ ^ 2 + 2 * ‖x.1‖ * ‖x.2‖ + ‖x.2‖ ^ 2 := by gcongr; positivity
    _ = (‖x.1‖ + ‖x.2‖) ^ 2 := by ring
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
x : C⋆ᵐᵒᵈ(A, E × F)
calc : ‖⟪x.1, x.1⟫_A‖ + ‖⟪x.2, x.2⟫_A‖ = HPow.hPow (β := ℕ) ‖x.1‖ 2 + 0 + HPow.hPow (β := ℕ) ‖x.2‖ 2
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 ≤ HPow.hPow (β := ℕ) (‖x.1‖ + ‖x.2‖) 2
have calc₁ : HPow.hPow (β := ℕ) ‖x.1‖ 2 + 0 + HPow.hPow (β := ℕ) ‖x.2‖ 2 ≤
  HPow.hPow (β := ℕ) ‖x.1‖ 2 + 2 * ‖x.1‖ * ‖x.2‖ + HPow.hPow (β := ℕ) ‖x.2‖ 2
Tactic: calc ‖x‖ ^ 2 ≤ ‖⟪x.1, x.1⟫_A‖ + ‖⟪x.2, x.2⟫_A‖ := prod_norm_sq x ▸ norm_add_le _ _
    _ = ‖x.1‖ ^ 2 + 0 + ‖x.2‖ ^ 2 := by simp [norm_sq_eq A]
    _ ≤ ‖x.1‖ ^ 2 + 2 * ‖x.1‖ * ‖x.2‖ + ‖x.2‖ ^ 2 := by gcongr; positivity
    _ = (‖x.1‖ + ‖x.2‖) ^ 2 := by ring
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
x : C⋆ᵐᵒᵈ(A, E × F)
calc : ‖⟪x.1, x.1⟫_A‖ + ‖⟪x.2, x.2⟫_A‖ = HPow.hPow (β := ℕ) ‖x.1‖ 2 + 0 + HPow.hPow (β := ℕ) ‖x.2‖ 2
calc₁ :
  HPow.hPow (β := ℕ) ‖x.1‖ 2 + 0 + HPow.hPow (β := ℕ) ‖x.2‖ 2 ≤
    HPow.hPow (β := ℕ) ‖x.1‖ 2 + 2 * ‖x.1‖ * ‖x.2‖ + HPow.hPow (β := ℕ) ‖x.2‖ 2
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 ≤ HPow.hPow (β := ℕ) (‖x.1‖ + ‖x.2‖) 2
have calc₂ : HPow.hPow (β := ℕ) ‖x.1‖ 2 + 2 * ‖x.1‖ * ‖x.2‖ + HPow.hPow (β := ℕ) ‖x.2‖ 2 = HPow.hPow (β := ℕ) (‖x.1‖ + ‖x.2‖) 2
Tactic: calc ‖x‖ ^ 2 ≤ ‖⟪x.1, x.1⟫_A‖ + ‖⟪x.2, x.2⟫_A‖ := prod_norm_sq x ▸ norm_add_le _ _
    _ = ‖x.1‖ ^ 2 + 0 + ‖x.2‖ ^ 2 := by simp [norm_sq_eq A]
    _ ≤ ‖x.1‖ ^ 2 + 2 * ‖x.1‖ * ‖x.2‖ + ‖x.2‖ ^ 2 := by gcongr; positivity
    _ = (‖x.1‖ + ‖x.2‖) ^ 2 := by ring
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ ⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A = 0 ↔ x = 0
have refine : ∀ (h : ⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A = 0), x = 0
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Module.Constructions (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
E : Type u_2
F : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : NormedAddCommGroup F
inst_6 : Module ℂ F
inst_7 : SMul A F
inst_8 : CStarModule A E
inst_9 : CStarModule A F
inst_10 : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
h : ⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A = 0
⊢ x = 0
have a : Eq (α := E × F) ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) x : E × F)
  ((equiv A (E × F) : (a : C⋆ᵐᵒᵈ(A, E × F)) → E × F) 0 : E × F)
Tactic: apply equiv A (E × F) |>.injective