awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst : Unique n
inst_1 : Semiring R
inst_2 : AddCommMonoid A
inst_3 : Mul A
inst_4 : Star A
inst_5 : Module R A
x : A
i j : n
⊢ star x = star (fun (x_1 y : n) ↦ x) i j

Tactic:
simp [star_eq_conjTranspose]

Premises used: CStarMatrix.star_eq_conjTranspose
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst : Unique n
inst_1 : Semiring R
inst_2 : AddCommMonoid A
inst_3 : Mul A
inst_4 : Star A
inst_5 : Module R A
x : R
x_1 : A
h : ∀ (i j : n), x • x_1 = HSMul.hSMul (β := CStarMatrix n n A) x (fun (x y : n) ↦ x_1) i j
⊢ (fun (x_2 y : n) ↦ x • x_1) = HSMul.hSMul (β := CStarMatrix n n A) x fun (x y : n) ↦ x_1

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst : Unique n
inst_1 : Semiring R
inst_2 : AddCommMonoid A
inst_3 : Mul A
inst_4 : Star A
inst_5 : Module R A
x : R
x_1 : A
i j : n
⊢ x • x_1 = HSMul.hSMul (β := CStarMatrix n n A) x (fun (x y : n) ↦ x_1) i j

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
M₁ M₂ : CStarMatrix m n A
x : C⋆ᵐᵒᵈ(A, m → A)
i : n
h :
  ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* (M₁ + M₂)) i =
    ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M₁) i +
      ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M₂) i
⊢ Eq.{u_5 + 1} (α := A)
    (({
            toFun :=
              Function.comp (β := n → A)
                (⇑(ContinuousLinearEquiv.symm (WithCStarModule.equivL ℂ (A := A) (E := n → A)) :
                      (n → A) ≃L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
                  (a : n → A) → C⋆ᵐᵒᵈ(A, n → A))
                ((fun (v : m → A) ↦ v ᵥ* (M₁ + M₂)) ∘
                  (⇑(WithCStarModule.equivL ℂ (A := A) (E := m → A) : C⋆ᵐᵒᵈ(A, m → A) ≃L[ℂ] m → A) :
                    (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A)),
            map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } :
          (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
        x i :
      A)
    ((HAdd.hAdd (α := C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
            {
              toFun :=
                Function.comp (β := n → A)
                  (⇑(ContinuousLinearEquiv.symm (WithCStarModule.equivL ℂ (A := A) (E := n → A)) :
                        (n → A) ≃L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
                    (a : n → A) → C⋆ᵐᵒᵈ(A, n → A))
                  ((fun (v : m → A) ↦ v ᵥ* M₁) ∘
                    (⇑(WithCStarModule.equivL ℂ (A := A) (E := m → A) : C⋆ᵐᵒᵈ(A, m → A) ≃L[ℂ] m → A) :
                      (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A)),
              map_add' := ⋯, map_smul' := ⋯, cont := ⋯ : C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A) }
            {
              toFun :=
                Function.comp (β := n → A)
                  (⇑(ContinuousLinearEquiv.symm (WithCStarModule.equivL ℂ (A := A) (E := n → A)) :
                        (n → A) ≃L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
                    (a : n → A) → C⋆ᵐᵒᵈ(A, n → A))
                  ((fun (v : m → A) ↦ v ᵥ* M₂) ∘
                    (⇑(WithCStarModule.equivL ℂ (A := A) (E := m → A) : C⋆ᵐᵒᵈ(A, m → A) ≃L[ℂ] m → A) :
                      (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A)),
              map_add' := ⋯, map_smul' := ⋯, cont := ⋯ : C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A) } :
          (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
        x i :
      A)

Tactic:
simp only [ContinuousLinearMap.coe_mk', LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply,
      WithCStarModule.equivL_apply, WithCStarModule.equivL_symm_apply,
      WithCStarModule.equiv_symm_pi_apply, ContinuousLinearMap.add_apply, WithCStarModule.add_apply]

Premises used: LinearMap.coe_mk, WithCStarModule.add_apply, ContinuousLinearMap.add_apply, Function.comp_apply, WithCStarModule.equivL_symm_apply, AddHom.coe_mk, WithCStarModule.equiv_symm_pi_apply, ContinuousLinearMap.coe_mk', WithCStarModule.equivL_apply
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
M₁ M₂ : CStarMatrix m n A
x : C⋆ᵐᵒᵈ(A, m → A)
i : n
h :
  ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M₁ +
        (WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M₂)
      i =
    ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M₁) i +
      ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M₂) i
h₁ h₂ :
  ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M₁) i +
      ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M₂) i =
    ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M₁) i +
      ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M₂) i
⊢ ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* (M₁ + M₂)) i =
    ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M₁) i +
      ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M₂) i

Tactic:
rw [Matrix.vecMul_add, Pi.add_apply]

Premises used: Pi.add_apply, Matrix.vecMul_add
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
c : ℂ
M : CStarMatrix m n A
h :
  ∀ (x : C⋆ᵐᵒᵈ(A, m → A)) (i : n),
    Eq.{u_5 + 1} (α := A)
      (({
              toFun :=
                Function.comp (β := n → A)
                  (⇑(ContinuousLinearEquiv.symm (WithCStarModule.equivL ℂ (A := A) (E := n → A)) :
                        (n → A) ≃L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
                    (a : n → A) → C⋆ᵐᵒᵈ(A, n → A))
                  ((fun (v : m → A) ↦ v ᵥ* (c • M)) ∘
                    (⇑(WithCStarModule.equivL ℂ (A := A) (E := m → A) : C⋆ᵐᵒᵈ(A, m → A) ≃L[ℂ] m → A) :
                      (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A)),
              map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } :
            (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
          x i :
        A)
      ((HSMul.hSMul (α := ℂ) (β := C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) ((RingHom.id ℂ : (a : ℂ) → ℂ) c : ℂ)
              {
                toFun :=
                  Function.comp (β := n → A)
                    (⇑(ContinuousLinearEquiv.symm (WithCStarModule.equivL ℂ (A := A) (E := n → A)) :
                          (n → A) ≃L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
                      (a : n → A) → C⋆ᵐᵒᵈ(A, n → A))
                    ((fun (v : m → A) ↦ v ᵥ* M) ∘
                      (⇑(WithCStarModule.equivL ℂ (A := A) (E := m → A) : C⋆ᵐᵒᵈ(A, m → A) ≃L[ℂ] m → A) :
                        (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A)),
                map_add' := ⋯, map_smul' := ⋯, cont := ⋯ : C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A) } :
            (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
          x i :
        A)
⊢ {
      toFun :=
        Function.comp (β := n → A)
          (⇑(ContinuousLinearEquiv.symm (WithCStarModule.equivL ℂ (A := A) (E := n → A)) :
                (n → A) ≃L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
            (a : n → A) → C⋆ᵐᵒᵈ(A, n → A))
          ((fun (v : m → A) ↦ v ᵥ* (c • M)) ∘
            (⇑(WithCStarModule.equivL ℂ (A := A) (E := m → A) : C⋆ᵐᵒᵈ(A, m → A) ≃L[ℂ] m → A) :
              (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A)),
      map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } =
    HSMul.hSMul (α := ℂ) (β := C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) ((RingHom.id ℂ : (a : ℂ) → ℂ) c : ℂ)
      {
        toFun :=
          Function.comp (β := n → A)
            (⇑(ContinuousLinearEquiv.symm (WithCStarModule.equivL ℂ (A := A) (E := n → A)) :
                  (n → A) ≃L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
              (a : n → A) → C⋆ᵐᵒᵈ(A, n → A))
            ((fun (v : m → A) ↦ v ᵥ* M) ∘
              (⇑(WithCStarModule.equivL ℂ (A := A) (E := m → A) : C⋆ᵐᵒᵈ(A, m → A) ≃L[ℂ] m → A) :
                (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A)),
        map_add' := ⋯, map_smul' := ⋯, cont := ⋯ : C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A) }

Tactic:
ext x i
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
c : ℂ
M : CStarMatrix m n A
x : C⋆ᵐᵒᵈ(A, m → A)
i : n
h :
  ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* (c • M)) i =
    c • ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M) i
⊢ Eq.{u_5 + 1} (α := A)
    (({
            toFun :=
              Function.comp (β := n → A)
                (⇑(ContinuousLinearEquiv.symm (WithCStarModule.equivL ℂ (A := A) (E := n → A)) :
                      (n → A) ≃L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
                  (a : n → A) → C⋆ᵐᵒᵈ(A, n → A))
                ((fun (v : m → A) ↦ v ᵥ* (c • M)) ∘
                  (⇑(WithCStarModule.equivL ℂ (A := A) (E := m → A) : C⋆ᵐᵒᵈ(A, m → A) ≃L[ℂ] m → A) :
                    (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A)),
            map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } :
          (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
        x i :
      A)
    ((HSMul.hSMul (α := ℂ) (β := C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) ((RingHom.id ℂ : (a : ℂ) → ℂ) c : ℂ)
            {
              toFun :=
                Function.comp (β := n → A)
                  (⇑(ContinuousLinearEquiv.symm (WithCStarModule.equivL ℂ (A := A) (E := n → A)) :
                        (n → A) ≃L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
                    (a : n → A) → C⋆ᵐᵒᵈ(A, n → A))
                  ((fun (v : m → A) ↦ v ᵥ* M) ∘
                    (⇑(WithCStarModule.equivL ℂ (A := A) (E := m → A) : C⋆ᵐᵒᵈ(A, m → A) ≃L[ℂ] m → A) :
                      (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A)),
              map_add' := ⋯, map_smul' := ⋯, cont := ⋯ : C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A) } :
          (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
        x i :
      A)

Tactic:
simp only [ContinuousLinearMap.coe_mk', LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply,
      WithCStarModule.equivL_apply, WithCStarModule.equivL_symm_apply,
      WithCStarModule.equiv_symm_pi_apply, ContinuousLinearMap.smul_apply,
      WithCStarModule.smul_apply, RingHom.id_apply]

Premises used: LinearMap.coe_mk, ContinuousLinearMap.smul_apply, RingHom.id_apply, Function.comp_apply, WithCStarModule.equivL_symm_apply, AddHom.coe_mk, WithCStarModule.equiv_symm_pi_apply, ContinuousLinearMap.coe_mk', WithCStarModule.equivL_apply, WithCStarModule.smul_apply
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
c : ℂ
M : CStarMatrix m n A
x : C⋆ᵐᵒᵈ(A, m → A)
i : n
h :
  (c • (WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M) i =
    c • ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M) i
h₁ h₂ :
  c • ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M) i =
    c • ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M) i
⊢ ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* (c • M)) i =
    c • ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M) i

Tactic:
rw [Matrix.vecMul_smul, Pi.smul_apply]

Premises used: Matrix.vecMul_smul, Pi.smul_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
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ(A, m → A)
⊢ Eq (α := C⋆ᵐᵒᵈ(A, n → A))
    ((((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
            C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
          (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
        v :
      C⋆ᵐᵒᵈ(A, n → A))
    ((Equiv.symm (WithCStarModule.equiv A (n → A)) : (a : n → A) → C⋆ᵐᵒᵈ(A, n → A)) (v ᵥ* M) : C⋆ᵐᵒᵈ(A, n → A))

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.vecMul, Finset.sum, 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
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ(A, m → A)
h :
  ∀ (i : n),
    Eq.{u_5 + 1} (α := A)
      ((((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
              C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
            (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
          v i :
        A)
      ((Equiv.symm (WithCStarModule.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)
⊢ Eq (α := C⋆ᵐᵒᵈ(A, n → A))
    ((((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
            C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
          (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
        v :
      C⋆ᵐᵒᵈ(A, n → A))
    ((Equiv.symm (WithCStarModule.equiv A ((j : n) → A)) : (a : (j : n) → A) → C⋆ᵐᵒᵈ(A, (j : n) → A)) fun (j : n) ↦
        ∑ i : m, v i * M i j :
      C⋆ᵐᵒᵈ(A, (j : n) → A))

Tactic:
ext i
-- 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
v : C⋆ᵐᵒᵈ(A, m → A)
i : n
⊢ Eq.{u_5 + 1} (α := A)
    ((((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
            C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
          (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
        v i :
      A)
    ((Equiv.symm (WithCStarModule.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)

Tactic:
simp [toCLM_apply, Matrix.vecMul, dotProduct]

Premises used: dotProduct, Matrix.vecMul, CStarMatrix.toCLM_apply
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
inst_2 : Fintype n
⊢ Eq (α := (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))ᵐᵒᵖ)
    (AddHom.toFun
      (LinearMap.toAddHom
        ((↑(MulOpposite.opLinearEquiv ℂ) :
            (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) →ₗ[ℂ] (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))ᵐᵒᵖ) ∘ₗ
          toCLM))
      0)
    0

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
inst_2 : Fintype n
x y : CStarMatrix n n A
simp :
  (toCLM : (a : CStarMatrix n n A) → C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) (x * y) =
    HMul.hMul (α := C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) (β := C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
      ((toCLM : (a : CStarMatrix n n A) → C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) y :
        C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
      ((toCLM : (a : CStarMatrix n n A) → C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) x :
        C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
⊢ AddHom.toFun
      (LinearMap.toAddHom
        ((↑(MulOpposite.opLinearEquiv ℂ) :
            (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) →ₗ[ℂ] (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))ᵐᵒᵖ) ∘ₗ
          toCLM))
      (x * y) =
    HMul.hMul (α := (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))ᵐᵒᵖ)
      (AddHom.toFun
        (LinearMap.toAddHom
          ((↑(MulOpposite.opLinearEquiv ℂ) :
              (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) →ₗ[ℂ] (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))ᵐᵒᵖ) ∘ₗ
            toCLM))
        x)
      (AddHom.toFun
        (LinearMap.toAddHom
          ((↑(MulOpposite.opLinearEquiv ℂ) :
              (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) →ₗ[ℂ] (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))ᵐᵒᵖ) ∘ₗ
            toCLM))
        y)

Tactic:
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearMap.coe_comp,
        LinearEquiv.coe_coe, MulOpposite.coe_opLinearEquiv, Function.comp_apply,
        ← MulOpposite.op_mul, MulOpposite.op_inj]

Premises used: AddHom.toFun_eq_coe, LinearMap.coe_comp, MulOpposite.op_inj, LinearMap.coe_toAddHom, MulOpposite.op_mul, MulOpposite.coe_opLinearEquiv, Function.comp_apply, LinearEquiv.coe_coe
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
inst_2 : Fintype n
x y : CStarMatrix n n A
h :
  ∀ (x_1 : C⋆ᵐᵒᵈ(A, n → A)) (i : n),
    Eq.{u_5 + 1} (α := A)
      ((((toCLM : (a : CStarMatrix n n A) → C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) (x * y) :
              C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
            (a : C⋆ᵐᵒᵈ(A, n → A)) → C⋆ᵐᵒᵈ(A, n → A))
          x_1 i :
        A)
      ((HMul.hMul (α := C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) (β := C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
              ((toCLM : (a : CStarMatrix n n A) → C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) y :
                C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
              ((toCLM : (a : CStarMatrix n n A) → C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) x :
                C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
            (a : C⋆ᵐᵒᵈ(A, n → A)) → C⋆ᵐᵒᵈ(A, n → A))
          x_1 i :
        A)
⊢ (toCLM : (a : CStarMatrix n n A) → C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) (x * y) =
    HMul.hMul (α := C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) (β := C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
      ((toCLM : (a : CStarMatrix n n A) → C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) y :
        C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
      ((toCLM : (a : CStarMatrix n n A) → C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) x :
        C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
inst_2 : Fintype n
x y : CStarMatrix n n A
x_1 : C⋆ᵐᵒᵈ(A, n → A)
i : n
⊢ Eq.{u_5 + 1} (α := A)
    ((((toCLM : (a : CStarMatrix n n A) → C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) (x * y) :
            C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
          (a : C⋆ᵐᵒᵈ(A, n → A)) → C⋆ᵐᵒᵈ(A, n → A))
        x_1 i :
      A)
    ((HMul.hMul (α := C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) (β := C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
            ((toCLM : (a : CStarMatrix n n A) → C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) y :
              C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
            ((toCLM : (a : CStarMatrix n n A) → C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) x :
              C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
          (a : C⋆ᵐᵒᵈ(A, n → A)) → C⋆ᵐᵒᵈ(A, n → A))
        x_1 i :
      A)

Tactic:
simp [toCLM]

Premises used: CStarMatrix.toCLM
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
n : Type u_2
A : Type u_5
inst : NonUnitalCStarAlgebra A
inst_1 : Fintype n
M : CStarMatrix n n A
⊢ Eq (α := (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))ᵐᵒᵖ)
    (MulOpposite.op ((toCLM : (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: rfl, MulOpposite.op
-- 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 : DecidableEq m
M : CStarMatrix m n A
i : m
a : A
h :
  ∀ (i_1 : n),
    Eq.{u_5 + 1} (α := A)
      ((((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
              C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
            (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
          ((Equiv.symm (equiv A (m → A)) : (a : m → A) → C⋆ᵐᵒᵈ(A, m → A)) (Pi.single (M := fun (a : m) ↦ A) i a)) i_1 :
        A)
      ((Equiv.symm (equiv A ((j : n) → A)) : (a : (j : n) → A) → C⋆ᵐᵒᵈ(A, (j : n) → A)) (fun (j : n) ↦ a * M i j) i_1 :
        A)
⊢ Eq (α := C⋆ᵐᵒᵈ(A, n → A))
    ((((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
            C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
          (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
        ((Equiv.symm (equiv A (m → A)) : (a : m → A) → C⋆ᵐᵒᵈ(A, m → A)) (Pi.single (M := fun (a : m) ↦ A) i a)) :
      C⋆ᵐᵒᵈ(A, n → A))
    ((Equiv.symm (equiv A ((j : n) → A)) : (a : (j : n) → A) → C⋆ᵐᵒᵈ(A, (j : n) → A)) fun (j : n) ↦ a * M i j :
      C⋆ᵐᵒᵈ(A, (j : n) → A))

Tactic:
ext
-- 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 : DecidableEq m
M : CStarMatrix m n A
i : m
a : A
i_1 : n
⊢ Eq.{u_5 + 1} (α := A)
    ((((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
            C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
          (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
        ((Equiv.symm (equiv A (m → A)) : (a : m → A) → C⋆ᵐᵒᵈ(A, m → A)) (Pi.single (M := fun (a : m) ↦ A) i a)) i_1 :
      A)
    ((Equiv.symm (equiv A ((j : n) → A)) : (a : (j : n) → A) → C⋆ᵐᵒᵈ(A, (j : n) → A)) (fun (j : n) ↦ a * M i j) i_1 : A)

Tactic:
simp [toCLM_apply, equiv, Equiv.refl]

Premises used: CStarMatrix.toCLM_apply, WithCStarModule.equiv, Equiv.refl
-- 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 : DecidableEq m
M : CStarMatrix m n A
i : m
j : n
a : 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)) j =
    a * M i j

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
rw :
  ∀ (a : CStarMatrix m n A),
    Eq (α := C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
        ((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) a :
          C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
        (0 : C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) →
      a = 0
⊢ 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:
rw [injective_iff_map_eq_zero]

Premises used: injective_iff_map_eq_zero
-- 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))
h₁ : ∀ (i : m) (j : n), M i j = 0 i j
⊢ M = 0

Tactic:
ext i j
-- 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
h₁ :
  norm.{u_5} (E := A)
      ((((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
              C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
            (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
          ((Equiv.symm (WithCStarModule.equiv A (m → A)) : (a : m → A) → C⋆ᵐᵒᵈ(A, m → A))
            (Pi.single (M := fun (a : m) ↦ A) i (star (M i j))))
          j :
        A) =
    0
⊢ M i j = 0 i j

Tactic:
rw [zero_apply, ← norm_eq_zero, ← sq_eq_zero_iff, sq, ← CStarRing.norm_star_mul_self,
    ← toCLM_apply_single_apply]

Premises used: norm_eq_zero, CStarMatrix.zero_apply, sq, CStarRing.norm_star_mul_self, CStarMatrix.toCLM_apply_single_apply, sq_eq_zero_iff