awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst : CommSemiring R
inst_1 : Fintype l
inst_2 : Fintype m
inst_3 : Fintype n
inst_4 : Fintype p
inst_5 : DecidableEq l
inst_6 : DecidableEq m
inst_7 : DecidableEq n
inst_8 : DecidableEq p
x : Matrix l m R
y : Matrix n p R
⊢ Eq (α := Matrix (l × n) (m × p) R)
    ((kroneckerLinearEquiv l m n p R : (a : Matrix l m R ⊗[R] Matrix n p R) → Matrix (l × n) (m × p) R) (x ⊗ₜ[R] y) :
      Matrix (l × n) (m × p) R)
    (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) x y : Matrix (l × n) (m × p) R)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, Matrix.kroneckerMap, Matrix.map, FreeAddMonoid.sumAux, 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
inst : CommSemiring R
inst_1 : Fintype l
inst_2 : Fintype m
inst_3 : Fintype n
inst_4 : Fintype p
inst_5 : DecidableEq l
inst_6 : DecidableEq m
inst_7 : DecidableEq n
inst_8 : DecidableEq p
x : Matrix l m R
y : Matrix n p R
⊢ Eq (α := Matrix l m R ⊗[R] Matrix n p R)
    ((LinearEquiv.symm (kroneckerLinearEquiv l m n p R) :
          (a : Matrix (l × n) (m × p) R) → Matrix l m R ⊗[R] Matrix n p R)
        (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) x y) :
      Matrix l m R ⊗[R] Matrix n p R)
    (x ⊗ₜ[R] y : Matrix l m R ⊗[R] Matrix n p R)

Tactic:
simp [LinearEquiv.symm_apply_eq]

Premises used: LinearEquiv.symm_apply_eq
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
a : A
m : Matrix n n R
⊢ (((toFunBilinear n R A : (a : A) → Matrix n n R →ₗ[R] Matrix n n A) a : Matrix n n R →ₗ[R] Matrix n n A) :
        (a : Matrix n n R) → Matrix n n A)
      m =
    HSMul.hSMul (β := Matrix n n A) a (m.map (⇑(algebraMap R A) : (a : R) → A))

Tactic:
rfl

Premises used: Matrix.map, 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 : DecidableEq n
inst_6 : Fintype n
a₁ a₂ : A
b₁ b₂ : Matrix n n R
simp_rw :
  (a₁ * a₂) •
      HMul.hMul (α := Matrix n n A) (b₁.map (⇑(algebraMap R A) : (a : R) → A))
        (b₂.map (⇑(algebraMap R A) : (a : R) → A)) =
    HSMul.hSMul (β := Matrix n n A) a₁ (b₁.map (⇑(algebraMap R A) : (a : R) → A)) *
      HSMul.hSMul (β := Matrix n n A) a₂ (b₂.map (⇑(algebraMap R A) : (a : R) → A))
⊢ (toFunLinear n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
    HMul.hMul (α := Matrix n n A) (β := Matrix n n A)
      ((toFunLinear n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) (a₁ ⊗ₜ[R] b₁) : Matrix n n A)
      ((toFunLinear n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) (a₂ ⊗ₜ[R] b₂) : Matrix n n A)

Tactic:
simp_rw [toFunLinear, lift.tmul, toFunBilinear_apply, Matrix.map_mul]

Premises used: MatrixEquivTensor.toFunBilinear_apply, TensorProduct.lift.tmul, Matrix.map_mul, MatrixEquivTensor.toFunLinear
-- 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 : DecidableEq n
inst_6 : Fintype n
a₁ a₂ : A
b₁ b₂ : Matrix n n R
a :
  ∀ (i j : n),
    ((a₁ * a₂) •
          HMul.hMul (α := Matrix n n A) (b₁.map (⇑(algebraMap R A) : (a : R) → A))
            (b₂.map (⇑(algebraMap R A) : (a : R) → A)))
        i j =
      (HSMul.hSMul (β := Matrix n n A) a₁ (b₁.map (⇑(algebraMap R A) : (a : R) → A)) *
          HSMul.hSMul (β := Matrix n n A) a₂ (b₂.map (⇑(algebraMap R A) : (a : R) → A)))
        i j
⊢ (a₁ * a₂) •
      HMul.hMul (α := Matrix n n A) (b₁.map (⇑(algebraMap R A) : (a : R) → A))
        (b₂.map (⇑(algebraMap R A) : (a : R) → A)) =
    HSMul.hSMul (β := Matrix n n A) a₁ (b₁.map (⇑(algebraMap R A) : (a : R) → A)) *
      HSMul.hSMul (β := Matrix n n A) a₂ (b₂.map (⇑(algebraMap R A) : (a : R) → A))

Tactic:
ext
-- 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 : DecidableEq n
inst_6 : Fintype n
a₁ a₂ : A
b₁ b₂ : Matrix n n R
i j : n
a :
  a₁ * a₂ *
      HMul.hMul (α := Matrix n n A) (β := Matrix n n A) (b₁.map (⇑(algebraMap R A) : (a : R) → A))
        (b₂.map (⇑(algebraMap R A) : (a : R) → A)) i j =
    (HSMul.hSMul (β := Matrix n n A) a₁ (b₁.map (⇑(algebraMap R A) : (a : R) → A)) *
        HSMul.hSMul (β := Matrix n n A) a₂ (b₂.map (⇑(algebraMap R A) : (a : R) → A)))
      i j
⊢ ((a₁ * a₂) •
        HMul.hMul (α := Matrix n n A) (b₁.map (⇑(algebraMap R A) : (a : R) → A))
          (b₂.map (⇑(algebraMap R A) : (a : R) → A)))
      i j =
    (HSMul.hSMul (β := Matrix n n A) a₁ (b₁.map (⇑(algebraMap R A) : (a : R) → A)) *
        HSMul.hSMul (β := Matrix n n A) a₂ (b₂.map (⇑(algebraMap R A) : (a : R) → A)))
      i j

Tactic:
dsimp
-- 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 : DecidableEq n
inst_6 : Fintype n
simp_rw :
  Eq (α := Matrix n n A)
    ((TensorProduct.lift (toFunBilinear n R A) : (a : A ⊗[R] Matrix n n R) → Matrix n n A) (1 ⊗ₜ[R] 1) : Matrix n n A)
    (1 : Matrix n n A)
simp_rw₁ :
  Eq (α := Matrix n n A)
    (((toFunBilinear n R A : (a : A) → Matrix n n R →ₗ[R] Matrix n n A) 1 : (a : Matrix n n R) → Matrix n n A) 1) 1
simp_rw₂ :
  HSMul.hSMul (α := A) (β := Matrix n n A) 1
      (Matrix.map.{u_5, u_7, u_3, u_3} (α := R) 1 (⇑(algebraMap R A) : (a : R) → A)) =
    1
simp_rw₃ : HSMul.hSMul (α := A) (β := Matrix n n A) 1 1 = 1
⊢ Eq (α := Matrix n n A) ((toFunLinear n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) (1 ⊗ₜ[R] 1) : Matrix n n A)
    (1 : Matrix n n A)

Tactic:
simp_rw [toFunLinear, lift.tmul, toFunBilinear_apply,
        Matrix.map_one (algebraMap R A) (map_zero _) (map_one _), one_smul]

Premises used: Algebra.algebraMap, MatrixEquivTensor.toFunBilinear_apply, Matrix.map_one, map_zero, TensorProduct.lift.tmul, one_smul, map_one, DFunLike.coe, MatrixEquivTensor.toFunLinear
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
a : A
m : Matrix n n R
⊢ (toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) (a ⊗ₜ[R] m) =
    HSMul.hSMul (β := Matrix n n A) a (m.map (⇑(algebraMap R A) : (a : R) → A))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, Matrix.map, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
⊢ Eq (α := A ⊗[R] Matrix n n R) (invFun n R A 0) 0

Tactic:
simp [invFun]

Premises used: MatrixEquivTensor.invFun
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
M N : Matrix n n A
⊢ invFun n R A (M + N) = HAdd.hAdd (α := A ⊗[R] Matrix n n R) (invFun n R A M) (invFun n R A N)

Tactic:
simp [invFun, add_tmul, Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib, MatrixEquivTensor.invFun, TensorProduct.add_tmul
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
a : A
M : Matrix n n A
⊢ invFun n R A (a • M) = HMul.hMul (α := A ⊗[R] Matrix n n R) (a ⊗ₜ[R] 1) (invFun n R A M)

Tactic:
simp [invFun, Finset.mul_sum]

Premises used: Finset.mul_sum, MatrixEquivTensor.invFun
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix n n R
dsimp :
  Eq (α := A ⊗[R] Matrix n n R) (∑ p : n × n, (algebraMap R A : (a : R) → A) (M p.1 p.2) ⊗ₜ[R] single p.1 p.2 1)
    (1 ⊗ₜ[R] M)
⊢ Eq (α := A ⊗[R] Matrix n n R) (invFun n R A (M.map (⇑(algebraMap R A) : (a : R) → A))) (1 ⊗ₜ[R] M)

Tactic:
dsimp [invFun]

Premises used: MatrixEquivTensor.invFun
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix n n R
simp :
  Eq (α := A ⊗[R] Matrix n n R) (1 ⊗ₜ[R] ∑ a : n × n, HSMul.hSMul (β := Matrix n n R) (M a.1 a.2) (single a.1 a.2 1))
    (1 ⊗ₜ[R] M)
⊢ Eq (α := A ⊗[R] Matrix n n R) (∑ p : n × n, (algebraMap R A : (a : R) → A) (M p.1 p.2) ⊗ₜ[R] single p.1 p.2 1)
    (1 ⊗ₜ[R] M)

Tactic:
simp only [Algebra.algebraMap_eq_smul_one, smul_tmul, ← tmul_sum]

Premises used: TensorProduct.smul_tmul, TensorProduct.tmul_sum, Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix n n R
e_n : ∑ a : n × n, HSMul.hSMul (β := Matrix n n R) (M a.1 a.2) (single a.1 a.2 1) = M
⊢ Eq (α := A ⊗[R] Matrix n n R) (1 ⊗ₜ[R] ∑ a : n × n, HSMul.hSMul (β := Matrix n n R) (M a.1 a.2) (single a.1 a.2 1))
    (1 ⊗ₜ[R] M)

Tactic:
congr
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix n n R
rw : ∑ i : n, ∑ j : n, single i j (M i j)
| M

Tactic:
rw [matrix_eq_sum_single M]

Premises used: Matrix.matrix_eq_sum_single
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix n n R
e_n :
  Eq (α := Matrix n n R) (∑ a : n × n, HSMul.hSMul (β := Matrix n n R) (M a.1 a.2) (single a.1 a.2 1))
    (∑ i : n, ∑ j : n, single i j (M i j))
⊢ ∑ a : n × n, HSMul.hSMul (β := Matrix n n R) (M a.1 a.2) (single a.1 a.2 1) = M

Tactic:
conv_rhs => rw [matrix_eq_sum_single M]

Premises used: Matrix.matrix_eq_sum_single
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix n n R
⊢ Eq (α := Matrix n n R)
    (∑ x ∈ SProd.sprod (α := Finset n) (β := Finset n) Finset.univ Finset.univ,
      HSMul.hSMul (β := Matrix n n R) (M x.1 x.2) (single x.1 x.2 1))
    (∑ x : n, ∑ y : n, HSMul.hSMul (β := Matrix n n R) (M (x, y).1 (x, y).2) (single (x, y).1 (x, y).2 1))

Tactic:
Finset.sum_product (β := Matrix n n R) ..

Premises used: Finset.sum_product
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix n n R
h :
  ∀ (x : n),
    Membership.mem (γ := Finset n) Finset.univ x →
      ∀ (x_1 : n),
        Membership.mem (γ := Finset n) Finset.univ x_1 →
          single x x_1 (M x x_1) =
            HSMul.hSMul (β := Matrix n n R) (M (x, x_1).1 (x, x_1).2) (single (x, x_1).1 (x, x_1).2 1)
⊢ Eq (α := Matrix n n R) (∑ a : n × n, HSMul.hSMul (β := Matrix n n R) (M a.1 a.2) (single a.1 a.2 1))
    (∑ i : n, ∑ j : n, single i j (M i j))

Tactic:
convert! Finset.sum_product (β := Matrix n n R) ..

Premises used: Finset.sum_product
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix n n R
x : n
h : Membership.mem (γ := Finset n) Finset.univ x
x_1 : n
h_1 : Membership.mem (γ := Finset n) Finset.univ x_1
⊢ single x x_1 (M x x_1) = HSMul.hSMul (β := Matrix n n R) (M (x, x_1).1 (x, x_1).2) (single (x, x_1).1 (x, x_1).2 1)

Tactic:
simp
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix n n A
simp :
  ∑ x : n × n,
      HSMul.hSMul (β := Matrix n n A) (M x.1 x.2)
        (Matrix.map.{u_5, u_7, u_3, u_3} (α := R) (single x.1 x.2 1) (⇑(algebraMap R A) : (a : R) → A)) =
    M
⊢ (toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) (invFun n R A M) = M

Tactic:
simp only [invFun, map_sum, toFunAlgHom_apply]

Premises used: MatrixEquivTensor.invFun, map_sum, MatrixEquivTensor.toFunAlgHom_apply
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix n n A
⊢ Eq (α := Matrix n n A)
    (∑ x ∈ SProd.sprod (α := Finset n) (β := Finset n) Finset.univ Finset.univ,
      HSMul.hSMul (β := Matrix n n A) (M x.1 x.2)
        (Matrix.map.{u_5, u_7, u_3, u_3} (α := R) (single x.1 x.2 1) (⇑(algebraMap R A) : (a : R) → A)))
    (∑ x : n,
      ∑ y : n,
        HSMul.hSMul (β := Matrix n n A) (M (x, y).1 (x, y).2)
          (Matrix.map.{u_5, u_7, u_3, u_3} (α := R) (single (x, y).1 (x, y).2 1) (⇑(algebraMap R A) : (a : R) → A)))

Tactic:
Finset.sum_product (β := Matrix n n A) ..

Premises used: Finset.sum_product
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix n n A
h :
  M =
    ∑ x : n,
      ∑ y : n,
        HSMul.hSMul (β := Matrix n n A) (M (x, y).1 (x, y).2)
          (Matrix.map.{u_5, u_7, u_3, u_3} (α := R) (single (x, y).1 (x, y).2 1) (⇑(algebraMap R A) : (a : R) → A))
⊢ ∑ x : n × n,
      HSMul.hSMul (β := Matrix n n A) (M x.1 x.2)
        (Matrix.map.{u_5, u_7, u_3, u_3} (α := R) (single x.1 x.2 1) (⇑(algebraMap R A) : (a : R) → A)) =
    M

Tactic:
convert! Finset.sum_product (β := Matrix n n A) ..

Premises used: Finset.sum_product
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix n n A
rw : ∑ i : n, ∑ j : n, single i j (M i j)
| M

Tactic:
rw [matrix_eq_sum_single M]

Premises used: Matrix.matrix_eq_sum_single
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix n n A
h :
  Eq (α := Matrix n n A) (∑ i : n, ∑ j : n, single i j (M i j))
    (∑ x : n,
      ∑ y : n,
        HSMul.hSMul (β := Matrix n n A) (M (x, y).1 (x, y).2)
          (Matrix.map.{u_5, u_7, u_3, u_3} (α := R) (single (x, y).1 (x, y).2 1) (⇑(algebraMap R A) : (a : R) → A)))
⊢ M =
    ∑ x : n,
      ∑ y : n,
        HSMul.hSMul (β := Matrix n n A) (M (x, y).1 (x, y).2)
          (Matrix.map.{u_5, u_7, u_3, u_3} (α := R) (single (x, y).1 (x, y).2 1) (⇑(algebraMap R A) : (a : R) → A))

Tactic:
conv_lhs => rw [matrix_eq_sum_single M]

Premises used: Matrix.matrix_eq_sum_single
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
M : Matrix n n A
⊢ Eq (α := Matrix n n A) (∑ i : n, ∑ j : n, single i j (M i j))
    (∑ x : n,
      ∑ y : n,
        HSMul.hSMul (β := Matrix n n A) (M (x, y).1 (x, y).2)
          (Matrix.map.{u_5, u_7, u_3, u_3} (α := R) (single (x, y).1 (x, y).2 1) (⇑(algebraMap R A) : (a : R) → A)))

Tactic:
simp
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
⊢ Eq (α := A ⊗[R] Matrix n n R) (invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) 0)) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
a : A
m : Matrix n n R
⊢ Eq (α := A ⊗[R] Matrix n n R)
    (invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) (a ⊗ₜ[R] m))) (a ⊗ₜ[R] m)

Tactic:
simp
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
x y : A ⊗[R] Matrix n n R
hx : invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) x) = x
hy : invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) y) = y
add :
  invFun n R A
      (HAdd.hAdd (α := Matrix n n A) (β := Matrix n n A)
        ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) x : Matrix n n A)
        ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) y : Matrix n n A)) =
    x + y
⊢ invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) (x + y)) = x + y

Tactic:
rw [map_add]

Premises used: map_add
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
x y : A ⊗[R] Matrix n n R
hx : invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) x) = x
hy : invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) y) = y
rw :
  invFun n R A
    (HAdd.hAdd (α := Matrix n n A) (β := Matrix n n A)
      ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) x : Matrix n n A)
      ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) y : Matrix n n A))
| x + y

Tactic:
rw [← hx, ← hy, ← invFun_add]

Premises used: MatrixEquivTensor.invFun_add
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
x y : A ⊗[R] Matrix n n R
hx : invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) x) = x
hy : invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) y) = y
conv_rhs :
  invFun n R A
      (HAdd.hAdd (α := Matrix n n A) (β := Matrix n n A)
        ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) x : Matrix n n A)
        ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) y : Matrix n n A)) =
    x + y
add :
  Eq (α := A ⊗[R] Matrix n n R)
    (invFun n R A
      (HAdd.hAdd (α := Matrix n n A) (β := Matrix n n A)
        ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) x : Matrix n n A)
        ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) y : Matrix n n A)))
    (invFun n R A
      (HAdd.hAdd (α := Matrix n n A) (β := Matrix n n A)
        ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) x : Matrix n n A)
        ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) y : Matrix n n A)))
⊢ invFun n R A
      (HAdd.hAdd (α := Matrix n n A) (β := Matrix n n A)
        ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) x : Matrix n n A)
        ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) y : Matrix n n A)) =
    x + y

Tactic:
conv_rhs => rw [← hx, ← hy, ← invFun_add]

Premises used: MatrixEquivTensor.invFun_add
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
M : A ⊗[R] Matrix n n R
zero : Eq (α := A ⊗[R] Matrix n n R) (invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) 0)) 0
tmul :
  ∀ (a : A) (m : Matrix n n R),
    Eq (α := A ⊗[R] Matrix n n R)
      (invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) (a ⊗ₜ[R] m))) (a ⊗ₜ[R] m)
add :
  ∀ (x y : A ⊗[R] Matrix n n R)
    (hx : invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) x) = x)
    (hy : invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) y) = y),
    invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) (x + y)) = x + y
⊢ invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) M) = M

Tactic:
induction M with
  | zero => simp
  | tmul a m => simp
  | add x y hx hy =>
    rw [map_add]
    conv_rhs => rw [← hx, ← hy, ← invFun_add]

Premises used: Matrix.add, MatrixEquivTensor.invFun_add, map_add, TensorProduct.tmul, Matrix.zero
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Fintype n
inst_4 : DecidableEq n
M : Matrix n n A
⊢ Eq (α := A ⊗[R] Matrix n n R)
    ((matrixEquivTensor n R A : (a : Matrix n n A) → A ⊗[R] Matrix n n R) M : A ⊗[R] Matrix n n R)
    (∑ p : n × n, M p.1 p.2 ⊗ₜ[R] single p.1 p.2 1 : A ⊗[R] Matrix n n R)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, MatrixEquivTensor.invFun, Finset.sum, rfl
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Fintype n
inst_4 : DecidableEq n
i j : n
x : A
⊢ ∀ (p : n × n), i = p.1 ∧ j = p.2 ↔ p = (i, j)

Tactic:
aesop
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Fintype n
inst_4 : DecidableEq n
i j : n
x : A
⊢ ∀ (p : n × n), i = p.1 ∧ j = p.2 ↔ p = (i, j)

Tactic:
have t : ∀ p : n × n, i = p.1 ∧ j = p.2 ↔ p = (i, j) := by aesop
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Fintype n
inst_4 : DecidableEq n
i j : n
x : A
t : ∀ (p : n × n), i = p.1 ∧ j = p.2 ↔ p = (i, j)
⊢ Eq (α := A ⊗[R] Matrix n n R)
    ((matrixEquivTensor n R A : (a : Matrix n n A) → A ⊗[R] Matrix n n R) (single i j x) : A ⊗[R] Matrix n n R)
    (x ⊗ₜ[R] single i j 1 : A ⊗[R] Matrix n n R)

Tactic:
simp [ite_tmul, t, single]

Premises used: TensorProduct.ite_tmul, Matrix.single
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Fintype n
inst_4 : DecidableEq n
a : A
M : Matrix n n R
⊢ (AlgEquiv.symm (matrixEquivTensor n R A) : (a : A ⊗[R] Matrix n n R) → Matrix n n A) (a ⊗ₜ[R] M) =
    HSMul.hSMul (β := Matrix n n A) a (M.map (⇑(algebraMap R A) : (a : R) → A))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, Matrix.map, FreeAddMonoid.sumAux, rfl