awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MatrixPolynomialAlgebra (goal)
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
⊢ coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) m) k i j = (m i j).coeff k
have 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
Tactic: refine Matrix.induction_on' m ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.MatrixPolynomialAlgebra (goal)
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]
⊢ 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
have refine_3 : single i' j' (x.coeff k) i j = (single i' j' x i j).coeff k
Tactic: rw [matPolyEquiv_coeff_apply_aux_2]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixPolynomialAlgebra (goal)
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]
⊢ single i' j' (x.coeff k) i j = (single i' j' x i j).coeff k
have refine_3 : (if i' = i ∧ j' = j then x.coeff k else 0) = (if i' = i ∧ j' = j then x else 0).coeff k
Tactic: dsimp [single]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixPolynomialAlgebra (goal)
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]
⊢ (if i' = i ∧ j' = j then x.coeff k else 0) = (if i' = i ∧ j' = j then x else 0).coeff k
have pos : i' = i ∧ j' = j → x.coeff k = x.coeff k
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.MatrixPolynomialAlgebra (goal)
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
⊢ (if i' = i ∧ j' = j then x.coeff k else 0) = (if i' = i ∧ j' = j then x else 0).coeff k
have neg : ¬(i' = i ∧ j' = j) → Eq.{u_1 + 1} (α := R) 0 (coeff 0 k)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.MatrixPolynomialAlgebra (hypothesis)
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 : ℕ
⊢ coeff ((AlgEquiv.symm matPolyEquiv : (a : (Matrix n n R)[X]) → Matrix n n R[X]) p i j) k = p.coeff k i j
have 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)
Tactic: have t : p = matPolyEquiv (matPolyEquiv.symm p) := by simp
-- Lean 4 proof step from Mathlib.RingTheory.MatrixPolynomialAlgebra (goal)
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)
| p.coeff k i j
have 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
Tactic: rw [t]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixPolynomialAlgebra (goal)
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)
⊢ coeff ((AlgEquiv.symm matPolyEquiv : (a : (Matrix n n R)[X]) → Matrix n n R[X]) p i j) k = p.coeff k i j
have 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)
Tactic: conv_rhs => rw [t]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixPolynomialAlgebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
p : R[X]
⊢ 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])
have 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)
Tactic: ext m i j
-- Lean 4 proof step from Mathlib.RingTheory.MatrixPolynomialAlgebra (goal)
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
⊢ 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)
have a : (if i = j then p else 0).coeff m = if i = j then p.coeff m else 0
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]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixPolynomialAlgebra (goal)
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
⊢ (if i = j then p else 0).coeff m = if i = j then p.coeff m else 0
have pos : i = j → p.coeff m = p.coeff m
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.MatrixPolynomialAlgebra (goal)
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
⊢ (if i = j then p else 0).coeff m = if i = j then p.coeff m else 0
have neg : ¬i = j → Eq.{u_1 + 1} (α := R) (coeff 0 m) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.MatrixPolynomialAlgebra (goal)
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]
⊢ (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])
have 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])
Tactic: rw [← one_mul M, ← smul_mul_assoc, map_mul, matPolyEquiv_smul_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixPolynomialAlgebra (goal)
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])
⊢ (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])
have 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])
Tactic: rw [← one_mul M, ← smul_mul_assoc, map_mul, matPolyEquiv_smul_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixPolynomialAlgebra (goal)
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])
⊢ (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])
have 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])
Tactic: rw [← one_mul M, ← smul_mul_assoc, map_mul, matPolyEquiv_smul_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixPolynomialAlgebra (goal)
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])
⊢ (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])
have 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])
Tactic: rw [← one_mul M, ← smul_mul_assoc, map_mul, matPolyEquiv_smul_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixPolynomialAlgebra (goal)
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])
⊢ (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])
have 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])
Tactic: rw [← one_mul M, ← smul_mul_assoc, map_mul, matPolyEquiv_smul_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixPolynomialAlgebra (goal)
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
⊢ 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)
have 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) sorry)
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
-- Lean 4 proof step from Mathlib.RingTheory.MatrixPolynomialAlgebra (goal)
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
⊢ 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) ⋯)
have hC : Eq (α := Matrix n n R →ₐ[R] Matrix n n R)
  (AlgHom.comp
    (AlgHom.comp (AlgHom.mapMatrix (aeval r)) (↑(AlgEquiv.symm matPolyEquiv) : (Matrix n n R)[X] →ₐ[R] Matrix n n R[X]))
    CAlgHom)
  (AlgHom.comp (eval₂AlgHom (AlgHom.id R (Matrix n n R)) ((scalar n : (a : R) → Matrix n n R) r) sorry) CAlgHom)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.RingTheory.MatrixPolynomialAlgebra (goal)
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
hC :
  Eq (α := Matrix n n R →ₐ[R] Matrix n n R)
    (AlgHom.comp
      (AlgHom.comp (AlgHom.mapMatrix (aeval r))
        (↑(AlgEquiv.symm matPolyEquiv) : (Matrix n n R)[X] →ₐ[R] Matrix n n R[X]))
      CAlgHom)
    (AlgHom.comp (eval₂AlgHom (AlgHom.id R (Matrix n n R)) ((scalar n : (a : R) → Matrix n n R) r) ⋯) CAlgHom)
⊢ 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) ⋯)
have hX : Eq (α := Matrix n n R)
  ((AlgHom.comp (AlgHom.mapMatrix (aeval r)) (↑(AlgEquiv.symm matPolyEquiv) : (Matrix n n R)[X] →ₐ[R] Matrix n n R[X]) :
        (a : (Matrix n n R)[X]) → Matrix n n R)
      X :
    Matrix n n R)
  (((eval₂AlgHom (AlgHom.id R (Matrix n n R)) ((scalar n : (a : R) → Matrix n n R) r) sorry :
          (Matrix n n R)[X] →ₐ[R] Matrix n n R) :
        (a : (Matrix n n R)[X]) → Matrix n n R)
      X :
    Matrix n n R)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.RingTheory.MatrixPolynomialAlgebra (goal)
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
⊢ Eq (α := Matrix n n R →ₐ[R] Matrix n n R)
    (AlgHom.comp
      (AlgHom.comp (AlgHom.mapMatrix (aeval r))
        (↑(AlgEquiv.symm matPolyEquiv) : (Matrix n n R)[X] →ₐ[R] Matrix n n R[X]))
      CAlgHom)
    (AlgHom.comp (eval₂AlgHom (AlgHom.id R (Matrix n n R)) ((scalar n : (a : R) → Matrix n n R) r) ⋯) CAlgHom)
have hC : ∀ (M : Matrix n n R),
  Eq (α := Matrix n n R)
    ((AlgHom.comp
            (AlgHom.comp (AlgHom.mapMatrix (aeval r))
              (↑(AlgEquiv.symm matPolyEquiv) : (Matrix n n R)[X] →ₐ[R] Matrix n n R[X]))
            CAlgHom :
          (a : Matrix n n R) → Matrix n n R)
        M :
      Matrix n n R)
    (((AlgHom.comp (eval₂AlgHom (AlgHom.id R (Matrix n n R)) ((scalar n : (a : R) → Matrix n n R) r) sorry) CAlgHom :
            Matrix n n R →ₐ[R] Matrix n n R) :
          (a : Matrix n n R) → Matrix n n R)
        M :
      Matrix n n R)
Tactic: ext M : 1
-- Lean 4 proof step from Mathlib.RingTheory.MatrixPolynomialAlgebra (goal)
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]
r : R
i j : n
⊢ eval ((scalar n : (a : R) → Matrix n n R) r) ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) M) i j =
    eval r (M i j)
have rw : M.map (eval r) i j = eval r (M i j)
Tactic: rw [matPolyEquiv_eval_eq_map, map_apply]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixPolynomialAlgebra (goal)
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]
r : R
i j : n
rw : M.map (eval r) i j = eval r (M i j)
⊢ eval ((scalar n : (a : R) → Matrix n n R) r) ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) M) i j =
    eval r (M i j)
have rw₁ : eval r (M i j) = eval r (M i j)
Tactic: rw [matPolyEquiv_eval_eq_map, map_apply]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixPolynomialAlgebra (goal)
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]
i j : n
k : ℕ
⊢ k ∈ (m i j).support → k ∈ support (R := Matrix n n R) ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) m)
have contrapose : k ∉ support (R := Matrix n n R) ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) m) → k ∉ (m i j).support
Tactic: contrapose
-- Lean 4 proof step from Mathlib.RingTheory.MatrixPolynomialAlgebra (goal)
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]
i j : n
k : ℕ
⊢ k ∉ support (R := Matrix n n R) ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) m) → k ∉ (m i j).support
have simp : Eq (α := Matrix n n R) (coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) m) k) 0 → (m i j).coeff k = 0
Tactic: simp only [notMem_support_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixPolynomialAlgebra (goal)
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]
i j : n
k : ℕ
hk : Eq (α := Matrix n n R) (coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) m) k) 0
⊢ (m i j).coeff k = 0
have rw : Eq.{u_1 + 1} (α := R) (coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) m) k i j) 0
Tactic: rw [← matPolyEquiv_coeff_apply, hk, zero_apply]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixPolynomialAlgebra (goal)
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]
i j : n
k : ℕ
hk : Eq (α := Matrix n n R) (coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) m) k) 0
rw : Eq.{u_1 + 1} (α := R) (coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) m) k i j) 0
⊢ (m i j).coeff k = 0
have rw₁ : Eq.{u_1 + 1} (α := R) (0 i j) 0
Tactic: rw [← matPolyEquiv_coeff_apply, hk, zero_apply]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixPolynomialAlgebra (goal)
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]
i j : n
k : ℕ
hk : Eq (α := Matrix n n R) (coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) m) k) 0
rw : Eq.{u_1 + 1} (α := R) (coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) m) k i j) 0
rw₁ : Eq.{u_1 + 1} (α := R) (0 i j) 0
⊢ (m i j).coeff k = 0
have rw₂ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [← matPolyEquiv_coeff_apply, hk, zero_apply]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixPolynomialAlgebra (goal)
Goal:
n : Type w
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_3
inst_2 : CommRing R
M : Matrix.{w, w, u_3} n n R[X]
r : R
⊢ eval r M.det =
    det.{u_3, w} (n := n)
      (eval ((scalar n : (a : R) → Matrix n n R) r) ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) M))
have rw : Eq.{u_3 + 1} (α := R)
  (det.{u_3, w} (n := n) ((RingHom.mapMatrix (eval₂RingHom (RingHom.id R) r) : (a : Matrix n n R[X]) → Matrix n n R) M))
  (det.{u_3, w} (n := n)
    (eval ((scalar n : (a : R) → Matrix n n R) r) ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) M)))
Tactic: rw [Polynomial.eval, ← coe_eval₂RingHom, RingHom.map_det]