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
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))
⊢ 0 ≤ (↑C : ℝ) * ‖v‖

Tactic:
positivity
-- 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))
⊢ 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:
le_of_mul_le_mul_right ?_ 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
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))
inr :
  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))
⊢ 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 le_of_mul_le_mul_right ?_ 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
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))
⊢ 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))

Tactic:
simpa [← sq, norm_sq_eq A] using h ..

Premises used: sq, CStarModule.norm_sq_eq
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalCStarAlgebra A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
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

Tactic:
CStarMatrix.norm_le_of_forall_inner_le fun v w => h v w

Premises used: CStarMatrix.norm_le_of_forall_inner_le, NNReal.toReal
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalCStarAlgebra A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
⊢ LipschitzWith (α := CStarMatrix m n A) (β := Matrix m n A) 1
    (⇑(LinearEquiv.symm ofMatrixₗ) : (a : CStarMatrix m n A) → Matrix m n A)

Tactic:
AddMonoidHomClass.lipschitz_of_bound_nnnorm _ _ fun M => ?_

Premises used: AddMonoidHomClass.lipschitz_of_bound_nnnorm
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalCStarAlgebra A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
refine :
  ∀ (M : CStarMatrix m n A),
    nnnorm (E := Matrix m n A)
        ((LinearEquiv.symm ofMatrixₗ : (a : CStarMatrix m n A) → Matrix m n A) M : Matrix m n A) ≤
      1 * ‖M‖₊
⊢ LipschitzWith (α := CStarMatrix m n A) (β := Matrix m n A) 1
    (⇑(LinearEquiv.symm ofMatrixₗ) : (a : CStarMatrix m n A) → Matrix m n A)

Tactic:
refine AddMonoidHomClass.lipschitz_of_bound_nnnorm _ _ fun M => ?_

Premises used: AddMonoidHomClass.lipschitz_of_bound_nnnorm
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalCStarAlgebra A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
M : CStarMatrix m n A
rw :
  ∀ (i : m) (j : n),
    norm.{u_3} (E := A) ((LinearEquiv.symm ofMatrixₗ : (a : CStarMatrix m n A) → Matrix m n A) M i j : A) ≤ ‖M‖
⊢ nnnorm (E := Matrix m n A) ((LinearEquiv.symm ofMatrixₗ : (a : CStarMatrix m n A) → Matrix m n A) M : Matrix m n A) ≤
    1 * ‖M‖₊

Tactic:
rw [one_mul, ← NNReal.coe_le_coe, coe_nnnorm, coe_nnnorm, Matrix.norm_le_iff (norm_nonneg _)]

Premises used: Matrix.norm_le_iff, coe_nnnorm, NNReal.coe_le_coe, norm_nonneg, one_mul
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalCStarAlgebra A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
M : CStarMatrix m n A
⊢ ∀ (i : m) (j : n),
    norm.{u_3} (E := A) ((LinearEquiv.symm ofMatrixₗ : (a : CStarMatrix m n A) → Matrix m n A) M i j : A) ≤ ‖M‖

Tactic:
fun _ _ ↦ CStarMatrix.norm_entry_le_norm

Premises used: CStarMatrix.norm_entry_le_norm
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalCStarAlgebra A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
M : CStarMatrix m n A
⊢ ∀ (i : m) (j : n),
    norm.{u_3} (E := A) ((LinearEquiv.symm ofMatrixₗ : (a : CStarMatrix m n A) → Matrix m n A) M i j : A) ≤ ‖M‖

Tactic:
exact fun _ _ ↦ CStarMatrix.norm_entry_le_norm

Premises used: CStarMatrix.norm_entry_le_norm
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalCStarAlgebra A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
⊢ AntilipschitzWith (α := CStarMatrix m n A) (β := Matrix m n A)
    (HMul.hMul (α := ℝ≥0) (↑(Fintype.card n) : ℝ≥0) (↑(Fintype.card m) : ℝ≥0))
    (⇑(LinearEquiv.symm ofMatrixₗ) : (a : CStarMatrix m n A) → Matrix m n A)

Tactic:
AddMonoidHomClass.antilipschitz_of_bound _ fun M => ?_

Premises used: AddMonoidHomClass.antilipschitz_of_bound
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalCStarAlgebra A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
refine :
  ∀ (M : CStarMatrix m n A),
    ‖M‖ ≤
      (↑(HMul.hMul (α := ℝ≥0) (↑(Fintype.card n) : ℝ≥0) (↑(Fintype.card m) : ℝ≥0)) : ℝ) *
        norm (E := Matrix m n A)
          ((LinearEquiv.symm ofMatrixₗ : (a : CStarMatrix m n A) → Matrix m n A) M : Matrix m n A)
⊢ AntilipschitzWith (α := CStarMatrix m n A) (β := Matrix m n A)
    (HMul.hMul (α := ℝ≥0) (↑(Fintype.card n) : ℝ≥0) (↑(Fintype.card m) : ℝ≥0))
    (⇑(LinearEquiv.symm ofMatrixₗ) : (a : CStarMatrix m n A) → Matrix m n A)

Tactic:
refine AddMonoidHomClass.antilipschitz_of_bound _ fun M => ?_

Premises used: AddMonoidHomClass.antilipschitz_of_bound
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalCStarAlgebra A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
M : CStarMatrix m n A
⊢ LE.le (α := ℝ) 0 (∑ j : n, ∑ i : m, ‖M i j‖)

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalCStarAlgebra A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
M : CStarMatrix m n A
refine :
  ∀ (v : C⋆ᵐᵒᵈ(A, m → A)),
    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)) ≤
      (∑ j : n, ∑ i : m, ‖M i j‖) * ‖v‖
⊢ 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)) ≤
    ∑ j : n, ∑ i : m, ‖M i j‖

Tactic:
refine (toCLM M).opNorm_le_bound (by positivity) 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_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalCStarAlgebra A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ(A, m → A)
simp :
  norm (E := C⋆ᵐᵒᵈ(A, n → A))
      ((Equiv.symm (equiv A ((j : n) → A)) : (a : (j : n) → A) → C⋆ᵐᵒᵈ(A, (j : n) → A)) fun (j : n) ↦
        ∑ i : m, v i * M i j) ≤
    ∑ x : n, ∑ i : m, ‖M i x‖ * ‖v‖
⊢ 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)) ≤
    (∑ j : n, ∑ i : m, ‖M i j‖) * ‖v‖

Tactic:
simp only [toCLM_apply_eq_sum, Finset.sum_mul]

Premises used: CStarMatrix.toCLM_apply_eq_sum, Finset.sum_mul
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalCStarAlgebra A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ(A, m → A)
apply :
  LE.le (α := ℝ)
    (∑ i : n,
      norm.{u_3} (E := A)
        ((Equiv.symm (equiv A ((j : n) → A)) : (a : (j : n) → A) → C⋆ᵐᵒᵈ(A, (j : n) → A))
            (fun (j : n) ↦ ∑ i : m, v i * M i j) i :
          A))
    (∑ x : n, ∑ i : m, ‖M i x‖ * ‖v‖)
⊢ norm (E := C⋆ᵐᵒᵈ(A, n → A))
      ((Equiv.symm (equiv A ((j : n) → A)) : (a : (j : n) → A) → C⋆ᵐᵒᵈ(A, (j : n) → A)) fun (j : n) ↦
        ∑ i : m, v i * M i j) ≤
    ∑ x : n, ∑ i : m, ‖M i x‖ * ‖v‖

Tactic:
apply pi_norm_le_sum_norm _ |>.trans

Premises used: WithCStarModule.pi_norm_le_sum_norm, LE.le.trans
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalCStarAlgebra A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ(A, m → A)
h :
  ∀ (i : n),
    Membership.mem (γ := Finset n) Finset.univ i →
      norm.{u_3} (E := A)
          ((Equiv.symm (equiv A ((j : n) → A)) : (a : (j : n) → A) → C⋆ᵐᵒᵈ(A, (j : n) → A))
              (fun (j : n) ↦ ∑ i : m, v i * M i j) i :
            A) ≤
        ∑ i_1 : m, ‖M i_1 i‖ * ‖v‖
⊢ LE.le (α := ℝ)
    (∑ i : n,
      norm.{u_3} (E := A)
        ((Equiv.symm (equiv A ((j : n) → A)) : (a : (j : n) → A) → C⋆ᵐᵒᵈ(A, (j : n) → A))
            (fun (j : n) ↦ ∑ i : m, v i * M i j) i :
          A))
    (∑ x : n, ∑ i : m, ‖M i x‖ * ‖v‖)

Tactic:
gcongr with i _
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalCStarAlgebra A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ(A, m → A)
i : n
h_1 : Membership.mem (γ := Finset n) Finset.univ i
h : LE.le (α := ℝ) (∑ i_1 : m, ‖v i_1 * M i_1 i‖) (∑ i_1 : m, ‖M i_1 i‖ * ‖v‖)
⊢ norm.{u_3} (E := A)
      ((Equiv.symm (equiv A ((j : n) → A)) : (a : (j : n) → A) → C⋆ᵐᵒᵈ(A, (j : n) → A))
          (fun (j : n) ↦ ∑ i : m, v i * M i j) i :
        A) ≤
    ∑ i_1 : m, ‖M i_1 i‖ * ‖v‖

Tactic:
apply norm_sum_le _ _ |>.trans

Premises used: LE.le.trans, norm_sum_le
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalCStarAlgebra A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ(A, m → A)
i : n
h_1 : Membership.mem (γ := Finset n) Finset.univ i
h : ∀ (j : m), Membership.mem (γ := Finset m) Finset.univ j → ‖v j * M j i‖ ≤ ‖M j i‖ * ‖v‖
⊢ LE.le (α := ℝ) (∑ i_1 : m, ‖v i_1 * M i_1 i‖) (∑ i_1 : m, ‖M i_1 i‖ * ‖v‖)

Tactic:
gcongr with j _
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalCStarAlgebra A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ(A, m → A)
i : n
h_1 : Membership.mem (γ := Finset n) Finset.univ i
j : m
h_2 : Membership.mem (γ := Finset m) Finset.univ j
h : ‖v j‖ * ‖M j i‖ ≤ ‖M j i‖ * ‖v‖
⊢ ‖v j * M j i‖ ≤ ‖M j i‖ * ‖v‖

Tactic:
apply norm_mul_le _ _ |>.trans

Premises used: LE.le.trans, norm_mul_le
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalCStarAlgebra A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ(A, m → A)
i : n
h_1 : Membership.mem (γ := Finset n) Finset.univ i
j : m
h_2 : Membership.mem (γ := Finset m) Finset.univ j
h : ‖M j i‖ * ‖v j‖ ≤ ‖M j i‖ * ‖v‖
⊢ ‖v j‖ * ‖M j i‖ ≤ ‖M j i‖ * ‖v‖

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalCStarAlgebra A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ(A, m → A)
i : n
h_1 : Membership.mem (γ := Finset n) Finset.univ i
j : m
h_2 : Membership.mem (γ := Finset m) Finset.univ j
h : ‖v j‖ ≤ ‖v‖
⊢ ‖M j i‖ * ‖v j‖ ≤ ‖M j i‖ * ‖v‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalCStarAlgebra A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ(A, m → A)
i : n
h : Membership.mem (γ := Finset n) Finset.univ i
j : m
h_1 : Membership.mem (γ := Finset m) Finset.univ j
⊢ ‖v j‖ ≤ ‖v‖

Tactic:
norm_apply_le_norm v j

Premises used: WithCStarModule.norm_apply_le_norm
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalCStarAlgebra A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ(A, m → A)
i : n
h : Membership.mem (γ := Finset n) Finset.univ i
j : m
h_1 : Membership.mem (γ := Finset m) Finset.univ j
⊢ ‖v j‖ ≤ ‖v‖

Tactic:
exact norm_apply_le_norm v j

Premises used: WithCStarModule.norm_apply_le_norm
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalCStarAlgebra A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
M : CStarMatrix m n A
h :
  ∀ (j : n),
    Membership.mem (γ := Finset n) Finset.univ j →
      ∀ (i : m),
        Membership.mem (γ := Finset m) Finset.univ i →
          ‖M i j‖ ≤
            norm (E := Matrix m n A)
              ((LinearEquiv.symm ofMatrixₗ : (a : CStarMatrix m n A) → Matrix m n A) M : Matrix m n A)
⊢ LE.le (α := ℝ) (∑ j : n, ∑ i : m, ‖M i j‖)
    (∑ x : n,
      ∑ x : m,
        norm (E := Matrix m n A)
          ((LinearEquiv.symm ofMatrixₗ : (a : CStarMatrix m n A) → Matrix m n A) M : Matrix m n A))

Tactic:
gcongr with j _ i _
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalCStarAlgebra A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
M : CStarMatrix m n A
j : n
h : Membership.mem (γ := Finset n) Finset.univ j
i : m
h_1 : Membership.mem (γ := Finset m) Finset.univ i
⊢ ‖M i j‖ ≤
    norm (E := Matrix m n A) ((LinearEquiv.symm ofMatrixₗ : (a : CStarMatrix m n A) → Matrix m n A) M : Matrix m n A)

Tactic:
ofMatrixₗ.symm (R := ℂ) M |>.norm_entry_le_entrywise_sup_norm

Premises used: LinearEquiv.symm, Matrix.norm_entry_le_entrywise_sup_norm, CStarMatrix.ofMatrixₗ, DFunLike.coe
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalCStarAlgebra A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
M : CStarMatrix m n A
j : n
h : Membership.mem (γ := Finset n) Finset.univ j
i : m
h_1 : Membership.mem (γ := Finset m) Finset.univ i
⊢ ‖M i j‖ ≤
    norm (E := Matrix m n A) ((LinearEquiv.symm ofMatrixₗ : (a : CStarMatrix m n A) → Matrix m n A) M : Matrix m n A)

Tactic:
exact ofMatrixₗ.symm (R := ℂ) M |>.norm_entry_le_entrywise_sup_norm

Premises used: LinearEquiv.symm, Matrix.norm_entry_le_entrywise_sup_norm, CStarMatrix.ofMatrixₗ, DFunLike.coe
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalCStarAlgebra A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
M : CStarMatrix m n A
⊢ ∑ x : n,
      ∑ x : m,
        norm (E := Matrix m n A)
          ((LinearEquiv.symm ofMatrixₗ : (a : CStarMatrix m n A) → Matrix m n A) M : Matrix m n A) =
    (↑(HMul.hMul (α := ℝ≥0) (↑(Fintype.card n) : ℝ≥0) (↑(Fintype.card m) : ℝ≥0)) : ℝ) *
      norm (E := Matrix m n A) ((LinearEquiv.symm ofMatrixₗ : (a : CStarMatrix m n A) → Matrix m n A) M : Matrix m n A)

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalCStarAlgebra A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
M : CStarMatrix m n A
i : ‖M‖ ≤ ∑ j : n, ∑ i : m, ‖M i j‖
i₁ :
  LE.le (α := ℝ) (∑ j : n, ∑ i : m, ‖M i j‖)
    (∑ x : n,
      ∑ x : m,
        norm (E := Matrix m n A)
          ((LinearEquiv.symm ofMatrixₗ : (a : CStarMatrix m n A) → Matrix m n A) M : Matrix m n A))
i₂ :
  ∑ x : n,
      ∑ x : m,
        norm (E := Matrix m n A)
          ((LinearEquiv.symm ofMatrixₗ : (a : CStarMatrix m n A) → Matrix m n A) M : Matrix m n A) =
    (↑(HMul.hMul (α := ℝ≥0) (↑(Fintype.card n) : ℝ≥0) (↑(Fintype.card m) : ℝ≥0)) : ℝ) *
      norm (E := Matrix m n A) ((LinearEquiv.symm ofMatrixₗ : (a : CStarMatrix m n A) → Matrix m n A) M : Matrix m n A)
⊢ ‖M‖ ≤
    (↑(HMul.hMul (α := ℝ≥0) (↑(Fintype.card n) : ℝ≥0) (↑(Fintype.card m) : ℝ≥0)) : ℝ) *
      norm (E := Matrix m n A) ((LinearEquiv.symm ofMatrixₗ : (a : CStarMatrix m n A) → Matrix m n A) M : Matrix m n A)

Tactic:
calc
    ‖M‖ ≤ ∑ j, ∑ i, ‖M i j‖ := by
      rw [norm_def]
      refine (toCLM M).opNorm_le_bound (by positivity) fun v => ?_
      simp only [toCLM_apply_eq_sum, Finset.sum_mul]
      apply pi_norm_le_sum_norm _ |>.trans
      gcongr with i _
      apply norm_sum_le _ _ |>.trans
      gcongr with j _
      apply norm_mul_le _ _ |>.trans
      rw [mul_comm]
      gcongr
      exact norm_apply_le_norm v j
    _ ≤ ∑ _ : n, ∑ _ : m, ‖ofMatrixₗ.symm (R := ℂ) M‖ := by
      gcongr with j _ i _
      exact ofMatrixₗ.symm (R := ℂ) M |>.norm_entry_le_entrywise_sup_norm
    _ = _ := by simp [mul_assoc]

Premises used: LinearEquiv.symm, CStarMatrix.ofMatrixₗ, DFunLike.coe
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonUnitalCStarAlgebra A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
⊢ IsUniformInducing (α := CStarMatrix m n A) (β := Matrix m n A)
    (⇑(Equiv.symm ofMatrix) : (a : CStarMatrix m n A) → Matrix m n A)

Tactic:
AntilipschitzWith.isUniformInducing antilipschitzWith_toMatrixAux
    lipschitzWith_toMatrixAux.uniformContinuous

Premises used: _private.0.CStarMatrix.antilipschitzWith_toMatrixAux, Matrix, Matrix.instUniformSpace._aux_1, AntilipschitzWith.isUniformInducing, LipschitzWith.uniformContinuous, _private.0.CStarMatrix.lipschitzWith_toMatrixAux