awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
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
⊢ 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:
ext 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
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:
rfl
-- 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
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:
rfl
-- 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
⊢ 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
-- 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
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
rw : Eq (α := Filter (CStarMatrix m n A × CStarMatrix m n A)) (𝓤 (Matrix m n A)) (𝓤 (CStarMatrix m n A))
⊢ Eq (α := Filter (CStarMatrix m n A × CStarMatrix m n A)) (𝓤 (CStarMatrix m n A)) (𝓤 (CStarMatrix m n A))

Tactic:
rw [← uniformInducing_toMatrixAux.comap_uniformity, this, Filter.comap_id]

Premises used: IsUniformInducing.comap_uniformity, Filter.comap_id, _private.0.CStarMatrix.uniformInducing_toMatrixAux
-- 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
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)) (𝓤 (Matrix m n A)) (𝓤 (CStarMatrix m n A))

Tactic:
rfl
-- 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
⊢ 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)))

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- 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_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)))
refine_2 :
  LE.le (α := Filter (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)))
    (cobounded (CStarMatrix m n 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)))

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- 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
⊢ 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:
antilipschitzWith_toMatrixAux.tendsto_cobounded.le_comap

Premises used: Filter.Tendsto.le_comap, _private.0.CStarMatrix.antilipschitzWith_toMatrixAux, AntilipschitzWith.tendsto_cobounded, Set.Mem, setOf, CStarMatrix
-- 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
⊢ 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:
exact antilipschitzWith_toMatrixAux.tendsto_cobounded.le_comap

Premises used: Filter.Tendsto.le_comap, _private.0.CStarMatrix.antilipschitzWith_toMatrixAux, AntilipschitzWith.tendsto_cobounded
-- 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
⊢ LE.le (α := Filter (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)))
    (cobounded (CStarMatrix m n A))

Tactic:
lipschitzWith_toMatrixAux.comap_cobounded_le

Premises used: Set.Mem, setOf, LipschitzWith.comap_cobounded_le, CStarMatrix, _private.0.CStarMatrix.lipschitzWith_toMatrixAux
-- 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
⊢ LE.le (α := Filter (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)))
    (cobounded (CStarMatrix m n A))

Tactic:
exact lipschitzWith_toMatrixAux.comap_cobounded_le

Premises used: LipschitzWith.comap_cobounded_le, _private.0.CStarMatrix.lipschitzWith_toMatrixAux
-- 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
⊢ 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)))

Tactic:
have : cobounded (CStarMatrix m n A) = Filter.comap ofMatrix.symm (cobounded _) := by
    refine le_antisymm ?_ ?_
    · exact antilipschitzWith_toMatrixAux.tendsto_cobounded.le_comap
    · exact lipschitzWith_toMatrixAux.comap_cobounded_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
this :
  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)))
⊢ Eq (α := Filter (CStarMatrix m n A)) (cobounded (CStarMatrix m n A)) (cobounded ((i : m) → n → A))

Tactic:
this.trans Filter.comap_id

Premises used: Filter.comap_id, Eq.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
this :
  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)))
⊢ Eq (α := Filter (CStarMatrix m n A)) (cobounded (CStarMatrix m n A)) (cobounded ((i : m) → n → A))

Tactic:
exact this.trans Filter.comap_id

Premises used: Filter.comap_id, Eq.trans
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m : Type u_2
n : Type u_3
inst_3 : Fintype m
inst_4 : Fintype n
⊢ CompleteSpace (CStarMatrix m n A)

Tactic:
inferInstanceAs <| CompleteSpace (Matrix m n A)

Premises used: _private.0.CStarMatrix.instCompleteSpace._proof_1
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m : Type u_2
n : Type u_3
inst_3 : Fintype m
inst_4 : Fintype n
⊢ T2Space (CStarMatrix m n A)

Tactic:
inferInstanceAs <| T2Space (Matrix m n A)

Premises used: _private.0.CStarMatrix.instT2Space._proof_1
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m : Type u_2
n : Type u_3
inst_3 : Fintype m
inst_4 : Fintype n
⊢ T3Space (CStarMatrix m n A)

Tactic:
inferInstanceAs <| T3Space (Matrix m n A)

Premises used: _private.0.CStarMatrix.instT3Space._proof_1
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m : Type u_2
n : Type u_3
inst_3 : Fintype m
inst_4 : Fintype n
⊢ IsTopologicalAddGroup (CStarMatrix m n A)

Tactic:
inferInstanceAs <| IsTopologicalAddGroup (Matrix m n A)

Premises used: _private.0.CStarMatrix.instIsTopologicalAddGroup._proof_1
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m : Type u_2
n : Type u_3
inst_3 : Fintype m
inst_4 : Fintype n
⊢ IsUniformAddGroup (CStarMatrix m n A)

Tactic:
inferInstanceAs <| IsUniformAddGroup (Matrix m n A)

Premises used: _private.0.CStarMatrix.instIsUniformAddGroup._proof_1
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m : Type u_2
n : Type u_3
inst_3 : Fintype m
inst_4 : Fintype n
R : Type u_4
inst_5 : SMul R A
inst_6 : TopologicalSpace R
inst_7 : ContinuousSMul R A
⊢ ContinuousSMul R (CStarMatrix m n A)

Tactic:
inferInstanceAs <| ContinuousSMul R (Matrix m n A)

Premises used: _private.0.CStarMatrix.instContinuousSMul._proof_1
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m : Type u_2
n : Type u_3
inst_3 : Fintype m
inst_4 : Fintype n
⊢ Eq (α := Filter (CStarMatrix m n A × CStarMatrix m n A)) (𝓤 (CStarMatrix m n A)) (𝓤 (CStarMatrix m n A))

Tactic:
CStarMatrix.uniformity_eq_aux.symm

Premises used: Matrix, _private.0.CStarMatrix.uniformity_eq_aux, CStarMatrix, instTopologicalSpaceMatrix._aux_1, CStarMatrix.instTopologicalSpace._aux_1, Eq.symm
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m : Type u_2
n : Type u_3
inst_3 : Fintype m
inst_4 : Fintype n
x : Set (CStarMatrix m n A)
⊢ Bornology.IsBounded x ↔ Bornology.IsBounded x

Tactic:
Filter.ext_iff.1 CStarMatrix.cobounded_eq_aux.symm _

Premises used: Set.Mem, _private.0.CStarMatrix.cobounded_eq_aux, setOf, Bornology.IsBounded, Filter.ext_iff, Iff.mp, Bornology.IsCobounded, Eq.symm
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m : Type u_2
n : Type u_3
inst_3 : Fintype m
inst_4 : Fintype n
⊢ Eq (α := Filter (CStarMatrix m n A × CStarMatrix m n A)) (𝓤 (CStarMatrix m n A)) (𝓤 (CStarMatrix m n A))

Tactic:
exacts [CStarMatrix.uniformity_eq_aux.symm, Filter.ext_iff.1 CStarMatrix.cobounded_eq_aux.symm _]

Premises used: _private.0.CStarMatrix.cobounded_eq_aux, _private.0.CStarMatrix.uniformity_eq_aux, Filter.ext_iff, Iff.mp, Eq.symm
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m : Type u_2
n : Type u_3
inst_3 : Fintype m
inst_4 : Fintype n
⊢ Eq (α := Filter (CStarMatrix m n A × CStarMatrix m n A)) (𝓤 (CStarMatrix m n A)) (𝓤 (CStarMatrix m n A))

Tactic:
finally
  exacts [CStarMatrix.uniformity_eq_aux.symm, Filter.ext_iff.1 CStarMatrix.cobounded_eq_aux.symm _]
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m : Type u_2
n : Type u_3
inst_3 : Fintype m
inst_4 : Fintype n
x x_1 : CStarMatrix n n A
simpa :
  ‖HMul.hMul (α := (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))ᵐᵒᵖ) (β := (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))ᵐᵒᵖ)
        ((toCLMNonUnitalAlgHom : (a : CStarMatrix n n A) → (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))ᵐᵒᵖ) x :
          (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))ᵐᵒᵖ)
        ((toCLMNonUnitalAlgHom : (a : CStarMatrix n n A) → (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))ᵐᵒᵖ) x_1 :
          (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))ᵐᵒᵖ)‖ ≤
    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))ᵐᵒᵖ) x :
          (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))ᵐᵒᵖ) *
      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))ᵐᵒᵖ) x_1 :
          (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))ᵐᵒᵖ)
⊢ ‖x * x_1‖ ≤ ‖x‖ * ‖x_1‖

Tactic:
simpa only [norm_def', map_mul] using norm_mul_le _ _

Premises used: CStarMatrix.norm_def', map_mul, norm_mul_le
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m : Type u_2
n : Type u_3
inst_3 : Fintype m
inst_4 : Fintype n
⊢ sorry

Tactic:
.of_le_norm_mul_star_self fun M ↦ by
    have hmain : ‖M‖ ≤ √‖M * star M‖ := by
      change ‖toCLM M‖ ≤ √‖M * star M‖
      rw [opNorm_le_iff (by positivity)]
      intro v
      rw [norm_eq_sqrt_norm_inner_self (A := A), ← inner_toCLM_conjTranspose_right]
      have h₁ : ‖⟪v, (toCLM Mᴴ) ((toCLM M) v)⟫_A‖ ≤ ‖M * star M‖ * ‖v‖ ^ 2 := calc
          _ ≤ ‖v‖ * ‖(toCLM Mᴴ) (toCLM M v)‖ := norm_inner_le (C⋆ᵐᵒᵈ(A, n → A))
          _ ≤ ‖v‖ * ‖(toCLM Mᴴ).comp (toCLM M)‖ * ‖v‖ := by
                    rw [mul_assoc]
                    gcongr
                    rw [← ContinuousLinearMap.comp_apply]
                    exact le_opNorm ((toCLM Mᴴ).comp (toCLM M)) v
          _ = ‖(toCLM Mᴴ).comp (toCLM M)‖ * ‖v‖ ^ 2 := by ring
          _ = ‖M * star M‖ * ‖v‖ ^ 2 := by
                    congr
                    apply MulOpposite.op_injective
                    simp only [← toCLMNonUnitalAlgHom_eq_toCLM, map_mul]
                    rfl
      have h₂ : ‖v‖ = √(‖v‖ ^ 2) := by simp
      rw [h₂, ← Real.sqrt_mul]
      · gcongr
      positivity
    rw [← Real.sqrt_le_sqrt_iff (by positivity)]
    simp [hmain]

Premises used: Unit.unit, sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Bool.true, Function.const, Lean.Name, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m : Type u_2
n : Type u_3
inst_3 : Fintype m
inst_4 : Fintype n
x : ℂ
y z : CStarMatrix n n A
⊢ (x • y) • z = x • y • z

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
m : Type u_2
n : Type u_3
inst_3 : Fintype m
inst_4 : Fintype n
⊢ StarOrderedRing (CStarMatrix n n A)

Tactic:
CStarAlgebra.spectralOrderedRing _

Premises used: CStarAlgebra.spectralOrderedRing
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
n : Type u_2
inst_3 : Fintype n
inst_4 : DecidableEq n
r : ℂ
M : CStarMatrix n n A
⊢ ‖r • M‖ ≤ ‖r‖ * ‖M‖

Tactic:
simpa only [norm_def, map_smul] using (toCLM M).opNorm_smul_le r

Premises used: CStarMatrix.toCLM, ContinuousLinearMap.opNorm_smul_le, DFunLike.coe, map_smul, CStarMatrix.norm_def
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
inst : NonUnitalCStarAlgebra A
⊢ Eq (α := (a : Matrix m n A) → CStarMatrix m n A) (⇑ofMatrix : (a : Matrix m n A) → CStarMatrix m n A)
    (⇑ofMatrixL : (a : Matrix m n A) → CStarMatrix m n A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
Goal:
F : Type u_1
A₁ : Type u_2
A₂ : Type u_3
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : PartialOrder A₂
inst_4 : StarOrderedRing A₁
inst_5 : StarOrderedRing A₂
inst_6 : FunLike F A₁ A₂
inst_7 : LinearMapClass F ℂ A₁ A₂
h :
  ∀ (φ : F) (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁),
    0 ≤ M → LE.le.{u_3} (α := CStarMatrix (Fin k) (Fin k) A₂) 0 (M.map (⇑φ : (a : A₁) → A₂))
φ : F
a : A₁
ha : 0 ≤ a
⊢ LE.le.{u_3} (α := A₂) (0 : A₂) ((φ : (a : A₁) → A₂) a : A₂)

Tactic:
simpa using map_nonneg (toOneByOne (Fin 1) ℂ A₂).symm <|
    h φ 1 _ <| map_nonneg (toOneByOne (Fin 1) ℂ A₁) ha

Premises used: CStarMatrix.toOneByOne, map_nonneg, StarAlgEquiv.symm, Complex, OfNat.ofNat, Fin
-- Module: Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
Goal:
F : Type u_1
A₁ : Type u_2
A₂ : Type u_3
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : PartialOrder A₂
inst_4 : StarOrderedRing A₁
inst_5 : StarOrderedRing A₂
inst_6 : FunLike F A₁ A₂
inst_7 : LinearMapClass F ℂ A₁ A₂
inst_8 : CompletelyPositiveMapClass F A₁ A₂
⊢ OrderHomClass F A₁ A₂

Tactic:
.of_map_cstarMatrix_nonneg CompletelyPositiveMapClass.map_cstarMatrix_nonneg'

Premises used: CompletelyPositiveMapClass.map_cstarMatrix_nonneg', OrderHomClass.of_map_cstarMatrix_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : PartialOrder A₂
inst_4 : StarOrderedRing A₁
inst_5 : StarOrderedRing A₂
f g : A₁ →CP A₂
h : Eq (α := (a : A₁) → A₂) ((fun (f : A₁ →CP A₂) ↦ f.toFun) f) ((fun (f : A₁ →CP A₂) ↦ f.toFun) g)
mk :
  ∀ (toLinearMap : A₁ →ₗ[ℂ] A₂)
    (map_cstarMatrix_nonneg' :
      ∀ (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁) (hM : 0 ≤ M),
        LE.le.{u_2} (α := CStarMatrix (Fin k) (Fin k) A₂) 0 (M.map (⇑toLinearMap : (a : A₁) → A₂)))
    (h :
      Eq (α := (a : A₁) → A₂)
        ((fun (f : A₁ →CP A₂) ↦ f.toFun)
          { toLinearMap := toLinearMap, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg' })
        ((fun (f : A₁ →CP A₂) ↦ f.toFun) g)),
    { toLinearMap := toLinearMap, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg' : A₁ →CP A₂ } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : PartialOrder A₂
inst_4 : StarOrderedRing A₁
inst_5 : StarOrderedRing A₂
g : A₁ →CP A₂
toLinearMap : A₁ →ₗ[ℂ] A₂
map_cstarMatrix_nonneg' :
  ∀ (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁) (hM : 0 ≤ M),
    LE.le.{u_2} (α := CStarMatrix (Fin k) (Fin k) A₂) 0 (M.map (⇑toLinearMap : (a : A₁) → A₂))
h :
  Eq (α := (a : A₁) → A₂)
    ((fun (f : A₁ →CP A₂) ↦ f.toFun) { toLinearMap := toLinearMap, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg' })
    ((fun (f : A₁ →CP A₂) ↦ f.toFun) g)
mk :
  ∀ (toLinearMap_1 : A₁ →ₗ[ℂ] A₂)
    (map_cstarMatrix_nonneg'_1 :
      ∀ (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁) (hM : 0 ≤ M),
        LE.le.{u_2} (α := CStarMatrix (Fin k) (Fin k) A₂) 0 (M.map (⇑toLinearMap_1 : (a : A₁) → A₂)))
    (h :
      Eq (α := (a : A₁) → A₂)
        ((fun (f : A₁ →CP A₂) ↦ f.toFun)
          { toLinearMap := toLinearMap, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg' })
        ((fun (f : A₁ →CP A₂) ↦ f.toFun)
          { toLinearMap := toLinearMap_1, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg'_1 })),
    { toLinearMap := toLinearMap, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg' : A₁ →CP A₂ } =
      { toLinearMap := toLinearMap_1, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg'_1 }
⊢ { toLinearMap := toLinearMap, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg' : A₁ →CP A₂ } = g

Tactic:
cases g
-- Module: Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : PartialOrder A₂
inst_4 : StarOrderedRing A₁
inst_5 : StarOrderedRing A₂
toLinearMap : A₁ →ₗ[ℂ] A₂
map_cstarMatrix_nonneg' :
  ∀ (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁) (hM : 0 ≤ M),
    LE.le.{u_2} (α := CStarMatrix (Fin k) (Fin k) A₂) 0 (M.map (⇑toLinearMap : (a : A₁) → A₂))
toLinearMap_1 : A₁ →ₗ[ℂ] A₂
map_cstarMatrix_nonneg'_1 :
  ∀ (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁) (hM : 0 ≤ M),
    LE.le.{u_2} (α := CStarMatrix (Fin k) (Fin k) A₂) 0 (M.map (⇑toLinearMap_1 : (a : A₁) → A₂))
h :
  Eq (α := (a : A₁) → A₂)
    ((fun (f : A₁ →CP A₂) ↦ f.toFun) { toLinearMap := toLinearMap, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg' })
    ((fun (f : A₁ →CP A₂) ↦ f.toFun)
      { toLinearMap := toLinearMap_1, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg'_1 })
mk : toLinearMap = toLinearMap_1
⊢ { toLinearMap := toLinearMap, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg' : A₁ →CP A₂ } =
    { toLinearMap := toLinearMap_1, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg'_1 }

Tactic:
congr