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
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)
⊢ 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‖
have 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‖
Tactic: obtain (h₀ | h₀) := (norm_nonneg (toCLM M v)).eq_or_lt
-- 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‖
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‖
⊢ 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‖
have 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‖
Tactic: obtain (h₀ | h₀) := (norm_nonneg (toCLM M v)).eq_or_lt
-- 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‖
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‖
have inl : 0 ≤ (↑C : ℝ) * ‖v‖
Tactic: rw [← 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
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‖
have 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))
Tactic: refine le_of_mul_le_mul_right ?_ h₀
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
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)
have 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‖₊
Tactic: refine AddMonoidHomClass.lipschitz_of_bound_nnnorm _ _ fun M => ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
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
⊢ 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‖₊
have 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‖
Tactic: rw [one_mul, ← NNReal.coe_le_coe, coe_nnnorm, coe_nnnorm, Matrix.norm_le_iff (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
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)
have 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)
Tactic: refine AddMonoidHomClass.antilipschitz_of_bound _ fun M => ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
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
⊢ 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‖
have 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‖
Tactic: refine (toCLM M).opNorm_le_bound (by positivity) fun v => ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
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)
⊢ 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‖
have 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‖
Tactic: simp only [toCLM_apply_eq_sum, 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_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)
⊢ 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‖
have 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‖)
Tactic: apply pi_norm_le_sum_norm _ |>.trans
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
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)
⊢ 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‖)
have 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‖
Tactic: gcongr with i _
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
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
⊢ 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‖
have h : LE.le (α := ℝ) (∑ i_1 : m, ‖v i_1 * M i_1 i‖) (∑ i_1 : m, ‖M i_1 i‖ * ‖v‖)
Tactic: apply norm_sum_le _ _ |>.trans
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
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
⊢ LE.le (α := ℝ) (∑ i_1 : m, ‖v i_1 * M i_1 i‖) (∑ i_1 : m, ‖M i_1 i‖ * ‖v‖)
have h : ∀ (j : m), Membership.mem (γ := Finset m) Finset.univ j → ‖v j * M j i‖ ≤ ‖M j i‖ * ‖v‖
Tactic: gcongr with j _
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
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 * M j i‖ ≤ ‖M j i‖ * ‖v‖
have h : ‖v j‖ * ‖M j i‖ ≤ ‖M j i‖ * ‖v‖
Tactic: apply norm_mul_le _ _ |>.trans
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
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‖ * ‖M j i‖ ≤ ‖M j i‖ * ‖v‖
have h : ‖M j i‖ * ‖v j‖ ≤ ‖M j i‖ * ‖v‖
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
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
⊢ ‖M j i‖ * ‖v j‖ ≤ ‖M j i‖ * ‖v‖
have h : ‖v j‖ ≤ ‖v‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
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 (α := ℝ) (∑ 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))
have 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)
Tactic: gcongr with j _ i _
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
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
⊢ ‖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)
have i : ‖M‖ ≤ ∑ j : n, ∑ i : m, ‖M i j‖
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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
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‖
⊢ ‖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)
have 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))
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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
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))
⊢ ‖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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
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
⊢ Eq (α := (x : CStarMatrix m n A × CStarMatrix m n A) → CStarMatrix m n A × CStarMatrix m n A)
    (fun (x : CStarMatrix m n A × CStarMatrix m n A) ↦
      ((Equiv.symm ofMatrix : (a : CStarMatrix m n A) → Matrix m n A) x.1,
        (Equiv.symm ofMatrix : (a : CStarMatrix m n A) → Matrix m n A) x.2))
    id
have h : ∀ (i : CStarMatrix m n A × CStarMatrix m n A) (i_1 : m) (j : n),
  ((Equiv.symm ofMatrix : (a : CStarMatrix m n A) → Matrix m n A) i.1,
          (Equiv.symm ofMatrix : (a : CStarMatrix m n A) → Matrix m n A) i.2).1
      i_1 j =
    (id i).1 i_1 j
Tactic: ext i
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
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
h :
  ∀ (i : CStarMatrix m n A × CStarMatrix m n A) (i_1 : m) (j : n),
    ((Equiv.symm ofMatrix : (a : CStarMatrix m n A) → Matrix m n A) i.1,
            (Equiv.symm ofMatrix : (a : CStarMatrix m n A) → Matrix m n A) i.2).1
        i_1 j =
      (id i).1 i_1 j
⊢ Eq (α := (x : CStarMatrix m n A × CStarMatrix m n A) → CStarMatrix m n A × CStarMatrix m n A)
    (fun (x : CStarMatrix m n A × CStarMatrix m n A) ↦
      ((Equiv.symm ofMatrix : (a : CStarMatrix m n A) → Matrix m n A) x.1,
        (Equiv.symm ofMatrix : (a : CStarMatrix m n A) → Matrix m n A) x.2))
    id
have h₁ : ∀ (i : CStarMatrix m n A × CStarMatrix m n A) (i_1 : m) (j : n),
  ((Equiv.symm ofMatrix : (a : CStarMatrix m n A) → Matrix m n A) i.1,
          (Equiv.symm ofMatrix : (a : CStarMatrix m n A) → Matrix m n A) i.2).2
      i_1 j =
    (id i).2 i_1 j
Tactic: ext i
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (hypothesis)
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
⊢ Eq (α := Filter (CStarMatrix m n A × CStarMatrix m n A)) (𝓤 (CStarMatrix m n A)) (𝓤 (CStarMatrix m n A))
have this : Eq (α := (x : CStarMatrix m n A × CStarMatrix m n A) → CStarMatrix m n A × CStarMatrix m n A)
  (fun (x : CStarMatrix m n A × CStarMatrix m n A) ↦
    ((Equiv.symm ofMatrix : (a : CStarMatrix m n A) → Matrix m n A) x.1,
      (Equiv.symm ofMatrix : (a : CStarMatrix m n A) → Matrix m n A) x.2))
  id
Tactic: have :
    (fun x : CStarMatrix m n A × CStarMatrix m n A => ⟨ofMatrix.symm x.1, ofMatrix.symm x.2⟩)
      = id := by
    ext i <;> rfl
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
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
this :
  Eq (α := (x : CStarMatrix m n A × CStarMatrix m n A) → CStarMatrix m n A × CStarMatrix m n A)
    (fun (x : CStarMatrix m n A × CStarMatrix m n A) ↦
      ((Equiv.symm ofMatrix : (a : CStarMatrix m n A) → Matrix m n A) x.1,
        (Equiv.symm ofMatrix : (a : CStarMatrix m n A) → Matrix m n A) x.2))
    id
⊢ Eq (α := Filter (CStarMatrix m n A × CStarMatrix m n A)) (𝓤 (CStarMatrix m n A)) (𝓤 (CStarMatrix m n A))
have rw : Eq (α := Filter (CStarMatrix m n A × CStarMatrix m n A)) (𝓤 (Matrix m n A)) (𝓤 (CStarMatrix m n A))
Tactic: rw [← uniformInducing_toMatrixAux.comap_uniformity, this, Filter.comap_id]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
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
⊢ Eq (α := Filter (CStarMatrix m n A)) (cobounded (CStarMatrix m n A))
    (Filter.comap (β := Matrix m n A) (⇑(Equiv.symm ofMatrix) : (a : CStarMatrix m n A) → Matrix m n A)
      (cobounded (Matrix m n A)))
have refine_1 : LE.le (α := Filter (CStarMatrix m n A)) (cobounded (CStarMatrix m n A))
  (Filter.comap (β := Matrix m n A) (⇑(Equiv.symm ofMatrix) : (a : CStarMatrix m n A) → Matrix m n A)
    (cobounded (Matrix m n A)))
Tactic: refine le_antisymm ?_ ?_