awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  single i j 1 ⊗ₜ[R] (monomial k : (a : R) → R[X]) x =
    HMul.hMul (α := Matrix n n R ⊗[R] R[X])
      (((↑includeLeft : Matrix n n R →+* Matrix n n R ⊗[R] R[X]) : (a : Matrix n n R) → Matrix n n R ⊗[R] R[X])
          (single i j x) :
        Matrix n n R ⊗[R] R[X])
      (HPow.hPow (α := Matrix n n R ⊗[R] R[X]) (1 ⊗ₜ[R] X) k)
⊢ 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])

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

Premises used: Polynomial.eval₂_monomial, AlgEquiv.apply_symm_apply, polyEquivTensor_apply, Algebra.TensorProduct.comm_tmul
-- 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 :
  single i j 1 ⊗ₜ[R] (monomial k : (a : R) → R[X]) x =
    HMul.hMul (α := Matrix n n R ⊗[R] R[X]) (β := Matrix n n R ⊗[R] R[X])
      (((↑includeLeft : Matrix n n R →+* Matrix n n R ⊗[R] R[X]) : (a : Matrix n n R) → Matrix n n R ⊗[R] R[X])
          (single i j x) :
        Matrix n n R ⊗[R] R[X])
      (1 ⊗ₜ[R] HPow.hPow (α := R[X]) X k)
⊢ single i j 1 ⊗ₜ[R] (monomial k : (a : R) → R[X]) x =
    HMul.hMul (α := Matrix n n R ⊗[R] R[X])
      (((↑includeLeft : Matrix n n R →+* Matrix n n R ⊗[R] R[X]) : (a : Matrix n n R) → Matrix n n R ⊗[R] R[X])
          (single i j x) :
        Matrix n n R ⊗[R] R[X])
      (HPow.hPow (α := Matrix n n R ⊗[R] R[X]) (1 ⊗ₜ[R] X) k)

Tactic:
simp only [one_pow,
    Algebra.TensorProduct.tmul_pow]

Premises used: one_pow, Algebra.TensorProduct.tmul_pow
-- 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 :
  HSMul.hSMul (β := Matrix n n R) x (single i j 1) ⊗ₜ[R] HPow.hPow (α := R[X]) X k =
    HMul.hMul (α := Matrix n n R ⊗[R] R[X]) (β := Matrix n n R ⊗[R] R[X])
      (((↑includeLeft : Matrix n n R →+* Matrix n n R ⊗[R] R[X]) : (a : Matrix n n R) → Matrix n n R ⊗[R] R[X])
          (single i j x) :
        Matrix n n R ⊗[R] R[X])
      (1 ⊗ₜ[R] HPow.hPow (α := R[X]) X k)
⊢ single i j 1 ⊗ₜ[R] (monomial k : (a : R) → R[X]) x =
    HMul.hMul (α := Matrix n n R ⊗[R] R[X]) (β := Matrix n n R ⊗[R] R[X])
      (((↑includeLeft : Matrix n n R →+* Matrix n n R ⊗[R] R[X]) : (a : Matrix n n R) → Matrix n n R ⊗[R] R[X])
          (single i j x) :
        Matrix n n R ⊗[R] R[X])
      (1 ⊗ₜ[R] HPow.hPow (α := R[X]) X k)

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

Premises used: TensorProduct.smul_tmul, Polynomial.smul_X_eq_monomial
-- 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 :
  ∀ (i' j_1 : n),
    HSMul.hSMul (β := Matrix n n R) x (single i j 1) i' j_1 =
      ((((LinearMap.mul R (Matrix n n R) : (a : Matrix n n R) → Matrix n n R →ₗ[R] Matrix n n R) (single i j x, 1).1,
                (LinearMap.mul R R[X] : (a : R[X]) → R[X] →ₗ[R] R[X]) (single i j x, 1).2).1 :
            Matrix n n R →ₗ[R] Matrix n n R) :
          (a : Matrix n n R) → Matrix n n R)
        (1, HPow.hPow (α := R[X]) X k).1 i' j_1
a₁ :
  ∀ (i' : ℕ),
    (HPow.hPow (α := R[X]) X k).coeff i' =
      coeff
        (((((LinearMap.mul R (Matrix n n R) : (a : Matrix n n R) → Matrix n n R →ₗ[R] Matrix n n R) (single i j x, 1).1,
                  (LinearMap.mul R R[X] : (a : R[X]) → R[X] →ₗ[R] R[X]) (single i j x, 1).2) :
                (Matrix n n R →ₗ[R] Matrix n n R) × (R[X] →ₗ[R] R[X])).2 :
            (a : R[X]) → R[X])
          (1, HPow.hPow (α := R[X]) X k).2)
        i'
⊢ HSMul.hSMul (β := Matrix n n R) x (single i j 1) ⊗ₜ[R] HPow.hPow (α := R[X]) X k =
    HMul.hMul (α := Matrix n n R ⊗[R] R[X]) (β := Matrix n n R ⊗[R] R[X])
      (((↑includeLeft : Matrix n n R →+* Matrix n n R ⊗[R] R[X]) : (a : Matrix n n R) → Matrix n n R ⊗[R] R[X])
          (single i j x) :
        Matrix n n R ⊗[R] R[X])
      (1 ⊗ₜ[R] HPow.hPow (α := R[X]) X k)

Tactic:
congr with i'
-- 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
i' j_1 : n
⊢ HSMul.hSMul (β := Matrix n n R) x (single i j 1) i' j_1 =
    ((((LinearMap.mul R (Matrix n n R) : (a : Matrix n n R) → Matrix n n R →ₗ[R] Matrix n n R) (single i j x, 1).1,
              (LinearMap.mul R R[X] : (a : R[X]) → R[X] →ₗ[R] R[X]) (single i j x, 1).2).1 :
          Matrix n n R →ₗ[R] Matrix n n R) :
        (a : Matrix n n R) → Matrix n n R)
      (1, HPow.hPow (α := R[X]) X k).1 i' j_1

Tactic:
simp [single]

Premises used: Matrix.single
-- 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
i' : ℕ
⊢ (HPow.hPow (α := R[X]) X k).coeff i' =
    coeff
      (((((LinearMap.mul R (Matrix n n R) : (a : Matrix n n R) → Matrix n n R →ₗ[R] Matrix n n R) (single i j x, 1).1,
                (LinearMap.mul R R[X] : (a : R[X]) → R[X] →ₗ[R] R[X]) (single i j x, 1).2) :
              (Matrix n n R →ₗ[R] Matrix n n R) × (R[X] →ₗ[R] R[X])).2 :
          (a : R[X]) → R[X])
        (1, HPow.hPow (α := R[X]) X k).2)
      i'

Tactic:
simp [single]

Premises used: Matrix.single
-- 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
p : R[X]
k : ℕ
⊢ coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (single i j p)) k = single i j (p.coeff k)

Tactic:
Polynomial.induction_on' p ?_ ?_

Premises used: Polynomial.induction_on'
-- 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
p : R[X]
k : ℕ
refine_1 :
  ∀ (p q : R[X]),
    coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (single i j p)) k = single i j (p.coeff k) →
      coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (single i j q)) k = single i j (q.coeff k) →
        coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (single i j (p + q))) k =
          single i j ((p + q).coeff k)
refine_2 :
  ∀ (n_1 : ℕ) (a : R),
    Eq (α := Matrix n n R)
      (coeff
        ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (single i j ((monomial n_1 : (a : R) → R[X]) a))) k)
      (single i j (coeff ((monomial n_1 : (a : R) → R[X]) a) k))
⊢ coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (single i j p)) k = single i j (p.coeff k)

Tactic:
refine Polynomial.induction_on' p ?_ ?_
-- 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
p_1 : R[X]
k : ℕ
p q : R[X]
hp : coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (single i j p)) k = single i j (p.coeff k)
hq : coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (single i j q)) k = single i j (q.coeff k)
refine_1 :
  ∀ (i_1 j_1 : n),
    coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (single i j (p + q))) k i_1 j_1 =
      single i j ((p + q).coeff k) i_1 j_1
⊢ coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (single i j (p + q))) k =
    single i j ((p + q).coeff k)

Tactic:
ext
-- 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
p_1 : R[X]
k : ℕ
p q : R[X]
hp : coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (single i j p)) k = single i j (p.coeff k)
hq : coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (single i j q)) k = single i j (q.coeff k)
i_1 j_1 : n
⊢ coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (single i j (p + q))) k i_1 j_1 =
    single i j ((p + q).coeff k) i_1 j_1

Tactic:
simp [hp, hq, coeff_add, add_apply, single_add]

Premises used: Matrix.single_add, Matrix.add_apply, Polynomial.coeff_add
-- 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
p : R[X]
k_1 k : ℕ
x : R
refine_2 : (if k = k_1 then single i j x else 0) = single i j (if k = k_1 then x else 0)
⊢ Eq (α := Matrix n n R)
    (coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (single i j ((monomial k : (a : R) → R[X]) x)))
      k_1)
    (single i j (coeff ((monomial k : (a : R) → R[X]) x) k_1))

Tactic:
simp only [matPolyEquiv_coeff_apply_aux_1, coeff_monomial]

Premises used: matPolyEquiv_coeff_apply_aux_1, Polynomial.coeff_monomial
-- 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
p : R[X]
k_1 k : ℕ
x : R
pos : k = k_1 → single i j x = single i j x
neg : ¬k = k_1 → Eq (α := Matrix n n R) 0 (single i j 0)
⊢ (if k = k_1 then single i j x else 0) = single i j (if k = k_1 then x else 0)

Tactic:
split_ifs
-- 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
p : R[X]
k_1 k : ℕ
x : R
h : k = k_1
pos : ∀ (x_1 x_2 : n), single i j x x_1 x_2 = single i j x x_1 x_2
⊢ single i j x = single i j x

Tactic:
funext
-- 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
p : R[X]
k_1 k : ℕ
x : R
h : k = k_1
x_1 x_2 : n
⊢ single i j x x_1 x_2 = single i j x x_1 x_2

Tactic:
simp
-- 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
p : R[X]
k_1 k : ℕ
x : R
h : ¬k = k_1
neg : ∀ (x x_1 : n), Eq.{u_1 + 1} (α := R) (0 x x_1) (single i j 0 x x_1)
⊢ Eq (α := Matrix n n R) 0 (single i j 0)

Tactic:
funext
-- 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
p : R[X]
k_1 k : ℕ
x : R
h : ¬k = k_1
x_1 x_2 : n
⊢ Eq.{u_1 + 1} (α := R) (0 x_1 x_2) (single i j 0 x_1 x_2)

Tactic:
simp
-- 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.{w, w, u_1} n n R[X]
k : ℕ
i j : n
⊢ coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) m) k i j = (m i j).coeff k

Tactic:
Matrix.induction_on' m ?_ ?_ ?_

Premises used: Matrix.induction_on'
-- 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.{w, w, u_1} n n R[X]
k : ℕ
i j : n
refine_1 :
  Eq.{u_1 + 1} (α := R) (coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) 0) k i j) (coeff (0 i j) k)
refine_2 :
  ∀ (p q : Matrix.{w, w, u_1} n n R[X]),
    coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) p) k i j = (p i j).coeff k →
      coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) q) k i j = (q i j).coeff k →
        coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (p + q)) k i j = ((p + q) i j).coeff k
refine_3 :
  ∀ (i_1 j_1 : n) (x : R[X]),
    coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (single i_1 j_1 x)) k i j =
      (single i_1 j_1 x i j).coeff k
⊢ coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) m) k i j = (m i j).coeff k

Tactic:
refine Matrix.induction_on' m ?_ ?_ ?_
-- 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.{w, w, u_1} n n R[X]
k : ℕ
i j : n
⊢ Eq.{u_1 + 1} (α := R) (coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) 0) k i j) (coeff (0 i j) k)

Tactic:
simp
-- 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.{w, w, u_1} n n R[X]
k : ℕ
i j : n
p q : Matrix.{w, w, u_1} n n R[X]
hp : coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) p) k i j = (p i j).coeff k
hq : coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) q) k i j = (q i j).coeff k
⊢ coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (p + q)) k i j = ((p + q) i j).coeff k

Tactic:
simp [hp, hq]
-- 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.{w, w, u_1} n n R[X]
k : ℕ
i j i' j' : n
x : R[X]
refine_3 : single i' j' (x.coeff k) i j = (single i' j' x i j).coeff k
⊢ coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (single i' j' x)) k i j =
    (single i' j' x i j).coeff k

Tactic:
rw [matPolyEquiv_coeff_apply_aux_2]

Premises used: matPolyEquiv_coeff_apply_aux_2
-- 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.{w, w, u_1} n n R[X]
k : ℕ
i j i' j' : n
x : R[X]
refine_3 : (if i' = i ∧ j' = j then x.coeff k else 0) = (if i' = i ∧ j' = j then x else 0).coeff k
⊢ single i' j' (x.coeff k) i j = (single i' j' x i j).coeff k

Tactic:
dsimp [single]

Premises used: Matrix.single
-- 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.{w, w, u_1} n n R[X]
k : ℕ
i j i' j' : n
x : R[X]
pos : i' = i ∧ j' = j → x.coeff k = x.coeff k
neg : ¬(i' = i ∧ j' = j) → Eq.{u_1 + 1} (α := R) 0 (coeff 0 k)
⊢ (if i' = i ∧ j' = j then x.coeff k else 0) = (if i' = i ∧ j' = j then x else 0).coeff k

Tactic:
split_ifs
-- 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.{w, w, u_1} n n R[X]
k : ℕ
i j i' j' : n
x : R[X]
h : i' = i ∧ j' = j
⊢ x.coeff k = x.coeff k

Tactic:
constructor
-- 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.{w, w, u_1} n n R[X]
k : ℕ
i j i' j' : n
x : R[X]
h : ¬(i' = i ∧ j' = j)
⊢ Eq.{u_1 + 1} (α := R) 0 (coeff 0 k)

Tactic:
simp
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
p : (Matrix n n R)[X]
i j : n
k : ℕ
⊢ p =
    (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]) p)

Tactic:
simp
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
p : (Matrix n n R)[X]
i j : n
k : ℕ
⊢ p =
    (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]) p)

Tactic:
have t : p = matPolyEquiv (matPolyEquiv.symm p) := by simp
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
p : (Matrix n n R)[X]
i j : n
k : ℕ
t :
  p =
    (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]) p)
rw :
  coeff
    ((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]) p))
    k i j
| p.coeff k i j

Tactic:
rw [t]
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
p : (Matrix n n R)[X]
i j : n
k : ℕ
t :
  p =
    (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]) p)
conv_rhs :
  Eq.{u_1 + 1} (α := R) (coeff ((AlgEquiv.symm matPolyEquiv : (a : (Matrix n n R)[X]) → Matrix n n R[X]) p i j) k)
    (coeff
      ((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]) p))
      k i j)
⊢ coeff ((AlgEquiv.symm matPolyEquiv : (a : (Matrix n n R)[X]) → Matrix n n R[X]) p i j) k = p.coeff k i j

Tactic:
conv_rhs => rw [t]
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
p : (Matrix n n R)[X]
i j : n
k : ℕ
t :
  p =
    (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]) p)
⊢ Eq.{u_1 + 1} (α := R) (coeff ((AlgEquiv.symm matPolyEquiv : (a : (Matrix n n R)[X]) → Matrix n n R[X]) p i j) k)
    (coeff
      ((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]) p))
      k i j)

Tactic:
simp only [matPolyEquiv_coeff_apply]

Premises used: matPolyEquiv_coeff_apply
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
p : R[X]
a :
  ∀ (m : ℕ) (i j : n),
    Eq.{u_1 + 1} (α := R)
      (coeff
        ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X])
          (HSMul.hSMul (β := Matrix.{w, w, u_1} n n R[X]) p 1))
        m i j)
      (coeff (Polynomial.map (algebraMap R (Matrix n n R)) p) m i j)
⊢ Eq (α := (Matrix n n R)[X])
    ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (HSMul.hSMul (β := Matrix.{w, w, u_1} n n R[X]) p 1) :
      (Matrix n n R)[X])
    (Polynomial.map (algebraMap R (Matrix n n R)) p : (Matrix n n R)[X])

Tactic:
ext m i j
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
p : R[X]
m : ℕ
i j : n
a : (if i = j then p else 0).coeff m = if i = j then p.coeff m else 0
⊢ Eq.{u_1 + 1} (α := R)
    (coeff
      ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (HSMul.hSMul (β := Matrix.{w, w, u_1} n n R[X]) p 1))
      m i j)
    (coeff (Polynomial.map (algebraMap R (Matrix n n R)) p) m i j)

Tactic:
simp only [matPolyEquiv_coeff_apply, smul_apply, one_apply, smul_eq_mul, mul_ite, mul_one,
    mul_zero, coeff_map, algebraMap_matrix_apply, Algebra.algebraMap_self, RingHom.id_apply]

Premises used: Polynomial.coeff_map, RingHom.id_apply, Matrix.one_apply, Algebra.algebraMap_self, mul_ite, Matrix.smul_apply, MulZeroClass.mul_zero, matPolyEquiv_coeff_apply, smul_eq_mul, mul_one, Matrix.algebraMap_matrix_apply
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
p : R[X]
m : ℕ
i j : n
pos : i = j → p.coeff m = p.coeff m
neg : ¬i = j → Eq.{u_1 + 1} (α := R) (coeff 0 m) 0
⊢ (if i = j then p else 0).coeff m = if i = j then p.coeff m else 0

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
p : R[X]
m : ℕ
i j : n
h : i = j
⊢ p.coeff m = p.coeff m

Tactic:
simp
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
p : R[X]
m : ℕ
i j : n
h : ¬i = j
⊢ Eq.{u_1 + 1} (α := R) (coeff 0 m) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
p : R[X]
M : Matrix.{w, w, u_1} n n R[X]
rw :
  (matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (p • (1 * M)) =
    HMul.hMul (α := (Matrix n n R)[X]) (β := (Matrix n n R)[X]) (Polynomial.map (algebraMap R (Matrix n n R)) p)
      ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (1 * M) : (Matrix n n R)[X])
rw₁ :
  (matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (HSMul.hSMul (β := Matrix.{w, w, u_1} n n R[X]) p 1 * M) =
    HMul.hMul (α := (Matrix n n R)[X]) (β := (Matrix n n R)[X]) (Polynomial.map (algebraMap R (Matrix n n R)) p)
      ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (1 * M) : (Matrix n n R)[X])
rw₂ :
  HMul.hMul (α := (Matrix n n R)[X]) (β := (Matrix n n R)[X])
      ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (HSMul.hSMul (β := Matrix.{w, w, u_1} n n R[X]) p 1) :
        (Matrix n n R)[X])
      ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) M : (Matrix n n R)[X]) =
    HMul.hMul (α := (Matrix n n R)[X]) (β := (Matrix n n R)[X]) (Polynomial.map (algebraMap R (Matrix n n R)) p)
      ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (1 * M) : (Matrix n n R)[X])
rw₃ :
  HMul.hMul (α := (Matrix n n R)[X]) (β := (Matrix n n R)[X]) (Polynomial.map (algebraMap R (Matrix n n R)) p)
      ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) M : (Matrix n n R)[X]) =
    HMul.hMul (α := (Matrix n n R)[X]) (β := (Matrix n n R)[X]) (Polynomial.map (algebraMap R (Matrix n n R)) p)
      ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (1 * M) : (Matrix n n R)[X])
rw₄ rw₅ :
  HMul.hMul (α := (Matrix n n R)[X]) (β := (Matrix n n R)[X]) (Polynomial.map (algebraMap R (Matrix n n R)) p)
      ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) M : (Matrix n n R)[X]) =
    HMul.hMul (α := (Matrix n n R)[X]) (β := (Matrix n n R)[X]) (Polynomial.map (algebraMap R (Matrix n n R)) p)
      ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) M : (Matrix n n R)[X])
⊢ (matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (p • M) =
    HMul.hMul (α := (Matrix n n R)[X]) (β := (Matrix n n R)[X]) (Polynomial.map (algebraMap R (Matrix n n R)) p)
      ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) M : (Matrix n n R)[X])

Tactic:
rw [← one_mul M, ← smul_mul_assoc, map_mul, matPolyEquiv_smul_one, one_mul]

Premises used: smul_mul_assoc, map_mul, matPolyEquiv_smul_one, one_mul
-- 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)[X]
r : R
suffices :
  Eq (α := (Matrix n n R)[X] →ₐ[R] Matrix n n R)
    (AlgHom.comp (AlgHom.mapMatrix (aeval r)) (↑(AlgEquiv.symm matPolyEquiv) : (Matrix n n R)[X] →ₐ[R] Matrix n n R[X]))
    (eval₂AlgHom (AlgHom.id R (Matrix n n R)) ((scalar n : (a : R) → Matrix n n R) r) ⋯)
⊢ Eq (α := Matrix n n R)
    (Matrix.map (α := R[X]) ((AlgEquiv.symm matPolyEquiv : (a : (Matrix n n R)[X]) → Matrix n n R[X]) M) (eval r))
    (eval ((scalar n : (a : R) → Matrix n n R) r) M)

Tactic:
suffices ((aeval r).mapMatrix.comp matPolyEquiv.symm.toAlgHom : (Matrix n n R)[X] →ₐ[R] _) =
      (eval₂AlgHom (AlgHom.id R _) (scalar n r)
        fun x => (scalar_commute _ (Commute.all _) _).symm) from
    DFunLike.congr_fun this M