awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
R_1 : Type u_3
S : Type u_4
A_1 : Type u_5
B : Type u_6
R : Type u_7
A : Type u_8
inst : Fintype m
inst_1 : Fintype n
inst_2 : Semiring R
inst_3 : AddCommMonoid A
inst_4 : Mul A
inst_5 : Module R A
inst_6 : Star A
e : m ≃ n
M N : CStarMatrix m m A
i j : n
h :
  AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) (M * N) i j =
    ∑ j_1 : n,
      AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) M i j_1 *
        AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) N j_1 j
⊢ AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) (M * N) i j =
    (AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) M *
        AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) N)
      i j

Tactic:
simp only [mul_apply]

Premises used: CStarMatrix.mul_apply
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
R_1 : Type u_3
S : Type u_4
A_1 : Type u_5
B : Type u_6
R : Type u_7
A : Type u_8
inst : Fintype m
inst_1 : Fintype n
inst_2 : Semiring R
inst_3 : AddCommMonoid A
inst_4 : Mul A
inst_5 : Module R A
inst_6 : Star A
e : m ≃ n
M N : CStarMatrix m m A
i j : n
⊢ AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) (M * N) i j =
    ∑ j_1 : n,
      AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) M i j_1 *
        AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) N j_1 j

Tactic:
Fintype.sum_equiv e _ _ ?_

Premises used: Multiset.sum, Multiset.foldr, Matrix.submatrix, dotProduct, Fintype.sum_equiv, Finset.sum
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
R_1 : Type u_3
S : Type u_4
A_1 : Type u_5
B : Type u_6
R : Type u_7
A : Type u_8
inst : Fintype m
inst_1 : Fintype n
inst_2 : Semiring R
inst_3 : AddCommMonoid A
inst_4 : Mul A
inst_5 : Module R A
inst_6 : Star A
e : m ≃ n
M N : CStarMatrix m m A
i j : n
h :
  ∀ (x : m),
    HMul.hMul (α := A)
        ((fun (j : m) ↦
            ((Equiv.symm ofMatrix : (a : CStarMatrix m m A) → Matrix m m A) M ((e.symm : (a : n) → m) i) j : A))
          x)
        ((fun (j_1 : m) ↦
            ((Equiv.symm ofMatrix : (a : CStarMatrix m m A) → Matrix m m A) N j_1 ((e.symm : (a : n) → m) j) : A))
          x) =
      AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) M i
          ((e : (a : m) → n) x) *
        AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) N
          ((e : (a : m) → n) x) j
⊢ AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) (M * N) i j =
    ∑ j_1 : n,
      AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) M i j_1 *
        AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) N j_1 j

Tactic:
refine Fintype.sum_equiv e _ _ ?_

Premises used: Fintype.sum_equiv
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
R_1 : Type u_3
S : Type u_4
A_1 : Type u_5
B : Type u_6
R : Type u_7
A : Type u_8
inst : Fintype m
inst_1 : Fintype n
inst_2 : Semiring R
inst_3 : AddCommMonoid A
inst_4 : Mul A
inst_5 : Module R A
inst_6 : Star A
e : m ≃ n
M N : CStarMatrix m m A
i j : n
k : m
⊢ HMul.hMul (α := A)
      ((fun (j : m) ↦
          ((Equiv.symm ofMatrix : (a : CStarMatrix m m A) → Matrix m m A) M ((e.symm : (a : n) → m) i) j : A))
        k)
      ((fun (j_1 : m) ↦
          ((Equiv.symm ofMatrix : (a : CStarMatrix m m A) → Matrix m m A) N j_1 ((e.symm : (a : n) → m) j) : A))
        k) =
    AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) M i
        ((e : (a : m) → n) k) *
      AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) N
        ((e : (a : m) → n) k) j

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
R_1 : Type u_3
S : Type u_4
A_1 : Type u_5
B : Type u_6
R : Type u_7
A : Type u_8
inst : Fintype m
inst_1 : Fintype n
inst_2 : Semiring R
inst_3 : AddCommMonoid A
inst_4 : Mul A
inst_5 : Module R A
inst_6 : Star A
e : m ≃ n
M : CStarMatrix m m A
h :
  ∀ (i j : n),
    AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) (star M) i j =
      star (AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) M) i j
⊢ AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) (star M) =
    star (AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) M)

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
R_1 : Type u_3
S : Type u_4
A_1 : Type u_5
B : Type u_6
R : Type u_7
A : Type u_8
inst : Fintype m
inst_1 : Fintype n
inst_2 : Semiring R
inst_3 : AddCommMonoid A
inst_4 : Mul A
inst_5 : Module R A
inst_6 : Star A
e : m ≃ n
M : CStarMatrix m m A
i j : n
h :
  Eq.{u_8 + 1} (α := A)
    (AddHom.toFun
      (LinearMap.toAddHom
        (↑(let __src : Matrix m m A ≃ Matrix n n A := Matrix.reindex e e;
            { toFun := __src.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯,
              right_inv := ⋯ }) :
          CStarMatrix m m A →ₗ[R] CStarMatrix n n A))
      (star M) i j)
    (star
      (AddHom.toFun
        (LinearMap.toAddHom
          (↑(let __src : Matrix m m A ≃ Matrix n n A := Matrix.reindex e e;
              { toFun := __src.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯,
                right_inv := ⋯ }) :
            CStarMatrix m m A →ₗ[R] CStarMatrix n n A))
        M)
      i j)
⊢ AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) (star M) i j =
    star (AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) M) i j

Tactic:
unfold reindexₗ

Premises used: CStarMatrix.reindexₗ
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
R_1 : Type u_3
S : Type u_4
A_1 : Type u_5
B : Type u_6
R : Type u_7
A : Type u_8
inst : Fintype m
inst_1 : Fintype n
inst_2 : Semiring R
inst_3 : AddCommMonoid A
inst_4 : Mul A
inst_5 : Module R A
inst_6 : Star A
e : m ≃ n
M : CStarMatrix m m A
i j : n
h :
  star M ((e.symm : (a : n) → m) i) ((e.symm : (a : n) → m) j) =
    star (Matrix.submatrix M (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m)) i j
⊢ Eq.{u_8 + 1} (α := A)
    (AddHom.toFun
      (LinearMap.toAddHom
        (↑(let __src : Matrix m m A ≃ Matrix n n A := Matrix.reindex e e;
            { toFun := __src.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯,
              right_inv := ⋯ }) :
          CStarMatrix m m A →ₗ[R] CStarMatrix n n A))
      (star M) i j)
    (star
      (AddHom.toFun
        (LinearMap.toAddHom
          (↑(let __src : Matrix m m A ≃ Matrix n n A := Matrix.reindex e e;
              { toFun := __src.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯,
                right_inv := ⋯ }) :
            CStarMatrix m m A →ₗ[R] CStarMatrix n n A))
        M)
      i j)

Tactic:
dsimp only [Equiv.toFun_as_coe, Equiv.invFun_as_coe, Matrix.reindex_symm, AddHom.toFun_eq_coe,
        AddHom.coe_mk, Matrix.reindex_apply, Matrix.submatrix_apply]

Premises used: Equiv.invFun_as_coe, Equiv.toFun_as_coe, Matrix.reindex_apply, AddHom.toFun_eq_coe, Matrix.reindex_symm, Matrix.submatrix_apply, AddHom.coe_mk
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
R_1 : Type u_3
S : Type u_4
A_1 : Type u_5
B : Type u_6
R : Type u_7
A : Type u_8
inst : Fintype m
inst_1 : Fintype n
inst_2 : Semiring R
inst_3 : AddCommMonoid A
inst_4 : Mul A
inst_5 : Module R A
inst_6 : Star A
e : m ≃ n
M : CStarMatrix m m A
i j : n
h :
  star (M ((e.symm : (a : n) → m) j) ((e.symm : (a : n) → m) i)) =
    star (Matrix.submatrix M (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m) j i)
⊢ star M ((e.symm : (a : n) → m) i) ((e.symm : (a : n) → m) j) =
    star (Matrix.submatrix M (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m)) i j

Tactic:
rw [star_apply, star_apply]

Premises used: CStarMatrix.star_apply
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
R_1 : Type u_3
S : Type u_4
A_1 : Type u_5
B : Type u_6
R : Type u_7
A : Type u_8
inst : Fintype m
inst_1 : Fintype n
inst_2 : Semiring R
inst_3 : AddCommMonoid A
inst_4 : Mul A
inst_5 : Module R A
inst_6 : Star A
e : m ≃ n
M : CStarMatrix m m A
i j : n
⊢ star (M ((e.symm : (a : n) → m) j) ((e.symm : (a : n) → m) i)) =
    star (Matrix.submatrix M (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m) j i)

Tactic:
simp [Matrix.submatrix_apply]

Premises used: Matrix.submatrix_apply
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
A : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : Semiring R
inst_3 : AddCommMonoid A
inst_4 : Mul A
inst_5 : Star A
inst_6 : Module R A
e : m ≃ n
M : CStarMatrix m m A
i j : n
⊢ Eq.{u_5 + 1} (α := A) ((reindexₐ R A e : (a : CStarMatrix m m A) → CStarMatrix n n A) M i j : A)
    ((Matrix.reindex e e : (a : Matrix m m A) → Matrix n n A) M i j : A)

Tactic:
rfl

Premises used: Matrix.submatrix, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
A : Type u_5
B : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : Semiring R
inst_3 : AddCommMonoid A
inst_4 : Mul A
inst_5 : Module R A
inst_6 : Star A
inst_7 : AddCommMonoid B
inst_8 : Mul B
inst_9 : Module R B
inst_10 : Star B
e : m ≃ n
M : CStarMatrix m m A
φ : A →ₗ[R] B
⊢ Eq (α := CStarMatrix n n B)
    ((reindexₐ R B e : (a : CStarMatrix m m B) → CStarMatrix n n B)
        ((mapₗ φ : (a : CStarMatrix m m A) → CStarMatrix m m B) M) :
      CStarMatrix n n B)
    ((mapₗ φ : (a : CStarMatrix n n A) → CStarMatrix n n B)
        ((reindexₐ R A e : (a : CStarMatrix m m A) → CStarMatrix n n A) M) :
      CStarMatrix n n B)

Tactic:
rfl

Premises used: Matrix.submatrix, CStarMatrix.map, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
A : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : Semiring R
inst_3 : AddCommMonoid A
inst_4 : Mul A
inst_5 : Module R A
inst_6 : Star A
e : m ≃ n
⊢ Eq (α := CStarMatrix n n A ≃⋆ₐ[R] CStarMatrix m m A) (reindexₐ R A e.symm) (StarAlgEquiv.symm (reindexₐ R A e))

Tactic:
simp [reindexₐ, reindexₗ]

Premises used: CStarMatrix.reindexₗ, CStarMatrix.reindexₐ
-- 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 n
inst_1 : Semiring R
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : Star A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : Star B
f : A →⋆ₙₐ[R] B
⊢ ∀ (m : R) (x : CStarMatrix n n A),
    (mapₗ
            (↑f :
              [inst : FunLike (A →⋆ₙₐ[R] B) A B] → [SemilinearMapClass (A →⋆ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
          (a : CStarMatrix n n A) → CStarMatrix n n B)
        (m • x) =
      HSMul.hSMul (α := R) (β := CStarMatrix n n B) ((MonoidHom.id R : (a : R) → R) m : R)
        ((mapₗ
                (↑f :
                  [inst : FunLike (A →⋆ₙₐ[R] B) A B] →
                    [SemilinearMapClass (A →⋆ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
              (a : CStarMatrix n n A) → CStarMatrix n n B)
            x :
          CStarMatrix n n B)

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 n
inst_1 : Semiring R
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : Star A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : Star B
f : A →⋆ₙₐ[R] B
⊢ Eq (α := CStarMatrix n n B)
    ((mapₗ
          (↑f :
            [inst : FunLike (A →⋆ₙₐ[R] B) A B] → [SemilinearMapClass (A →⋆ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
        (a : CStarMatrix n n A) → CStarMatrix n n B)
      0)
    0

Tactic:
simp [map_zero]

Premises used: map_zero
-- 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 n
inst_1 : Semiring R
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : Star A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : Star B
f : A →⋆ₙₐ[R] B
⊢ ∀ (x y : CStarMatrix n n A),
    (mapₗ
            (↑f :
              [inst : FunLike (A →⋆ₙₐ[R] B) A B] → [SemilinearMapClass (A →⋆ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
          (a : CStarMatrix n n A) → CStarMatrix n n B)
        (x + y) =
      HAdd.hAdd (α := CStarMatrix n n B) (β := CStarMatrix n n B)
        ((mapₗ
                (↑f :
                  [inst : FunLike (A →⋆ₙₐ[R] B) A B] →
                    [SemilinearMapClass (A →⋆ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
              (a : CStarMatrix n n A) → CStarMatrix n n B)
            x :
          CStarMatrix n n B)
        ((mapₗ
                (↑f :
                  [inst : FunLike (A →⋆ₙₐ[R] B) A B] →
                    [SemilinearMapClass (A →⋆ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
              (a : CStarMatrix n n A) → CStarMatrix n n B)
            y :
          CStarMatrix n n B)

Tactic:
simp [map_add]

Premises used: map_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 n
inst_1 : Semiring R
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : Star A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : Star B
f : A →⋆ₙₐ[R] B
M N : CStarMatrix n n A
h :
  ∀ (i j : n),
    (mapₗ
            (↑f :
              [inst : FunLike (A →⋆ₙₐ[R] B) A B] → [SemilinearMapClass (A →⋆ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
          (a : CStarMatrix n n A) → CStarMatrix n n B)
        (M * N) i j =
      HMul.hMul (α := CStarMatrix n n B) (β := CStarMatrix n n B)
        ((mapₗ
                (↑f :
                  [inst : FunLike (A →⋆ₙₐ[R] B) A B] →
                    [SemilinearMapClass (A →⋆ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
              (a : CStarMatrix n n A) → CStarMatrix n n B)
            M :
          CStarMatrix n n B)
        ((mapₗ
                (↑f :
                  [inst : FunLike (A →⋆ₙₐ[R] B) A B] →
                    [SemilinearMapClass (A →⋆ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
              (a : CStarMatrix n n A) → CStarMatrix n n B)
            N :
          CStarMatrix n n B)
        i j
⊢ (mapₗ (↑f : [inst : FunLike (A →⋆ₙₐ[R] B) A B] → [SemilinearMapClass (A →⋆ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
        (a : CStarMatrix n n A) → CStarMatrix n n B)
      (M * N) =
    HMul.hMul (α := CStarMatrix n n B) (β := CStarMatrix n n B)
      ((mapₗ
              (↑f :
                [inst : FunLike (A →⋆ₙₐ[R] B) A B] →
                  [SemilinearMapClass (A →⋆ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
            (a : CStarMatrix n n A) → CStarMatrix n n B)
          M :
        CStarMatrix n n B)
      ((mapₗ
              (↑f :
                [inst : FunLike (A →⋆ₙₐ[R] B) A B] →
                  [SemilinearMapClass (A →⋆ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
            (a : CStarMatrix n n A) → CStarMatrix n n B)
          N :
        CStarMatrix n n B)

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 n
inst_1 : Semiring R
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : Star A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : Star B
f : A →⋆ₙₐ[R] B
M N : CStarMatrix n n A
i j : n
⊢ (mapₗ (↑f : [inst : FunLike (A →⋆ₙₐ[R] B) A B] → [SemilinearMapClass (A →⋆ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
        (a : CStarMatrix n n A) → CStarMatrix n n B)
      (M * N) i j =
    HMul.hMul (α := CStarMatrix n n B) (β := CStarMatrix n n B)
      ((mapₗ
              (↑f :
                [inst : FunLike (A →⋆ₙₐ[R] B) A B] →
                  [SemilinearMapClass (A →⋆ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
            (a : CStarMatrix n n A) → CStarMatrix n n B)
          M :
        CStarMatrix n n B)
      ((mapₗ
              (↑f :
                [inst : FunLike (A →⋆ₙₐ[R] B) A B] →
                  [SemilinearMapClass (A →⋆ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
            (a : CStarMatrix n n A) → CStarMatrix n n B)
          N :
        CStarMatrix n n B)
      i j

Tactic:
simp only [mapₗ_apply, map, LinearMap.coe_coe, ofMatrix_apply, mul_apply, map_sum, map_mul,
      ofMatrix_apply]

Premises used: CStarMatrix.ofMatrix_apply, CStarMatrix.mul_apply, map_sum, map_mul, LinearMap.coe_coe, CStarMatrix.map, CStarMatrix.mapₗ_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 n
inst_1 : Semiring R
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : Star A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : Star B
f : A →⋆ₙₐ[R] B
M : CStarMatrix n n A
h :
  ∀ (i j : n),
    Eq.{u_6 + 1} (α := B)
      ((mapₗ
              (↑f :
                [inst : FunLike (A →⋆ₙₐ[R] B) A B] →
                  [SemilinearMapClass (A →⋆ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
            (a : CStarMatrix n n A) → CStarMatrix n n B)
          (star M) i j :
        B)
      (star
          ((mapₗ
                (↑f :
                  [inst : FunLike (A →⋆ₙₐ[R] B) A B] →
                    [SemilinearMapClass (A →⋆ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
              (a : CStarMatrix n n A) → CStarMatrix n n B)
            M)
          i j :
        B)
⊢ Eq (α := CStarMatrix n n B)
    ((mapₗ
            (↑f :
              [inst : FunLike (A →⋆ₙₐ[R] B) A B] → [SemilinearMapClass (A →⋆ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
          (a : CStarMatrix n n A) → CStarMatrix n n B)
        (star M) :
      CStarMatrix n n B)
    (star
        ((mapₗ
              (↑f :
                [inst : FunLike (A →⋆ₙₐ[R] B) A B] →
                  [SemilinearMapClass (A →⋆ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
            (a : CStarMatrix n n A) → CStarMatrix n n B)
          M) :
      CStarMatrix n n B)

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 n
inst_1 : Semiring R
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : Star A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : Star B
f : A →⋆ₙₐ[R] B
M : CStarMatrix n n A
i j : n
⊢ Eq.{u_6 + 1} (α := B)
    ((mapₗ
            (↑f :
              [inst : FunLike (A →⋆ₙₐ[R] B) A B] → [SemilinearMapClass (A →⋆ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
          (a : CStarMatrix n n A) → CStarMatrix n n B)
        (star M) i j :
      B)
    (star
        ((mapₗ
              (↑f :
                [inst : FunLike (A →⋆ₙₐ[R] B) A B] →
                  [SemilinearMapClass (A →⋆ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
            (a : CStarMatrix n n A) → CStarMatrix n n B)
          M)
        i j :
      B)

Tactic:
simp [map, star_apply, map_star]

Premises used: StarHomClass.map_star, CStarMatrix.star_apply, CStarMatrix.map
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
n : Type u_2
R : Type u_3
A : Type u_5
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
inst_3 : Semiring A
inst_4 : Algebra R A
r : R
i j : n
⊢ Eq.{u_5 + 1} (α := A) ((algebraMap R (CStarMatrix n n A) : (a : R) → CStarMatrix n n A) r i j : A)
    (if i = j then (algebraMap R A : (a : R) → A) r else 0 : A)

Tactic:
rfl

Premises used: Matrix.diagonal, rfl, ite
-- 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
⊢ (fun (M : CStarMatrix n n A) ↦ M default default) ((fun (a : A) (x y : n) ↦ a) x) = x

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 : Unique n
inst_1 : Semiring R
inst_2 : AddCommMonoid A
inst_3 : Mul A
inst_4 : Star A
inst_5 : Module R A
x : CStarMatrix n n A
h : ∀ (i j : n), (fun (a : A) (x y : n) ↦ a) ((fun (M : CStarMatrix n n A) ↦ M default default) x) i j = x i j
⊢ (fun (a : A) (x y : n) ↦ a) ((fun (M : CStarMatrix n n A) ↦ M default default) x) = x

Tactic:
ext i j
-- 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 : CStarMatrix n n A
i j : n
⊢ (fun (a : A) (x y : n) ↦ a) ((fun (M : CStarMatrix n n A) ↦ M default default) x) i j = x i j

Tactic:
simp [Subsingleton.elim i default, Subsingleton.elim j default]

Premises used: Inhabited.default, Subsingleton.elim
-- 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 x_1 : A
h :
  ∀ (i j : n),
    x * x_1 =
      HMul.hMul (α := CStarMatrix n n A) (β := CStarMatrix n n A) (fun (x_2 y : n) ↦ x) (fun (x y : n) ↦ x_1) i j
⊢ (fun (x_2 y : n) ↦ x * x_1) = HMul.hMul (α := CStarMatrix n n A) (fun (x_2 y : n) ↦ 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 x_1 : A
i j : n
⊢ x * x_1 = HMul.hMul (α := CStarMatrix n n A) (β := CStarMatrix n n A) (fun (x_2 y : n) ↦ x) (fun (x y : n) ↦ x_1) i j

Tactic:
simp [mul_apply]

Premises used: CStarMatrix.mul_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 : Unique n
inst_1 : Semiring R
inst_2 : AddCommMonoid A
inst_3 : Mul A
inst_4 : Star A
inst_5 : Module R A
x x_1 : A
h :
  ∀ (i j : n),
    x + x_1 =
      HAdd.hAdd (α := CStarMatrix n n A) (β := CStarMatrix n n A) (fun (x_2 y : n) ↦ x) (fun (x y : n) ↦ x_1) i j
⊢ (fun (x_2 y : n) ↦ x + x_1) = HAdd.hAdd (α := CStarMatrix n n A) (fun (x_2 y : n) ↦ 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 x_1 : A
i j : n
⊢ x + x_1 = HAdd.hAdd (α := CStarMatrix n n A) (β := CStarMatrix n n A) (fun (x_2 y : n) ↦ 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 : 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
h : ∀ (i j : n), star x = star (fun (x_1 y : n) ↦ x) i j
⊢ Eq (α := CStarMatrix n n A) (fun (x_1 y : n) ↦ star x) (star fun (x_1 y : n) ↦ x)

Tactic:
ext