case refine_1
R : Type u_1
A : Type ?u.547358
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j : n
⊢ coeff (↑matPolyEquiv 0) k i j = coeff (OfNat.ofNat 0 i j) k

case refine_2
R : Type u_1
A : Type ?u.547358
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
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]),
    coeff (↑matPolyEquiv p) k i j = coeff (p i j) k →
      coeff (↑matPolyEquiv q) k i j = coeff (q i j) k → coeff (↑matPolyEquiv (p + q)) k i j = coeff ((p + q) i j) k

case refine_3
R : Type u_1
A : Type ?u.547358
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
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]),
    coeff (↑matPolyEquiv (stdBasisMatrix i_1 j_1 x)) k i j = coeff (stdBasisMatrix i_1 j_1 x i j) k
R : Type u_1
A : Type ?u.547358
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j : n
⊢ coeff (↑matPolyEquiv m) k i j = coeff (m i j) k
refine Matrix.induction_on' m ?_ ?_ ?_
no goals
case refine_1
R : Type u_1
A : Type ?u.547358
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j : n
⊢ coeff (↑matPolyEquiv 0) k i j = coeff (OfNat.ofNat 0 i j) k
simp
case refine_2
R : Type u_1
A : Type ?u.547358
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
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 : coeff (↑matPolyEquiv p) k i j = coeff (p i j) k
hq : coeff (↑matPolyEquiv q) k i j = coeff (q i j) k
⊢ coeff (↑matPolyEquiv (p + q)) k i j = coeff ((p + q) i j) k
case refine_2
R : Type u_1
A : Type ?u.547358
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
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]),
    coeff (↑matPolyEquiv p) k i j = coeff (p i j) k →
      coeff (↑matPolyEquiv q) k i j = coeff (q i j) k → coeff (↑matPolyEquiv (p + q)) k i j = coeff ((p + q) i j) k
intro p q hp hq
no goals
case refine_2
R : Type u_1
A : Type ?u.547358
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
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 : coeff (↑matPolyEquiv p) k i j = coeff (p i j) k
hq : coeff (↑matPolyEquiv q) k i j = coeff (q i j) k
⊢ coeff (↑matPolyEquiv (p + q)) k i j = coeff ((p + q) i j) k
simp [hp, hq]
case refine_3
R : Type u_1
A : Type ?u.547358
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j i' j' : n
x : R[X]
⊢ coeff (↑matPolyEquiv (stdBasisMatrix i' j' x)) k i j = coeff (stdBasisMatrix i' j' x i j) k
case refine_3
R : Type u_1
A : Type ?u.547358
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
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]),
    coeff (↑matPolyEquiv (stdBasisMatrix i_1 j_1 x)) k i j = coeff (stdBasisMatrix i_1 j_1 x i j) k
intro i' j' x
case refine_3
R : Type u_1
A : Type ?u.547358
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
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' (coeff x k) i j = coeff (stdBasisMatrix i' j' x i j) k
case refine_3
R : Type u_1
A : Type ?u.547358
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j i' j' : n
x : R[X]
⊢ coeff (↑matPolyEquiv (stdBasisMatrix i' j' x)) k i j = coeff (stdBasisMatrix i' j' x i j) k
erw [matPolyEquiv_coeff_apply_aux_2]
case refine_3
R : Type u_1
A : Type ?u.547358
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
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 coeff x k else 0) = coeff (if i' = i ∧ j' = j then x else 0) k
case refine_3
R : Type u_1
A : Type ?u.547358
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
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' (coeff x k) i j = coeff (stdBasisMatrix i' j' x i j) k
dsimp [stdBasisMatrix]
case refine_3.inl
R : Type u_1
A : Type ?u.547358
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
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
⊢ coeff x k = coeff x k

case refine_3.inr
R : Type u_1
A : Type ?u.547358
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
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
case refine_3
R : Type u_1
A : Type ?u.547358
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
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 coeff x k else 0) = coeff (if i' = i ∧ j' = j then x else 0) k
split_ifs <;> rename_i h
case refine_3.inl.intro
R : Type u_1
A : Type ?u.547358
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i' j' : n
x : R[X]
⊢ coeff x k = coeff x k
case refine_3.inl
R : Type u_1
A : Type ?u.547358
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
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
⊢ coeff x k = coeff x k
rcases h with ⟨rfl, rfl⟩
no goals
case refine_3.inl.intro
R : Type u_1
A : Type ?u.547358
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i' j' : n
x : R[X]
⊢ coeff x k = coeff x k
simp [stdBasisMatrix]
no goals
case refine_3.inr
R : Type u_1
A : Type ?u.547358
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
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
simp [stdBasisMatrix, h]