awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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
⊢ 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:
simp [h]
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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
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
⊢ 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))

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]

Premises used: norm_eq_zero, CStarMatrix.zero_apply, sq, CStarRing.norm_star_mul_self, injective_iff_map_eq_zero, CStarMatrix.toCLM_apply_single_apply, sq_eq_zero_iff
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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
inst_5 : DecidableEq m
inst_6 : DecidableEq n
M : CStarMatrix m n A
i : m
j : n
a b : A
⊢ a * M i j * star b =
    inner A (E := C⋆ᵐᵒᵈ(A, (j : n) → A))
      ((Equiv.symm (equiv A ((j : n) → A)) : (a : (j : n) → A) → C⋆ᵐᵒᵈ(A, (j : n) → A))
          (Pi.single (M := fun (j : n) ↦ A) j b) :
        C⋆ᵐᵒᵈ(A, (j : 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))

Tactic:
simp [mul_assoc, inner_def]

Premises used: WithCStarModule.inner_def, mul_assoc
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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)
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))
⊢ ⟪(((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

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]

Premises used: Finset.mul_sum, WithCStarModule.inner_def, star_star, star_sum, CStarMatrix.toCLM_apply_eq_sum, WithCStarModule.pi_inner, Matrix.conjTranspose_apply, StarMul.star_mul, WithCStarModule.equiv_symm_pi_apply, Finset.sum_mul
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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)
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))
⊢ 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:
rw [Finset.sum_comm]

Premises used: Finset.sum_comm
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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) (∑ 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:
simp_rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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)
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
⊢ ⟪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

Tactic:
apply Eq.symm

Premises used: Eq.symm
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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)
⊢ ⟪(((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:
simpa using inner_toCLM_conjTranspose_left (M := Mᴴ) (v := v) (w := w)

Premises used: CStarMatrix.inner_toCLM_conjTranspose_left
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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
⊢ ‖M‖ =
    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:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
n : Type u_2
A : Type u_5
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
inst_3 : Fintype n
M : CStarMatrix n n A
⊢ ‖M‖ =
    norm (E := (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))ᵐᵒᵖ)
      ((toCLMNonUnitalAlgHom : (a : CStarMatrix n n A) → (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))ᵐᵒᵖ) M :
        (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))ᵐᵒᵖ)

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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
rw : NormSMulClass ℂ (C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
⊢ ‖c • M‖ = ‖c‖ * ‖M‖

Tactic:
rw [norm_def, norm_def, map_smul, norm_smul _ (toCLM M)]

Premises used: norm_smul, CStarMatrix.toCLM, DFunLike.coe, map_smul, CStarMatrix.norm_def
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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₁ M₂ : CStarMatrix m n A
⊢ ‖M₁ + M₂‖ ≤ ‖M₁‖ + ‖M₂‖

Tactic:
simpa [← map_add] using norm_add_le (toCLM M₁) (toCLM M₂)

Premises used: CStarMatrix.toCLM, map_add, norm_add_le, DFunLike.coe
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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‖
inr : ∀ (h : 0 < ‖M i j‖), ‖M i j‖ ≤ ‖M‖
⊢ ‖M i j‖ ≤ ‖M‖

Tactic:
obtain (h | h) := eq_zero_or_norm_pos (M i j)

Premises used: eq_zero_or_norm_pos
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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
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))
⊢ ‖M i j‖ ≤ ‖M‖

Tactic:
simp [h, norm_def]

Premises used: CStarMatrix.norm_def
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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 : 0 < ‖M i j‖
⊢ ‖M i j‖ ≤ ‖M‖

Tactic:
le_of_mul_le_mul_right this h

Premises used: le_of_mul_le_mul_right
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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 : 0 < ‖M i j‖
⊢ ‖M i j‖ ≤ ‖M‖

Tactic:
exact le_of_mul_le_mul_right this h

Premises used: le_of_mul_le_mul_right
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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 : ‖M i j‖ * ‖M i j‖ ≤ ‖M‖ * ‖M i j‖
⊢ ‖M i j‖ ≤ ‖M‖

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
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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
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‖
⊢ ‖M i j‖ * ‖M i j‖ ≤ ‖M‖ * ‖M i j‖

Tactic:
rw [← CStarRing.norm_star_mul_self, ← toCLM_apply_single_apply]

Premises used: CStarRing.norm_star_mul_self, CStarMatrix.toCLM_apply_single_apply
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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
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‖
⊢ 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:
apply norm_apply_le_norm _ _ |>.trans

Premises used: WithCStarModule.norm_apply_le_norm, LE.le.trans
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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
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‖
⊢ 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 (toCLM M).le_opNorm _ |>.trans

Premises used: ContinuousLinearMap.le_opNorm, CStarMatrix.toCLM, LE.le.trans, DFunLike.coe
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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, 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:
simp [norm_def]

Premises used: CStarMatrix.norm_def
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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‖
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‖
⊢ ‖M i j‖ ≤ ‖M‖

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]

Premises used: ContinuousLinearMap.le_opNorm, CStarMatrix.toCLM, WithCStarModule.norm_apply_le_norm, CStarRing.norm_star_mul_self, LE.le.trans, DFunLike.coe, CStarMatrix.norm_def, CStarMatrix.toCLM_apply_single_apply
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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‖
⊢ 0 ≤ (↑C : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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‖
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‖
⊢ ‖M‖ ≤ (↑C : ℝ)

Tactic:
refine (toCLM M).opNorm_le_bound (by simp) fun v ↦ ?_

Premises used: CStarMatrix.toCLM, ContinuousLinearMap.opNorm_le_bound, DFunLike.coe
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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‖
v : C⋆ᵐᵒᵈ(A, m → A)
inl :
  ∀
    (h₀ :
      0 =
        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))),
    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‖
inr :
  ∀
    (h₀ :
      0 <
        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))),
    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‖
⊢ 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:
obtain (h₀ | h₀) := (norm_nonneg (toCLM M v)).eq_or_lt

Premises used: LE.le.eq_or_lt, CStarMatrix.toCLM, DFunLike.coe, norm_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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‖
v : C⋆ᵐᵒᵈ(A, m → A)
h₀ :
  0 =
    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))
inl : 0 ≤ (↑C : ℝ) * ‖v‖
⊢ 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:
rw [← h₀]