-- Mathlib/RingTheory/PolynomialAlgebra.lean
theorem matPolyEquiv_coeff_apply (m : Matrix n n R[X]) (k : ℕ) (i j : n) :
    coeff (matPolyEquiv m) k i j = coeff (m i j) k

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

Tactic:
rw [matPolyEquiv_coeff_apply_aux_2]

Result:
case refine_3
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j i' j' : n
x : R[X]
⊢ stdBasisMatrix i' j' (x.coeff k) i j = (stdBasisMatrix i' j' x i j).coeff k

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

Tactic:
simp

Result:
no goals

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

Tactic:
simp [hp, hq]

Result:
no goals

Proof state:
case refine_3
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j i' j' : n
x : R[X]
⊢ stdBasisMatrix i' j' (x.coeff k) i j = (stdBasisMatrix i' j' x i j).coeff k

Tactic:
dsimp [stdBasisMatrix]

Result:
case refine_3
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j i' j' : n
x : R[X]
⊢ (if i' = i ∧ j' = j then x.coeff k else 0) = (if i' = i ∧ j' = j then x else 0).coeff k

Proof state:
case refine_3
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j : n
⊢ ∀ (i_1 j_1 : n) (x : R[X]),
    (matPolyEquiv (stdBasisMatrix i_1 j_1 x)).coeff k i j = (stdBasisMatrix i_1 j_1 x i j).coeff k

Tactic:
intro i' j' x

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

Proof state:
case neg
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j i' j' : n
x : R[X]
h : ¬(i' = i ∧ j' = j)
⊢ 0 = coeff 0 k

Tactic:
simp [stdBasisMatrix, h]

Result:
no goals

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

Tactic:
intro p q hp hq

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

Proof state:
case refine_3
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j i' j' : n
x : R[X]
⊢ (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 <;> rename_i h

Result:
case pos
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j i' j' : n
x : R[X]
h : i' = i ∧ j' = j
⊢ x.coeff k = x.coeff k

case neg
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j i' j' : n
x : R[X]
h : ¬(i' = i ∧ j' = j)
⊢ 0 = coeff 0 k

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

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

Result:
case refine_1
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j : n
⊢ (matPolyEquiv 0).coeff k i j = (0 i j).coeff k

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

case refine_3
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j : n
⊢ ∀ (i_1 j_1 : n) (x : R[X]),
    (matPolyEquiv (stdBasisMatrix i_1 j_1 x)).coeff k i j = (stdBasisMatrix i_1 j_1 x i j).coeff k

Proof state:
case pos
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix 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:
rcases h with ⟨rfl, rfl⟩

Result:
case pos.intro
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i' j' : n
x : R[X]
⊢ x.coeff k = x.coeff k

Proof state:
case pos.intro
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i' j' : n
x : R[X]
⊢ x.coeff k = x.coeff k

Tactic:
simp [stdBasisMatrix]

Result:
no goals