-- Mathlib/RingTheory/PolynomialAlgebra.lean
theorem matPolyEquiv_coeff_apply_aux_1 (i j : n) (k : ℕ) (x : R) :
    matPolyEquiv (stdBasisMatrix i j <| monomial k x) = monomial k (stdBasisMatrix i j x)

Proof state:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
⊢ matPolyEquiv (stdBasisMatrix i j ((monomial k) x)) = (monomial k) (stdBasisMatrix i j x)

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

Result:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
⊢ (polyEquivTensor R (Matrix n n R)).symm
      ((Algebra.TensorProduct.comm R R[X] (Matrix n n R)) ((monomial k) x ⊗ₜ[R] stdBasisMatrix i j 1)) =
    (monomial k) (stdBasisMatrix i j x)

Proof state:
case a
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
⊢ stdBasisMatrix i j 1 ⊗ₜ[R] (monomial k) x = ↑includeLeft (stdBasisMatrix i j x) * 1 ⊗ₜ[R] X ^ k

Tactic:
simp only [Algebra.TensorProduct.tmul_mul_tmul, one_pow, one_mul, Matrix.mul_one,
  Algebra.TensorProduct.tmul_pow, Algebra.TensorProduct.includeLeft_apply]

Result:
case a
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
⊢ stdBasisMatrix i j 1 ⊗ₜ[R] (monomial k) x = ↑includeLeft (stdBasisMatrix i j x) * 1 ⊗ₜ[R] (X ^ k)

Proof state:
case a
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
⊢ stdBasisMatrix i j 1 ⊗ₜ[R] (monomial k) x = ↑includeLeft (stdBasisMatrix i j x) * 1 ⊗ₜ[R] (X ^ k)

Tactic:
rw [← smul_X_eq_monomial, ← TensorProduct.smul_tmul]

Result:
case a
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
⊢ (x • stdBasisMatrix i j 1) ⊗ₜ[R] (X ^ k) = ↑includeLeft (stdBasisMatrix i j x) * 1 ⊗ₜ[R] (X ^ k)

Proof state:
case a
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
⊢ (x • stdBasisMatrix i j 1) ⊗ₜ[R] (X ^ k) = ↑includeLeft (stdBasisMatrix i j x) * 1 ⊗ₜ[R] (X ^ k)

Tactic:
congr with i' <;> simp [stdBasisMatrix]

Result:
no goals

Proof state:
case a
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
⊢ (polyEquivTensor R (Matrix n n R))
      ((polyEquivTensor R (Matrix n n R)).symm
        ((Algebra.TensorProduct.comm R R[X] (Matrix n n R)) ((monomial k) x ⊗ₜ[R] stdBasisMatrix i j 1))) =
    (polyEquivTensor R (Matrix n n R)) ((monomial k) (stdBasisMatrix i j x))

Tactic:
simp only [AlgEquiv.apply_symm_apply,Algebra.TensorProduct.comm_tmul,
  polyEquivTensor_apply, eval₂_monomial]

Result:
case a
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
⊢ stdBasisMatrix i j 1 ⊗ₜ[R] (monomial k) x = ↑includeLeft (stdBasisMatrix i j x) * 1 ⊗ₜ[R] X ^ k

Proof state:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
⊢ (polyEquivTensor R (Matrix n n R)).symm
      ((Algebra.TensorProduct.comm R R[X] (Matrix n n R)) ((monomial k) x ⊗ₜ[R] stdBasisMatrix i j 1)) =
    (monomial k) (stdBasisMatrix i j x)

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

Result:
case a
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
⊢ (polyEquivTensor R (Matrix n n R))
      ((polyEquivTensor R (Matrix n n R)).symm
        ((Algebra.TensorProduct.comm R R[X] (Matrix n n R)) ((monomial k) x ⊗ₜ[R] stdBasisMatrix i j 1))) =
    (polyEquivTensor R (Matrix n n R)) ((monomial k) (stdBasisMatrix i j x))