-- Mathlib/RingTheory/PolynomialAlgebra.lean
theorem matPolyEquiv_coeff_apply_aux_2 (i j : n) (p : R[X]) (k : ℕ) :
    coeff (matPolyEquiv (stdBasisMatrix i j p)) k = stdBasisMatrix i j (coeff p k)

Proof state:
case refine_2
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k✝ k : ℕ
x : R
⊢ (matPolyEquiv (stdBasisMatrix i j ((monomial k) x))).coeff k✝ = stdBasisMatrix i j (((monomial k) x).coeff k✝)

Tactic:
simp only [matPolyEquiv_coeff_apply_aux_1, coeff_monomial]

Result:
case refine_2
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k✝ k : ℕ
x : R
⊢ (if k = k✝ then stdBasisMatrix i j x else 0) = stdBasisMatrix i j (if k = k✝ then x else 0)

Proof state:
case refine_2
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k : ℕ
⊢ ∀ (n_1 : ℕ) (a : R),
    (matPolyEquiv (stdBasisMatrix i j ((monomial n_1) a))).coeff k = stdBasisMatrix i j (((monomial n_1) a).coeff k)

Tactic:
intro k x

Result:
case refine_2
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k✝ k : ℕ
x : R
⊢ (matPolyEquiv (stdBasisMatrix i j ((monomial k) x))).coeff k✝ = stdBasisMatrix i j (((monomial k) x).coeff k✝)

Proof state:
case refine_1.a
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p✝ : R[X]
k : ℕ
p q : R[X]
hp : (matPolyEquiv (stdBasisMatrix i j p)).coeff k = stdBasisMatrix i j (p.coeff k)
hq : (matPolyEquiv (stdBasisMatrix i j q)).coeff k = stdBasisMatrix i j (q.coeff k)
i✝ j✝ : n
⊢ (matPolyEquiv (stdBasisMatrix i j (p + q))).coeff k i✝ j✝ = stdBasisMatrix i j ((p + q).coeff k) i✝ j✝

Tactic:
simp [hp, hq, coeff_add, DMatrix.add_apply, stdBasisMatrix_add]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k✝ k : ℕ
x : R
h✝ : ¬k = k✝
⊢ 0 = stdBasisMatrix i j 0

Tactic:
funext

Result:
case neg.h.h
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k✝ k : ℕ
x : R
h✝ : ¬k = k✝
x✝¹ x✝ : n
⊢ 0 x✝¹ x✝ = stdBasisMatrix i j 0 x✝¹ x✝

Proof state:
case refine_1
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p✝ : R[X]
k : ℕ
p q : R[X]
hp : (matPolyEquiv (stdBasisMatrix i j p)).coeff k = stdBasisMatrix i j (p.coeff k)
hq : (matPolyEquiv (stdBasisMatrix i j q)).coeff k = stdBasisMatrix i j (q.coeff k)
⊢ (matPolyEquiv (stdBasisMatrix i j (p + q))).coeff k = stdBasisMatrix i j ((p + q).coeff k)

Tactic:
ext

Result:
case refine_1.a
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p✝ : R[X]
k : ℕ
p q : R[X]
hp : (matPolyEquiv (stdBasisMatrix i j p)).coeff k = stdBasisMatrix i j (p.coeff k)
hq : (matPolyEquiv (stdBasisMatrix i j q)).coeff k = stdBasisMatrix i j (q.coeff k)
i✝ j✝ : n
⊢ (matPolyEquiv (stdBasisMatrix i j (p + q))).coeff k i✝ j✝ = stdBasisMatrix i j ((p + q).coeff k) i✝ j✝

Proof state:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k : ℕ
⊢ (matPolyEquiv (stdBasisMatrix i j p)).coeff k = stdBasisMatrix i j (p.coeff k)

Tactic:
refine Polynomial.induction_on' p ?_ ?_

Result:
case refine_1
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k : ℕ
⊢ ∀ (p q : R[X]),
    (matPolyEquiv (stdBasisMatrix i j p)).coeff k = stdBasisMatrix i j (p.coeff k) →
      (matPolyEquiv (stdBasisMatrix i j q)).coeff k = stdBasisMatrix i j (q.coeff k) →
        (matPolyEquiv (stdBasisMatrix i j (p + q))).coeff k = stdBasisMatrix i j ((p + q).coeff k)

case refine_2
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k : ℕ
⊢ ∀ (n_1 : ℕ) (a : R),
    (matPolyEquiv (stdBasisMatrix i j ((monomial n_1) a))).coeff k = stdBasisMatrix i j (((monomial n_1) a).coeff k)

Proof state:
case refine_1
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k : ℕ
⊢ ∀ (p q : R[X]),
    (matPolyEquiv (stdBasisMatrix i j p)).coeff k = stdBasisMatrix i j (p.coeff k) →
      (matPolyEquiv (stdBasisMatrix i j q)).coeff k = stdBasisMatrix i j (q.coeff k) →
        (matPolyEquiv (stdBasisMatrix i j (p + q))).coeff k = stdBasisMatrix i j ((p + q).coeff k)

Tactic:
intro p q hp hq

Result:
case refine_1
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p✝ : R[X]
k : ℕ
p q : R[X]
hp : (matPolyEquiv (stdBasisMatrix i j p)).coeff k = stdBasisMatrix i j (p.coeff k)
hq : (matPolyEquiv (stdBasisMatrix i j q)).coeff k = stdBasisMatrix i j (q.coeff k)
⊢ (matPolyEquiv (stdBasisMatrix i j (p + q))).coeff k = stdBasisMatrix i j ((p + q).coeff k)

Proof state:
case neg.h.h
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k✝ k : ℕ
x : R
h✝ : ¬k = k✝
x✝¹ x✝ : n
⊢ 0 x✝¹ x✝ = stdBasisMatrix i j 0 x✝¹ x✝

Tactic:
simp

Result:
no goals