case refine_1
R : Type u_1
A : Type ?u.521163
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k : ℕ
⊢ ∀ (p q : R[X]),
    coeff (↑matPolyEquiv (stdBasisMatrix i j p)) k = stdBasisMatrix i j (coeff p k) →
      coeff (↑matPolyEquiv (stdBasisMatrix i j q)) k = stdBasisMatrix i j (coeff q k) →
        coeff (↑matPolyEquiv (stdBasisMatrix i j (p + q))) k = stdBasisMatrix i j (coeff (p + q) k)

case refine_2
R : Type u_1
A : Type ?u.521163
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k : ℕ
⊢ ∀ (n_1 : ℕ) (a : R),
    coeff (↑matPolyEquiv (stdBasisMatrix i j (↑(monomial n_1) a))) k = stdBasisMatrix i j (coeff (↑(monomial n_1) a) k)
R : Type u_1
A : Type ?u.521163
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k : ℕ
⊢ coeff (↑matPolyEquiv (stdBasisMatrix i j p)) k = stdBasisMatrix i j (coeff p k)
refine Polynomial.induction_on' p ?_ ?_
case refine_1
R : Type u_1
A : Type ?u.521163
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p✝ : R[X]
k : ℕ
p q : R[X]
hp : coeff (↑matPolyEquiv (stdBasisMatrix i j p)) k = stdBasisMatrix i j (coeff p k)
hq : coeff (↑matPolyEquiv (stdBasisMatrix i j q)) k = stdBasisMatrix i j (coeff q k)
⊢ coeff (↑matPolyEquiv (stdBasisMatrix i j (p + q))) k = stdBasisMatrix i j (coeff (p + q) k)
case refine_1
R : Type u_1
A : Type ?u.521163
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k : ℕ
⊢ ∀ (p q : R[X]),
    coeff (↑matPolyEquiv (stdBasisMatrix i j p)) k = stdBasisMatrix i j (coeff p k) →
      coeff (↑matPolyEquiv (stdBasisMatrix i j q)) k = stdBasisMatrix i j (coeff q k) →
        coeff (↑matPolyEquiv (stdBasisMatrix i j (p + q))) k = stdBasisMatrix i j (coeff (p + q) k)
intro p q hp hq
case refine_1.a.h
R : Type u_1
A : Type ?u.521163
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p✝ : R[X]
k : ℕ
p q : R[X]
hp : coeff (↑matPolyEquiv (stdBasisMatrix i j p)) k = stdBasisMatrix i j (coeff p k)
hq : coeff (↑matPolyEquiv (stdBasisMatrix i j q)) k = stdBasisMatrix i j (coeff q k)
i✝ x✝ : n
⊢ coeff (↑matPolyEquiv (stdBasisMatrix i j (p + q))) k i✝ x✝ = stdBasisMatrix i j (coeff (p + q) k) i✝ x✝
case refine_1
R : Type u_1
A : Type ?u.521163
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p✝ : R[X]
k : ℕ
p q : R[X]
hp : coeff (↑matPolyEquiv (stdBasisMatrix i j p)) k = stdBasisMatrix i j (coeff p k)
hq : coeff (↑matPolyEquiv (stdBasisMatrix i j q)) k = stdBasisMatrix i j (coeff q k)
⊢ coeff (↑matPolyEquiv (stdBasisMatrix i j (p + q))) k = stdBasisMatrix i j (coeff (p + q) k)
ext
no goals
case refine_1.a.h
R : Type u_1
A : Type ?u.521163
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p✝ : R[X]
k : ℕ
p q : R[X]
hp : coeff (↑matPolyEquiv (stdBasisMatrix i j p)) k = stdBasisMatrix i j (coeff p k)
hq : coeff (↑matPolyEquiv (stdBasisMatrix i j q)) k = stdBasisMatrix i j (coeff q k)
i✝ x✝ : n
⊢ coeff (↑matPolyEquiv (stdBasisMatrix i j (p + q))) k i✝ x✝ = stdBasisMatrix i j (coeff (p + q) k) i✝ x✝
simp [hp, hq, coeff_add, DMatrix.add_apply, stdBasisMatrix_add]
case refine_2
R : Type u_1
A : Type ?u.521163
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k✝ k : ℕ
x : R
⊢ coeff (↑matPolyEquiv (stdBasisMatrix i j (↑(monomial k) x))) k✝ = stdBasisMatrix i j (coeff (↑(monomial k) x) k✝)
case refine_2
R : Type u_1
A : Type ?u.521163
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k : ℕ
⊢ ∀ (n_1 : ℕ) (a : R),
    coeff (↑matPolyEquiv (stdBasisMatrix i j (↑(monomial n_1) a))) k = stdBasisMatrix i j (coeff (↑(monomial n_1) a) k)
intro k x
case refine_2
R : Type u_1
A : Type ?u.521163
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
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)
case refine_2
R : Type u_1
A : Type ?u.521163
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k✝ k : ℕ
x : R
⊢ coeff (↑matPolyEquiv (stdBasisMatrix i j (↑(monomial k) x))) k✝ = stdBasisMatrix i j (coeff (↑(monomial k) x) k✝)
simp only [matPolyEquiv_coeff_apply_aux_1, coeff_monomial]
case refine_2.inr.h.h
R : Type u_1
A : Type ?u.521163
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
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
⊢ OfNat.ofNat 0 x✝¹ x✝ = stdBasisMatrix i j 0 x✝¹ x✝
case refine_2.inr
R : Type u_1
A : Type ?u.521163
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
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
funext
no goals
case refine_2.inr.h.h
R : Type u_1
A : Type ?u.521163
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
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
⊢ OfNat.ofNat 0 x✝¹ x✝ = stdBasisMatrix i j 0 x✝¹ x✝
simp