awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Fintype n
inst_6 : DecidableEq n
inst_7 : CommSemiring S
inst_8 : Algebra R S
inst_9 : Algebra S A
inst_10 : IsScalarTower R S A
inst_11 : Fintype m
inst_12 : DecidableEq m
x : Matrix m m A ⊗[R] Matrix n n B
⊢ Eq (α := Matrix (m × n) (m × n) (A ⊗[R] B))
    (((kroneckerTMulAlgEquiv m n R S A B : Matrix m m A ⊗[R] Matrix n n B ≃ₐ[S] Matrix (m × n) (m × n) (A ⊗[R] B)) :
          (a : Matrix m m A ⊗[R] Matrix n n B) → Matrix (m × n) (m × n) (A ⊗[R] B))
        x :
      Matrix (m × n) (m × n) (A ⊗[R] B))
    (((kroneckerTMulLinearEquiv m m n n R S A B :
            Matrix m m A ⊗[R] Matrix n n B ≃ₗ[S] Matrix (m × n) (m × n) (A ⊗[R] B)) :
          (a : Matrix m m A ⊗[R] Matrix n n B) → Matrix (m × n) (m × n) (A ⊗[R] B))
        x :
      Matrix (m × n) (m × n) (A ⊗[R] B))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Fintype n
inst_6 : DecidableEq n
inst_7 : CommSemiring S
inst_8 : Algebra R S
inst_9 : Algebra S A
inst_10 : IsScalarTower R S A
inst_11 : Fintype m
inst_12 : DecidableEq m
x : Matrix (m × n) (m × n) (A ⊗[R] B)
⊢ Eq (α := Matrix m m A ⊗[R] Matrix n n B)
    (((AlgEquiv.symm (kroneckerTMulAlgEquiv m n R S A B) :
            Matrix (m × n) (m × n) (A ⊗[R] B) ≃ₐ[S] Matrix m m A ⊗[R] Matrix n n B) :
          (a : Matrix (m × n) (m × n) (A ⊗[R] B)) → Matrix m m A ⊗[R] Matrix n n B)
        x :
      Matrix m m A ⊗[R] Matrix n n B)
    (((LinearEquiv.symm (kroneckerTMulLinearEquiv m m n n R S A B) :
            Matrix (m × n) (m × n) (A ⊗[R] B) ≃ₗ[S] Matrix m m A ⊗[R] Matrix n n B) :
          (a : Matrix (m × n) (m × n) (A ⊗[R] B)) → Matrix m m A ⊗[R] Matrix n n B)
        x :
      Matrix m m A ⊗[R] Matrix n n B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Fintype n
inst_6 : DecidableEq n
inst_7 : CommSemiring S
inst_8 : Algebra R S
inst_9 : Algebra S A
inst_10 : IsScalarTower R S A
inst_11 : Fintype m
inst_12 : DecidableEq m
inst_13 : StarRing R
inst_14 : StarAddMonoid A
inst_15 : StarAddMonoid B
inst_16 : StarModule R A
inst_17 : StarModule R B
x : Matrix m m A ⊗[R] Matrix n n B
⊢ Eq (α := Matrix (m × n) (m × n) (A ⊗[R] B))
    (((kroneckerTMulAlgEquiv m n R S A B : Matrix m m A ⊗[R] Matrix n n B ≃ₐ[S] Matrix (m × n) (m × n) (A ⊗[R] B)) :
        (a : Matrix m m A ⊗[R] Matrix n n B) → Matrix (m × n) (m × n) (A ⊗[R] B))
      (star 0))
    (star
      (((kroneckerTMulAlgEquiv m n R S A B : Matrix m m A ⊗[R] Matrix n n B ≃ₐ[S] Matrix (m × n) (m × n) (A ⊗[R] B)) :
          (a : Matrix m m A ⊗[R] Matrix n n B) → Matrix (m × n) (m × n) (A ⊗[R] B))
        0))

Tactic:
simp
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Fintype n
inst_6 : DecidableEq n
inst_7 : CommSemiring S
inst_8 : Algebra R S
inst_9 : Algebra S A
inst_10 : IsScalarTower R S A
inst_11 : Fintype m
inst_12 : DecidableEq m
inst_13 : StarRing R
inst_14 : StarAddMonoid A
inst_15 : StarAddMonoid B
inst_16 : StarModule R A
inst_17 : StarModule R B
x : Matrix m m A ⊗[R] Matrix n n B
⊢ ∀ (x : Matrix m m A) (y : Matrix n n B),
    Eq (α := Matrix (m × n) (m × n) (A ⊗[R] B))
      (((kroneckerTMulAlgEquiv m n R S A B : Matrix m m A ⊗[R] Matrix n n B ≃ₐ[S] Matrix (m × n) (m × n) (A ⊗[R] B)) :
            (a : Matrix m m A ⊗[R] Matrix n n B) → Matrix (m × n) (m × n) (A ⊗[R] B))
          (star (x ⊗ₜ[R] y)) :
        Matrix (m × n) (m × n) (A ⊗[R] B))
      (star
          (((kroneckerTMulAlgEquiv m n R S A B :
                Matrix m m A ⊗[R] Matrix n n B ≃ₐ[S] Matrix (m × n) (m × n) (A ⊗[R] B)) :
              (a : Matrix m m A ⊗[R] Matrix n n B) → Matrix (m × n) (m × n) (A ⊗[R] B))
            (x ⊗ₜ[R] y)) :
        Matrix (m × n) (m × n) (A ⊗[R] B))

Tactic:
simp [star_eq_conjTranspose, conjTranspose_kroneckerTMul]

Premises used: Matrix.star_eq_conjTranspose, Matrix.conjTranspose_kroneckerTMul
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Fintype n
inst_6 : DecidableEq n
inst_7 : CommSemiring S
inst_8 : Algebra R S
inst_9 : Algebra S A
inst_10 : IsScalarTower R S A
inst_11 : Fintype m
inst_12 : DecidableEq m
inst_13 : StarRing R
inst_14 : StarAddMonoid A
inst_15 : StarAddMonoid B
inst_16 : StarModule R A
inst_17 : StarModule R B
x : Matrix m m A ⊗[R] Matrix n n B
⊢ ∀ (x y : Matrix m m A ⊗[R] Matrix n n B),
    Eq (α := Matrix (m × n) (m × n) (A ⊗[R] B))
        (((kroneckerTMulAlgEquiv m n R S A B : Matrix m m A ⊗[R] Matrix n n B ≃ₐ[S] Matrix (m × n) (m × n) (A ⊗[R] B)) :
              (a : Matrix m m A ⊗[R] Matrix n n B) → Matrix (m × n) (m × n) (A ⊗[R] B))
            (star x) :
          Matrix (m × n) (m × n) (A ⊗[R] B))
        (star
            (((kroneckerTMulAlgEquiv m n R S A B :
                  Matrix m m A ⊗[R] Matrix n n B ≃ₐ[S] Matrix (m × n) (m × n) (A ⊗[R] B)) :
                (a : Matrix m m A ⊗[R] Matrix n n B) → Matrix (m × n) (m × n) (A ⊗[R] B))
              x) :
          Matrix (m × n) (m × n) (A ⊗[R] B)) →
      Eq (α := Matrix (m × n) (m × n) (A ⊗[R] B))
          (((kroneckerTMulAlgEquiv m n R S A B :
                  Matrix m m A ⊗[R] Matrix n n B ≃ₐ[S] Matrix (m × n) (m × n) (A ⊗[R] B)) :
                (a : Matrix m m A ⊗[R] Matrix n n B) → Matrix (m × n) (m × n) (A ⊗[R] B))
              (star y) :
            Matrix (m × n) (m × n) (A ⊗[R] B))
          (star
              (((kroneckerTMulAlgEquiv m n R S A B :
                    Matrix m m A ⊗[R] Matrix n n B ≃ₐ[S] Matrix (m × n) (m × n) (A ⊗[R] B)) :
                  (a : Matrix m m A ⊗[R] Matrix n n B) → Matrix (m × n) (m × n) (A ⊗[R] B))
                y) :
            Matrix (m × n) (m × n) (A ⊗[R] B)) →
        Eq (α := Matrix (m × n) (m × n) (A ⊗[R] B))
          (((kroneckerTMulAlgEquiv m n R S A B :
                  Matrix m m A ⊗[R] Matrix n n B ≃ₐ[S] Matrix (m × n) (m × n) (A ⊗[R] B)) :
                (a : Matrix m m A ⊗[R] Matrix n n B) → Matrix (m × n) (m × n) (A ⊗[R] B))
              (star (x + y)) :
            Matrix (m × n) (m × n) (A ⊗[R] B))
          (star
              (((kroneckerTMulAlgEquiv m n R S A B :
                    Matrix m m A ⊗[R] Matrix n n B ≃ₐ[S] Matrix (m × n) (m × n) (A ⊗[R] B)) :
                  (a : Matrix m m A ⊗[R] Matrix n n B) → Matrix (m × n) (m × n) (A ⊗[R] B))
                (x + y)) :
            Matrix (m × n) (m × n) (A ⊗[R] B))

Tactic:
simp_all
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Fintype n
inst_6 : DecidableEq n
inst_7 : CommSemiring S
inst_8 : Algebra R S
inst_9 : Algebra S A
inst_10 : IsScalarTower R S A
inst_11 : Fintype m
inst_12 : DecidableEq m
inst_13 : StarRing R
inst_14 : StarAddMonoid A
inst_15 : StarAddMonoid B
inst_16 : StarModule R A
inst_17 : StarModule R B
⊢ Eq (α := Matrix m m A ⊗[R] Matrix n n B ≃ₐ[S] Matrix (m × n) (m × n) (A ⊗[R] B))
    (StarAlgEquiv.toAlgEquiv (kroneckerTMulStarAlgEquiv m n R S A B) :
      Matrix m m A ⊗[R] Matrix n n B ≃ₐ[S] Matrix (m × n) (m × n) (A ⊗[R] B))
    (kroneckerTMulAlgEquiv m n R S A B : Matrix m m A ⊗[R] Matrix n n B ≃ₐ[S] Matrix (m × n) (m × n) (A ⊗[R] B))

Tactic:
rfl

Premises used: StarAlgEquiv.toAlgEquiv, Matrix.kroneckerTMulAlgEquiv, AlgEquiv.ofLinearEquiv, rfl
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Fintype n
inst_6 : DecidableEq n
inst_7 : CommSemiring S
inst_8 : Algebra R S
inst_9 : Algebra S A
inst_10 : IsScalarTower R S A
inst_11 : Fintype m
inst_12 : DecidableEq m
inst_13 : StarRing R
inst_14 : StarAddMonoid A
inst_15 : StarAddMonoid B
inst_16 : StarModule R A
inst_17 : StarModule R B
x : Matrix m m A ⊗[R] Matrix n n B
⊢ Eq (α := Matrix (m × n) (m × n) (A ⊗[R] B))
    (((kroneckerTMulStarAlgEquiv m n R S A B :
            Matrix m m A ⊗[R] Matrix n n B ≃⋆ₐ[S] Matrix (m × n) (m × n) (A ⊗[R] B)) :
          (a : Matrix m m A ⊗[R] Matrix n n B) → Matrix (m × n) (m × n) (A ⊗[R] B))
        x :
      Matrix (m × n) (m × n) (A ⊗[R] B))
    (((kroneckerTMulLinearEquiv m m n n R S A B :
            Matrix m m A ⊗[R] Matrix n n B ≃ₗ[S] Matrix (m × n) (m × n) (A ⊗[R] B)) :
          (a : Matrix m m A ⊗[R] Matrix n n B) → Matrix (m × n) (m × n) (A ⊗[R] B))
        x :
      Matrix (m × n) (m × n) (A ⊗[R] B))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Fintype n
inst_6 : DecidableEq n
inst_7 : CommSemiring S
inst_8 : Algebra R S
inst_9 : Algebra S A
inst_10 : IsScalarTower R S A
inst_11 : Fintype m
inst_12 : DecidableEq m
inst_13 : StarRing R
inst_14 : StarAddMonoid A
inst_15 : StarAddMonoid B
inst_16 : StarModule R A
inst_17 : StarModule R B
x : Matrix (m × n) (m × n) (A ⊗[R] B)
⊢ Eq (α := Matrix m m A ⊗[R] Matrix n n B)
    (((StarAlgEquiv.symm (kroneckerTMulStarAlgEquiv m n R S A B) :
            Matrix (m × n) (m × n) (A ⊗[R] B) ≃⋆ₐ[S] Matrix m m A ⊗[R] Matrix n n B) :
          (a : Matrix (m × n) (m × n) (A ⊗[R] B)) → Matrix m m A ⊗[R] Matrix n n B)
        x :
      Matrix m m A ⊗[R] Matrix n n B)
    (((LinearEquiv.symm (kroneckerTMulLinearEquiv m m n n R S A B) :
            Matrix (m × n) (m × n) (A ⊗[R] B) ≃ₗ[S] Matrix m m A ⊗[R] Matrix n n B) :
          (a : Matrix (m × n) (m × n) (A ⊗[R] B)) → Matrix m m A ⊗[R] Matrix n n B)
        x :
      Matrix m m A ⊗[R] Matrix n n B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
inst_3 : Fintype m
inst_4 : DecidableEq m
⊢ Eq (α := Matrix m m R ⊗[R] Matrix n n R ≃ₗ[R] Matrix (m × n) (m × n) R)
    (↑(kroneckerAlgEquiv m n R) : Matrix m m R ⊗[R] Matrix n n R ≃ₗ[R] Matrix (m × n) (m × n) R)
    (kroneckerLinearEquiv m m n n R)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, kroneckerLinearEquiv, AlgEquiv.toLinearEquiv, LinearEquiv.toEquiv, Matrix.map, TensorProduct.tmul, LinearEquiv.trans, AddCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
inst_3 : Fintype m
inst_4 : DecidableEq m
x : Matrix m m R ⊗[R] Matrix n n R
⊢ Eq (α := Matrix (m × n) (m × n) R)
    ((kroneckerAlgEquiv m n R : (a : Matrix m m R ⊗[R] Matrix n n R) → Matrix (m × n) (m × n) R) x :
      Matrix (m × n) (m × n) R)
    ((kroneckerLinearEquiv m m n n R : (a : Matrix m m R ⊗[R] Matrix n n R) → Matrix (m × n) (m × n) R) x :
      Matrix (m × n) (m × n) R)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Matrix.map, rfl
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
inst_3 : Fintype m
inst_4 : DecidableEq m
x : Matrix (m × n) (m × n) R
⊢ Eq (α := Matrix m m R ⊗[R] Matrix n n R)
    ((AlgEquiv.symm (kroneckerAlgEquiv m n R) : (a : Matrix (m × n) (m × n) R) → Matrix m m R ⊗[R] Matrix n n R) x :
      Matrix m m R ⊗[R] Matrix n n R)
    ((LinearEquiv.symm (kroneckerLinearEquiv m m n n R) :
          (a : Matrix (m × n) (m × n) R) → Matrix m m R ⊗[R] Matrix n n R)
        x :
      Matrix m m R ⊗[R] Matrix n n R)

Tactic:
rfl

Premises used: Matrix.map, TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Fintype n
inst_6 : DecidableEq n
inst_7 : CommSemiring S
inst_8 : Algebra R S
inst_9 : Algebra S A
inst_10 : IsScalarTower R S A
inst_11 : Fintype m
inst_12 : DecidableEq m
inst_13 : StarRing R
x : Matrix m m R ⊗[R] Matrix n n R
⊢ Eq (α := Matrix (m × n) (m × n) R)
    ((kroneckerAlgEquiv m n R : (a : Matrix m m R ⊗[R] Matrix n n R) → Matrix (m × n) (m × n) R) (star 0))
    (star ((kroneckerAlgEquiv m n R : (a : Matrix m m R ⊗[R] Matrix n n R) → Matrix (m × n) (m × n) R) 0))

Tactic:
simp
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Fintype n
inst_6 : DecidableEq n
inst_7 : CommSemiring S
inst_8 : Algebra R S
inst_9 : Algebra S A
inst_10 : IsScalarTower R S A
inst_11 : Fintype m
inst_12 : DecidableEq m
inst_13 : StarRing R
x : Matrix m m R ⊗[R] Matrix n n R
⊢ ∀ (x : Matrix m m R) (y : Matrix n n R),
    Eq (α := Matrix (m × n) (m × n) R)
      ((kroneckerAlgEquiv m n R : (a : Matrix m m R ⊗[R] Matrix n n R) → Matrix (m × n) (m × n) R) (star (x ⊗ₜ[R] y)) :
        Matrix (m × n) (m × n) R)
      (star ((kroneckerAlgEquiv m n R : (a : Matrix m m R ⊗[R] Matrix n n R) → Matrix (m × n) (m × n) R) (x ⊗ₜ[R] y)) :
        Matrix (m × n) (m × n) R)

Tactic:
simp [star_eq_conjTranspose, conjTranspose_kronecker]

Premises used: Matrix.star_eq_conjTranspose, Matrix.conjTranspose_kronecker
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Fintype n
inst_6 : DecidableEq n
inst_7 : CommSemiring S
inst_8 : Algebra R S
inst_9 : Algebra S A
inst_10 : IsScalarTower R S A
inst_11 : Fintype m
inst_12 : DecidableEq m
inst_13 : StarRing R
x : Matrix m m R ⊗[R] Matrix n n R
⊢ ∀ (x y : Matrix m m R ⊗[R] Matrix n n R),
    Eq (α := Matrix (m × n) (m × n) R)
        ((kroneckerAlgEquiv m n R : (a : Matrix m m R ⊗[R] Matrix n n R) → Matrix (m × n) (m × n) R) (star x) :
          Matrix (m × n) (m × n) R)
        (star ((kroneckerAlgEquiv m n R : (a : Matrix m m R ⊗[R] Matrix n n R) → Matrix (m × n) (m × n) R) x) :
          Matrix (m × n) (m × n) R) →
      Eq (α := Matrix (m × n) (m × n) R)
          ((kroneckerAlgEquiv m n R : (a : Matrix m m R ⊗[R] Matrix n n R) → Matrix (m × n) (m × n) R) (star y) :
            Matrix (m × n) (m × n) R)
          (star ((kroneckerAlgEquiv m n R : (a : Matrix m m R ⊗[R] Matrix n n R) → Matrix (m × n) (m × n) R) y) :
            Matrix (m × n) (m × n) R) →
        Eq (α := Matrix (m × n) (m × n) R)
          ((kroneckerAlgEquiv m n R : (a : Matrix m m R ⊗[R] Matrix n n R) → Matrix (m × n) (m × n) R) (star (x + y)) :
            Matrix (m × n) (m × n) R)
          (star ((kroneckerAlgEquiv m n R : (a : Matrix m m R ⊗[R] Matrix n n R) → Matrix (m × n) (m × n) R) (x + y)) :
            Matrix (m × n) (m × n) R)

Tactic:
simp_all
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
inst_3 : Fintype m
inst_4 : DecidableEq m
inst_5 : StarRing R
⊢ Eq (α := Matrix m m R ⊗[R] Matrix n n R ≃ₐ[R] Matrix (m × n) (m × n) R)
    (StarAlgEquiv.toAlgEquiv (kroneckerStarAlgEquiv m n R)) (kroneckerAlgEquiv m n R)

Tactic:
rfl

Premises used: StarAlgEquiv.toAlgEquiv, Equiv.trans, AlgEquiv.trans, Matrix.kroneckerAlgEquiv, rfl
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
inst_3 : Fintype m
inst_4 : DecidableEq m
inst_5 : StarRing R
x : Matrix m m R ⊗[R] Matrix n n R
⊢ Eq (α := Matrix (m × n) (m × n) R)
    (((kroneckerStarAlgEquiv m n R : Matrix m m R ⊗[R] Matrix n n R ≃⋆ₐ[R] Matrix (m × n) (m × n) R) :
          (a : Matrix m m R ⊗[R] Matrix n n R) → Matrix (m × n) (m × n) R)
        x :
      Matrix (m × n) (m × n) R)
    ((kroneckerLinearEquiv m m n n R : (a : Matrix m m R ⊗[R] Matrix n n R) → Matrix (m × n) (m × n) R) x :
      Matrix (m × n) (m × n) R)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Matrix.map, rfl
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
inst_3 : Fintype m
inst_4 : DecidableEq m
inst_5 : StarRing R
x : Matrix (m × n) (m × n) R
⊢ Eq (α := Matrix m m R ⊗[R] Matrix n n R)
    (((StarAlgEquiv.symm (kroneckerStarAlgEquiv m n R) :
            Matrix (m × n) (m × n) R ≃⋆ₐ[R] Matrix m m R ⊗[R] Matrix n n R) :
          (a : Matrix (m × n) (m × n) R) → Matrix m m R ⊗[R] Matrix n n R)
        x :
      Matrix m m R ⊗[R] Matrix n n R)
    ((LinearEquiv.symm (kroneckerLinearEquiv m m n n R) :
          (a : Matrix (m × n) (m × n) R) → Matrix m m R ⊗[R] Matrix n n R)
        x :
      Matrix m m R ⊗[R] Matrix n n R)

Tactic:
rfl

Premises used: Matrix.map, TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
⊢ Eq (α := Matrix.{w, w, u_1} n n R[X])
    ((AlgEquiv.symm matPolyEquiv : (a : (Matrix n n R)[X]) → Matrix n n R[X])
        ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M) :
      Matrix.{w, w, u_1} n n R[X])
    (M.map (⇑C : (a : R) → R[X]) : Matrix.{w, w, u_1} n n R[X])

Tactic:
simp [matPolyEquiv]

Premises used: matPolyEquiv
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
rw :
  Eq (α := (Matrix n n R)[X])
    ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X])
        ((AlgEquiv.symm matPolyEquiv : (a : (Matrix n n R)[X]) → Matrix n n R[X])
          ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M)) :
      (Matrix n n R)[X])
    ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M : (Matrix n n R)[X])
rw₁ rw₂ :
  Eq (α := (Matrix n n R)[X]) ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M : (Matrix n n R)[X])
    ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M : (Matrix n n R)[X])
⊢ Eq (α := (Matrix n n R)[X])
    ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (M.map (⇑C : (a : R) → R[X])) : (Matrix n n R)[X])
    ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M : (Matrix n n R)[X])

Tactic:
rw [← matPolyEquiv_symm_C, AlgEquiv.apply_symm_apply]

Premises used: AlgEquiv.apply_symm_apply, matPolyEquiv_symm_C
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
⊢ Eq (α := Matrix.{w, w, u_1} n n R[X])
    ((AlgEquiv.symm matPolyEquiv : (a : (Matrix n n R)[X]) → Matrix n n R[X]) X : Matrix.{w, w, u_1} n n R[X])
    (diagonal fun (x : n) ↦ X : Matrix.{w, w, u_1} n n R[X])

Tactic:
simp [matPolyEquiv, Matrix.smul_one_eq_diagonal]

Premises used: Matrix.smul_one_eq_diagonal, matPolyEquiv
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
rw :
  Eq (α := (Matrix n n R)[X])
    ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X])
        ((AlgEquiv.symm matPolyEquiv : (a : (Matrix n n R)[X]) → Matrix n n R[X]) X) :
      (Matrix n n R)[X])
    (X : (Matrix n n R)[X])
rw₁ rw₂ : Eq (α := (Matrix n n R)[X]) X X
⊢ Eq (α := (Matrix n n R)[X])
    ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (diagonal fun (x : n) ↦ X) : (Matrix n n R)[X])
    (X : (Matrix n n R)[X])

Tactic:
rw [← matPolyEquiv_symm_X, AlgEquiv.apply_symm_apply]

Premises used: AlgEquiv.apply_symm_apply, matPolyEquiv_symm_X
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
i j : n
k : ℕ
x : R
simp :
  Eq (α := (Matrix n n R)[X])
    ((AlgEquiv.symm (polyEquivTensor R (Matrix n n R)) : (a : Matrix n n R ⊗[R] R[X]) → (Matrix n n R)[X])
        (((Algebra.TensorProduct.comm R R[X] (Matrix n n R) : R[X] ⊗[R] Matrix n n R ≃ₐ[R] Matrix n n R ⊗[R] R[X]) :
            (a : R[X] ⊗[R] Matrix n n R) → Matrix n n R ⊗[R] R[X])
          ((monomial k : (a : R) → R[X]) x ⊗ₜ[R] single i j 1)) :
      (Matrix n n R)[X])
    ((monomial k : (a : Matrix n n R) → (Matrix n n R)[X]) (single i j x) : (Matrix n n R)[X])
⊢ Eq (α := (Matrix n n R)[X])
    ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (single i j ((monomial k : (a : R) → R[X]) x)) :
      (Matrix n n R)[X])
    ((monomial k : (a : Matrix n n R) → (Matrix n n R)[X]) (single i j x) : (Matrix n n R)[X])

Tactic:
simp only [matPolyEquiv, AlgEquiv.trans_apply, matrixEquivTensor_apply_single]

Premises used: matPolyEquiv, matrixEquivTensor_apply_single, AlgEquiv.trans_apply
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
i j : n
k : ℕ
x : R
a :
  Eq (α := Matrix n n R ⊗[R] R[X])
    ((polyEquivTensor R (Matrix n n R) : (a : (Matrix n n R)[X]) → Matrix n n R ⊗[R] R[X])
        ((AlgEquiv.symm (polyEquivTensor R (Matrix n n R)) : (a : Matrix n n R ⊗[R] R[X]) → (Matrix n n R)[X])
          (((Algebra.TensorProduct.comm R R[X] (Matrix n n R) : R[X] ⊗[R] Matrix n n R ≃ₐ[R] Matrix n n R ⊗[R] R[X]) :
              (a : R[X] ⊗[R] Matrix n n R) → Matrix n n R ⊗[R] R[X])
            ((monomial k : (a : R) → R[X]) x ⊗ₜ[R] single i j 1))) :
      Matrix n n R ⊗[R] R[X])
    ((polyEquivTensor R (Matrix n n R) : (a : (Matrix n n R)[X]) → Matrix n n R ⊗[R] R[X])
        ((monomial k : (a : Matrix n n R) → (Matrix n n R)[X]) (single i j x)) :
      Matrix n n R ⊗[R] R[X])
⊢ Eq (α := (Matrix n n R)[X])
    ((AlgEquiv.symm (polyEquivTensor R (Matrix n n R)) : (a : Matrix n n R ⊗[R] R[X]) → (Matrix n n R)[X])
        (((Algebra.TensorProduct.comm R R[X] (Matrix n n R) : R[X] ⊗[R] Matrix n n R ≃ₐ[R] Matrix n n R ⊗[R] R[X]) :
            (a : R[X] ⊗[R] Matrix n n R) → Matrix n n R ⊗[R] R[X])
          ((monomial k : (a : R) → R[X]) x ⊗ₜ[R] single i j 1)) :
      (Matrix n n R)[X])
    ((monomial k : (a : Matrix n n R) → (Matrix n n R)[X]) (single i j x) : (Matrix n n R)[X])

Tactic:
apply (polyEquivTensor R (Matrix n n R)).injective

Premises used: Matrix, polyEquivTensor, AlgEquiv.injective