awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
inst_2 : Fintype n
x y : CStarMatrix n n A
⊢ (toCLM : (a : CStarMatrix n n A) → C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) (x * y) =
    HMul.hMul (α := C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) (β := C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
      ((toCLM : (a : CStarMatrix n n A) → C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) y :
        C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
      ((toCLM : (a : CStarMatrix n n A) → C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) x :
        C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
have h : ∀ (x_1 : C⋆ᵐᵒᵈ(A, n → A)) (i : n),
  Eq.{u_5 + 1} (α := A)
    ((((toCLM : (a : CStarMatrix n n A) → C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) (x * y) :
            C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
          (a : C⋆ᵐᵒᵈ(A, n → A)) → C⋆ᵐᵒᵈ(A, n → A))
        x_1 i :
      A)
    ((HMul.hMul (α := C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) (β := C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
            ((toCLM : (a : CStarMatrix n n A) → C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) y :
              C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
            ((toCLM : (a : CStarMatrix n n A) → C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) x :
              C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
          (a : C⋆ᵐᵒᵈ(A, n → A)) → C⋆ᵐᵒᵈ(A, n → A))
        x_1 i :
      A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
inst_2 : DecidableEq m
M : CStarMatrix m n A
i : m
a : A
⊢ Eq (α := C⋆ᵐᵒᵈ(A, n → A))
    ((((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
            C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
          (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
        ((Equiv.symm (equiv A (m → A)) : (a : m → A) → C⋆ᵐᵒᵈ(A, m → A)) (Pi.single (M := fun (a : m) ↦ A) i a)) :
      C⋆ᵐᵒᵈ(A, n → A))
    ((Equiv.symm (equiv A ((j : n) → A)) : (a : (j : n) → A) → C⋆ᵐᵒᵈ(A, (j : n) → A)) fun (j : n) ↦ a * M i j :
      C⋆ᵐᵒᵈ(A, (j : n) → A))
have h : ∀ (i_1 : n),
  Eq.{u_5 + 1} (α := A)
    ((((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
            C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
          (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
        ((Equiv.symm (equiv A (m → A)) : (a : m → A) → C⋆ᵐᵒᵈ(A, m → A)) (Pi.single (M := fun (a : m) ↦ A) i a)) i_1 :
      A)
    ((Equiv.symm (equiv A ((j : n) → A)) : (a : (j : n) → A) → C⋆ᵐᵒᵈ(A, (j : n) → A)) (fun (j : n) ↦ a * M i j) i_1 : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
⊢ Function.Injective (α := CStarMatrix m n A) (β := C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
    (⇑toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
have rw : ∀ (a : CStarMatrix m n A),
  Eq (α := C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
      ((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) a :
        C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
      (0 : C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) →
    a = 0
Tactic: rw [injective_iff_map_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
M : CStarMatrix m n A
h :
  Eq (α := C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
    ((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
      C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
    (0 : C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
⊢ M = 0
have h₁ : ∀ (i : m) (j : n), M i j = 0 i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
M : CStarMatrix m n A
h :
  Eq (α := C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
    ((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
      C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
    (0 : C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
i : m
j : n
⊢ M i j = 0 i j
have h₁ : norm.{u_5} (E := A)
    ((((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
            C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
          (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
        ((Equiv.symm (WithCStarModule.equiv A (m → A)) : (a : m → A) → C⋆ᵐᵒᵈ(A, m → A))
          (Pi.single (M := fun (a : m) ↦ A) i (star (M i j))))
        j :
      A) =
  0
Tactic: rw [zero_apply, ← norm_eq_zero, ← sq_eq_zero_iff, sq, ← CStarRing.norm_star_mul_self,
    ← toCLM_apply_single_apply]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
⊢ Function.Injective (α := CStarMatrix m n A) (β := C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
    (⇑toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
have rw : ∀ (a : CStarMatrix m n A),
  Eq (α := C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
      ((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) a :
        C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
      (0 : C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) →
    a = 0
Tactic: classical
  rw [injective_iff_map_eq_zero]
  intro M h
  ext i j
  rw [zero_apply, ← norm_eq_zero, ← sq_eq_zero_iff, sq, ← CStarRing.norm_star_mul_self,
    ← toCLM_apply_single_apply]
  simp [h]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
rw rw₁ rw₂ rw₃ :
  ∀ (M : CStarMatrix m n A)
    (h :
      Eq (α := C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
        ((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
          C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
        (0 : C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))),
    M = 0
⊢ Function.Injective (α := CStarMatrix m n A) (β := C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
    (⇑toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
have h : ∀ (M : CStarMatrix m n A)
  (h :
    Eq (α := C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
      ((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
        C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
      (0 : C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)))
  (i : m) (j : n), M i j = 0 i j
Tactic: classical
  rw [injective_iff_map_eq_zero]
  intro M h
  ext i j
  rw [zero_apply, ← norm_eq_zero, ← sq_eq_zero_iff, sq, ← CStarRing.norm_star_mul_self,
    ← toCLM_apply_single_apply]
  simp [h]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
rw rw₁ rw₂ rw₃ :
  ∀ (M : CStarMatrix m n A)
    (h :
      Eq (α := C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
        ((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
          C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
        (0 : C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))),
    M = 0
h :
  ∀ (M : CStarMatrix m n A)
    (h :
      Eq (α := C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
        ((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
          C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
        (0 : C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)))
    (i : m) (j : n), M i j = 0 i j
⊢ Function.Injective (α := CStarMatrix m n A) (β := C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
    (⇑toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
have h₁ : ∀ (M : CStarMatrix m n A)
  (h :
    Eq (α := C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
      ((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
        C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
      (0 : C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)))
  (i : m) (j : n),
  norm.{u_5} (E := A)
      ((((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
              C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
            (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
          ((Equiv.symm (WithCStarModule.equiv A (m → A)) : (a : m → A) → C⋆ᵐᵒᵈ(A, m → A))
            (Pi.single (M := fun (a : m) ↦ A) i (star (M i j))))
          j :
        A) =
    0
Tactic: classical
  rw [injective_iff_map_eq_zero]
  intro M h
  ext i j
  rw [zero_apply, ← norm_eq_zero, ← sq_eq_zero_iff, sq, ← CStarRing.norm_star_mul_self,
    ← toCLM_apply_single_apply]
  simp [h]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
inst_2 : PartialOrder A
inst_3 : StarOrderedRing A
inst_4 : Fintype n
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ(A, n → A)
w : C⋆ᵐᵒᵈ(A, m → A)
⊢ ⟪(((toCLM : (a : CStarMatrix n m A) → C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, m → A)) Mᴴ :
            C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, m → A)) :
          (a : C⋆ᵐᵒᵈ(A, n → A)) → C⋆ᵐᵒᵈ(A, m → A))
        v,
      w⟫_A =
    ⟪v,
      (((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
            C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
          (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
        w⟫_A
have simp : Eq.{u_5 + 1} (α := A) (∑ x : m, ∑ i : n, w x * (M x i * star (v i))) (∑ x : n, ∑ i : m, w i * M i x * star (v x))
Tactic: simp only [toCLM_apply_eq_sum, pi_inner, equiv_symm_pi_apply, inner_def, Finset.mul_sum,
    Matrix.conjTranspose_apply, star_sum, star_mul, star_star, Finset.sum_mul]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
inst_2 : PartialOrder A
inst_3 : StarOrderedRing A
inst_4 : Fintype n
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ(A, n → A)
w : C⋆ᵐᵒᵈ(A, m → A)
⊢ Eq.{u_5 + 1} (α := A) (∑ x : m, ∑ i : n, w x * (M x i * star (v i))) (∑ x : n, ∑ i : m, w i * M i x * star (v x))
have rw : Eq.{u_5 + 1} (α := A) (∑ y : n, ∑ x : m, w x * (M x y * star (v y))) (∑ x : n, ∑ i : m, w i * M i x * star (v x))
Tactic: rw [Finset.sum_comm]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
inst_2 : PartialOrder A
inst_3 : StarOrderedRing A
inst_4 : Fintype n
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ(A, m → A)
w : C⋆ᵐᵒᵈ(A, n → A)
⊢ ⟪v,
      (((toCLM : (a : CStarMatrix n m A) → C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, m → A)) Mᴴ :
            C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, m → A)) :
          (a : C⋆ᵐᵒᵈ(A, n → A)) → C⋆ᵐᵒᵈ(A, m → A))
        w⟫_A =
    ⟪(((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
            C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
          (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
        v,
      w⟫_A
have h : ⟪(((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
          C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
        (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
      v,
    w⟫_A =
  ⟪v,
    (((toCLM : (a : CStarMatrix n m A) → C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, m → A)) Mᴴ :
          C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, m → A)) :
        (a : C⋆ᵐᵒᵈ(A, n → A)) → C⋆ᵐᵒᵈ(A, m → A))
      w⟫_A
Tactic: apply Eq.symm
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
inst_2 : PartialOrder A
inst_3 : StarOrderedRing A
inst_4 : Fintype n
c : ℂ
M : CStarMatrix m n A
⊢ ‖c • M‖ = ‖c‖ * ‖M‖
have rw : NormSMulClass ℂ (C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
Tactic: rw [norm_def, norm_def, map_smul, norm_smul _ (toCLM M)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
inst_2 : PartialOrder A
inst_3 : StarOrderedRing A
inst_4 : Fintype n
M : CStarMatrix m n A
i : m
j : n
this : ‖M i j‖ * ‖M i j‖ ≤ ‖M‖ * ‖M i j‖
⊢ ‖M i j‖ ≤ ‖M‖
have inl : ∀ (h : M i j = 0), ‖M i j‖ ≤ ‖M‖
Tactic: obtain (h | h) := eq_zero_or_norm_pos (M i j)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
inst_2 : PartialOrder A
inst_3 : StarOrderedRing A
inst_4 : Fintype n
M : CStarMatrix m n A
i : m
j : n
this : ‖M i j‖ * ‖M i j‖ ≤ ‖M‖ * ‖M i j‖
inl : ∀ (h : M i j = 0), ‖M i j‖ ≤ ‖M‖
⊢ ‖M i j‖ ≤ ‖M‖
have inr : ∀ (h : 0 < ‖M i j‖), ‖M i j‖ ≤ ‖M‖
Tactic: obtain (h | h) := eq_zero_or_norm_pos (M i j)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
inst_2 : PartialOrder A
inst_3 : StarOrderedRing A
inst_4 : Fintype n
M : CStarMatrix m n A
i : m
j : n
this : ‖M i j‖ * ‖M i j‖ ≤ ‖M‖ * ‖M i j‖
h : M i j = 0
⊢ ‖M i j‖ ≤ ‖M‖
have inl : 0 ≤
  norm (E := C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
    ((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
      C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
Tactic: simp [h, norm_def]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
inst_2 : PartialOrder A
inst_3 : StarOrderedRing A
inst_4 : Fintype n
M : CStarMatrix m n A
i : m
j : n
⊢ ‖M i j‖ ≤ ‖M‖
have suffices : ‖M i j‖ * ‖M i j‖ ≤ ‖M‖ * ‖M i j‖
Tactic: suffices ‖M i j‖ * ‖M i j‖ ≤ ‖M‖ * ‖M i j‖ by
    obtain (h | h) := eq_zero_or_norm_pos (M i j)
    · simp [h, norm_def]
    · exact le_of_mul_le_mul_right this h
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
inst_2 : PartialOrder A
inst_3 : StarOrderedRing A
inst_4 : Fintype n
M : CStarMatrix m n A
i : m
j : n
⊢ ‖M i j‖ * ‖M i j‖ ≤ ‖M‖ * ‖M i j‖
have rw : norm.{u_5} (E := A)
    ((((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
            C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
          (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
        ((Equiv.symm (equiv A (m → A)) : (a : m → A) → C⋆ᵐᵒᵈ(A, m → A))
          (Pi.single (M := fun (a : m) ↦ A) i (star (M i j))))
        j :
      A) ≤
  ‖M‖ * ‖M i j‖
Tactic: rw [← CStarRing.norm_star_mul_self, ← toCLM_apply_single_apply]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
inst_2 : PartialOrder A
inst_3 : StarOrderedRing A
inst_4 : Fintype n
M : CStarMatrix m n A
i : m
j : n
⊢ norm.{u_5} (E := A)
      ((((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
              C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
            (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
          ((Equiv.symm (equiv A (m → A)) : (a : m → A) → C⋆ᵐᵒᵈ(A, m → A))
            (Pi.single (M := fun (a : m) ↦ A) i (star (M i j))))
          j :
        A) ≤
    ‖M‖ * ‖M i j‖
have apply : norm (E := C⋆ᵐᵒᵈ(A, (i : n) → A))
    ((((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
            C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
          (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
        ((Equiv.symm (equiv A (m → A)) : (a : m → A) → C⋆ᵐᵒᵈ(A, m → A))
          (Pi.single (M := fun (a : m) ↦ A) i (star (M i j)))) :
      C⋆ᵐᵒᵈ(A, n → A)) ≤
  ‖M‖ * ‖M i j‖
Tactic: apply norm_apply_le_norm _ _ |>.trans
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
inst_2 : PartialOrder A
inst_3 : StarOrderedRing A
inst_4 : Fintype n
M : CStarMatrix m n A
i : m
j : n
⊢ norm (E := C⋆ᵐᵒᵈ(A, (i : n) → A))
      ((((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
              C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
            (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
          ((Equiv.symm (equiv A (m → A)) : (a : m → A) → C⋆ᵐᵒᵈ(A, m → A))
            (Pi.single (M := fun (a : m) ↦ A) i (star (M i j)))) :
        C⋆ᵐᵒᵈ(A, n → A)) ≤
    ‖M‖ * ‖M i j‖
have apply : norm (E := C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
      ((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
        C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) *
    norm (E := C⋆ᵐᵒᵈ(A, m → A))
      ((Equiv.symm (equiv A (m → A)) : (a : m → A) → C⋆ᵐᵒᵈ(A, m → A))
          (Pi.single (M := fun (a : m) ↦ A) i (star (M i j))) :
        C⋆ᵐᵒᵈ(A, m → A)) ≤
  ‖M‖ * ‖M i j‖
Tactic: apply (toCLM M).le_opNorm _ |>.trans
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
inst_2 : PartialOrder A
inst_3 : StarOrderedRing A
inst_4 : Fintype n
M : CStarMatrix m n A
i : m
j : n
⊢ ‖M i j‖ ≤ ‖M‖
have suffices : ‖M i j‖ * ‖M i j‖ ≤ ‖M‖ * ‖M i j‖
Tactic: classical
  suffices ‖M i j‖ * ‖M i j‖ ≤ ‖M‖ * ‖M i j‖ by
    obtain (h | h) := eq_zero_or_norm_pos (M i j)
    · simp [h, norm_def]
    · exact le_of_mul_le_mul_right this h
  rw [← CStarRing.norm_star_mul_self, ← toCLM_apply_single_apply]
  apply norm_apply_le_norm _ _ |>.trans
  apply (toCLM M).le_opNorm _ |>.trans
  simp [norm_def]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
inst_2 : PartialOrder A
inst_3 : StarOrderedRing A
inst_4 : Fintype n
M : CStarMatrix m n A
i : m
j : n
suffices suffices₁ suffices₂ : ‖M i j‖ * ‖M i j‖ ≤ ‖M‖ * ‖M i j‖
⊢ ‖M i j‖ ≤ ‖M‖
have suffices₃ : norm.{u_5} (E := A)
    ((((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
            C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
          (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
        ((Equiv.symm (equiv A (m → A)) : (a : m → A) → C⋆ᵐᵒᵈ(A, m → A))
          (Pi.single (M := fun (a : m) ↦ A) i (star (M i j))))
        j :
      A) ≤
  ‖M‖ * ‖M i j‖
Tactic: classical
  suffices ‖M i j‖ * ‖M i j‖ ≤ ‖M‖ * ‖M i j‖ by
    obtain (h | h) := eq_zero_or_norm_pos (M i j)
    · simp [h, norm_def]
    · exact le_of_mul_le_mul_right this h
  rw [← CStarRing.norm_star_mul_self, ← toCLM_apply_single_apply]
  apply norm_apply_le_norm _ _ |>.trans
  apply (toCLM M).le_opNorm _ |>.trans
  simp [norm_def]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
inst_2 : PartialOrder A
inst_3 : StarOrderedRing A
inst_4 : Fintype n
M : CStarMatrix m n A
i : m
j : n
suffices suffices₁ suffices₂ : ‖M i j‖ * ‖M i j‖ ≤ ‖M‖ * ‖M i j‖
suffices₃ :
  norm.{u_5} (E := A)
      ((((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
              C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
            (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
          ((Equiv.symm (equiv A (m → A)) : (a : m → A) → C⋆ᵐᵒᵈ(A, m → A))
            (Pi.single (M := fun (a : m) ↦ A) i (star (M i j))))
          j :
        A) ≤
    ‖M‖ * ‖M i j‖
⊢ ‖M i j‖ ≤ ‖M‖
have suffices₄ : norm (E := C⋆ᵐᵒᵈ(A, (i : n) → A))
    ((((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
            C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
          (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
        ((Equiv.symm (equiv A (m → A)) : (a : m → A) → C⋆ᵐᵒᵈ(A, m → A))
          (Pi.single (M := fun (a : m) ↦ A) i (star (M i j)))) :
      C⋆ᵐᵒᵈ(A, n → A)) ≤
  ‖M‖ * ‖M i j‖
Tactic: classical
  suffices ‖M i j‖ * ‖M i j‖ ≤ ‖M‖ * ‖M i j‖ by
    obtain (h | h) := eq_zero_or_norm_pos (M i j)
    · simp [h, norm_def]
    · exact le_of_mul_le_mul_right this h
  rw [← CStarRing.norm_star_mul_self, ← toCLM_apply_single_apply]
  apply norm_apply_le_norm _ _ |>.trans
  apply (toCLM M).le_opNorm _ |>.trans
  simp [norm_def]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
inst_2 : PartialOrder A
inst_3 : StarOrderedRing A
inst_4 : Fintype n
M : CStarMatrix m n A
i : m
j : n
suffices suffices₁ suffices₂ : ‖M i j‖ * ‖M i j‖ ≤ ‖M‖ * ‖M i j‖
suffices₃ :
  norm.{u_5} (E := A)
      ((((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
              C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
            (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
          ((Equiv.symm (equiv A (m → A)) : (a : m → A) → C⋆ᵐᵒᵈ(A, m → A))
            (Pi.single (M := fun (a : m) ↦ A) i (star (M i j))))
          j :
        A) ≤
    ‖M‖ * ‖M i j‖
suffices₄ :
  norm (E := C⋆ᵐᵒᵈ(A, (i : n) → A))
      ((((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
              C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
            (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
          ((Equiv.symm (equiv A (m → A)) : (a : m → A) → C⋆ᵐᵒᵈ(A, m → A))
            (Pi.single (M := fun (a : m) ↦ A) i (star (M i j)))) :
        C⋆ᵐᵒᵈ(A, n → A)) ≤
    ‖M‖ * ‖M i j‖
⊢ ‖M i j‖ ≤ ‖M‖
have suffices₅ : norm (E := C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
      ((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
        C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) *
    norm (E := C⋆ᵐᵒᵈ(A, m → A))
      ((Equiv.symm (equiv A (m → A)) : (a : m → A) → C⋆ᵐᵒᵈ(A, m → A))
          (Pi.single (M := fun (a : m) ↦ A) i (star (M i j))) :
        C⋆ᵐᵒᵈ(A, m → A)) ≤
  ‖M‖ * ‖M i j‖
Tactic: classical
  suffices ‖M i j‖ * ‖M i j‖ ≤ ‖M‖ * ‖M i j‖ by
    obtain (h | h) := eq_zero_or_norm_pos (M i j)
    · simp [h, norm_def]
    · exact le_of_mul_le_mul_right this h
  rw [← CStarRing.norm_star_mul_self, ← toCLM_apply_single_apply]
  apply norm_apply_le_norm _ _ |>.trans
  apply (toCLM M).le_opNorm _ |>.trans
  simp [norm_def]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
inst_2 : PartialOrder A
inst_3 : StarOrderedRing A
inst_4 : Fintype n
M : CStarMatrix m n A
C : ℝ≥0
h :
  ∀ (v : C⋆ᵐᵒᵈ(A, m → A)) (w : C⋆ᵐᵒᵈ(A, n → A)),
    ‖⟪w,
          (((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
                C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
              (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
            v⟫_A‖ ≤
      (↑C : ℝ) * ‖v‖ * ‖w‖
⊢ ‖M‖ ≤ (↑C : ℝ)
have refine : ∀ (v : C⋆ᵐᵒᵈ(A, m → A)),
  Norm.norm (E := C⋆ᵐᵒᵈ(A, n → A))
      ((((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
              C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
            (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
          v :
        C⋆ᵐᵒᵈ(A, n → A)) ≤
    (↑C : ℝ) * ‖v‖
Tactic: refine (toCLM M).opNorm_le_bound (by simp) fun v ↦ ?_