awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
x y : A ⊗[R] Matrix n n R
hx : invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) x) = x
hy : invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) y) = y
⊢ invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) (x + y)) = x + y
have add : invFun n R A
    (HAdd.hAdd (α := Matrix n n A) (β := Matrix n n A)
      ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) x : Matrix n n A)
      ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) y : Matrix n n A)) =
  x + y
Tactic: rw [map_add]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
x y : A ⊗[R] Matrix n n R
hx : invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) x) = x
hy : invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) y) = y
| x + y
have rw : invFun n R A
  (HAdd.hAdd (α := Matrix n n A) (β := Matrix n n A)
    ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) x : Matrix n n A)
    ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) y : Matrix n n A))
Tactic: rw [← hx, ← hy, ← invFun_add]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
x y : A ⊗[R] Matrix n n R
hx : invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) x) = x
hy : invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) y) = y
⊢ invFun n R A
      (HAdd.hAdd (α := Matrix n n A) (β := Matrix n n A)
        ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) x : Matrix n n A)
        ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) y : Matrix n n A)) =
    x + y
have conv_rhs : invFun n R A
    (HAdd.hAdd (α := Matrix n n A) (β := Matrix n n A)
      ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) x : Matrix n n A)
      ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) y : Matrix n n A)) =
  x + y
Tactic: conv_rhs => rw [← hx, ← hy, ← invFun_add]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
x y : A ⊗[R] Matrix n n R
hx : invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) x) = x
hy : invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) y) = y
conv_rhs :
  invFun n R A
      (HAdd.hAdd (α := Matrix n n A) (β := Matrix n n A)
        ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) x : Matrix n n A)
        ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) y : Matrix n n A)) =
    x + y
⊢ invFun n R A
      (HAdd.hAdd (α := Matrix n n A) (β := Matrix n n A)
        ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) x : Matrix n n A)
        ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) y : Matrix n n A)) =
    x + y
have add : Eq (α := A ⊗[R] Matrix n n R)
  (invFun n R A
    (HAdd.hAdd (α := Matrix n n A) (β := Matrix n n A)
      ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) x : Matrix n n A)
      ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) y : Matrix n n A)))
  (invFun n R A
    (HAdd.hAdd (α := Matrix n n A) (β := Matrix n n A)
      ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) x : Matrix n n A)
      ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) y : Matrix n n A)))
Tactic: conv_rhs => rw [← hx, ← hy, ← invFun_add]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
M : A ⊗[R] Matrix n n R
⊢ invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) M) = M
have zero : Eq (α := A ⊗[R] Matrix n n R) (invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) 0)) 0
Tactic: induction M with
  | zero => simp
  | tmul a m => simp
  | add x y hx hy =>
    rw [map_add]
    conv_rhs => rw [← hx, ← hy, ← invFun_add]
Cleared hypotheses: M
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
M : A ⊗[R] Matrix n n R
zero : Eq (α := A ⊗[R] Matrix n n R) (invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) 0)) 0
⊢ invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) M) = M
have tmul : ∀ (a : A) (m : Matrix n n R),
  Eq (α := A ⊗[R] Matrix n n R)
    (invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) (a ⊗ₜ[R] m))) (a ⊗ₜ[R] m)
Tactic: induction M with
  | zero => simp
  | tmul a m => simp
  | add x y hx hy =>
    rw [map_add]
    conv_rhs => rw [← hx, ← hy, ← invFun_add]
Cleared hypotheses: M
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq n
inst_4 : Fintype n
M : A ⊗[R] Matrix n n R
zero : Eq (α := A ⊗[R] Matrix n n R) (invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) 0)) 0
tmul :
  ∀ (a : A) (m : Matrix n n R),
    Eq (α := A ⊗[R] Matrix n n R)
      (invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) (a ⊗ₜ[R] m))) (a ⊗ₜ[R] m)
⊢ invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) M) = M
have add : ∀ (x y : A ⊗[R] Matrix n n R) (hx : invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) x) = x)
  (hy : invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) y) = y),
  invFun n R A ((toFunAlgHom n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) (x + y)) = x + y
Tactic: induction M with
  | zero => simp
  | tmul a m => simp
  | add x y hx hy =>
    rw [map_add]
    conv_rhs => rw [← hx, ← hy, ← invFun_add]
Cleared hypotheses: M
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (hypothesis)
Goal:
n : Type u_3
R : Type u_5
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Fintype n
inst_4 : DecidableEq n
i j : n
x : A
⊢ Eq (α := A ⊗[R] Matrix n n R)
    ((matrixEquivTensor n R A : (a : Matrix n n A) → A ⊗[R] Matrix n n R) (single i j x) : A ⊗[R] Matrix n n R)
    (x ⊗ₜ[R] single i j 1 : A ⊗[R] Matrix n n R)
have t : ∀ (p : n × n), i = p.1 ∧ j = p.2 ↔ p = (i, j)
Tactic: have t : ∀ p : n × n, i = p.1 ∧ j = p.2 ↔ p = (i, j) := by aesop
-- 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
⊢ Eq (α := (Matrix n n R)[X])
    ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (M.map (⇑C : (a : R) → R[X])) : (Matrix n n R)[X])
    ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M : (Matrix n n R)[X])
have rw : Eq (α := (Matrix n n R)[X])
  ((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])
        ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M)) :
    (Matrix n n R)[X])
  ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M : (Matrix n n R)[X])
Tactic: rw [← matPolyEquiv_symm_C, AlgEquiv.apply_symm_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 n n R
rw :
  Eq (α := (Matrix n n R)[X])
    ((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])
          ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M)) :
      (Matrix n n R)[X])
    ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M : (Matrix n n R)[X])
⊢ Eq (α := (Matrix n n R)[X])
    ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (M.map (⇑C : (a : R) → R[X])) : (Matrix n n R)[X])
    ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M : (Matrix n n R)[X])
have rw₁ : Eq (α := (Matrix n n R)[X]) ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M : (Matrix n n R)[X])
  ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M : (Matrix n n R)[X])
Tactic: rw [← matPolyEquiv_symm_C, AlgEquiv.apply_symm_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
⊢ Eq (α := (Matrix n n R)[X])
    ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (diagonal fun (x : n) ↦ X) : (Matrix n n R)[X])
    (X : (Matrix n n R)[X])
have rw : Eq (α := (Matrix n n R)[X])
  ((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]) X) :
    (Matrix n n R)[X])
  (X : (Matrix n n R)[X])
Tactic: rw [← matPolyEquiv_symm_X, AlgEquiv.apply_symm_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
rw :
  Eq (α := (Matrix n n R)[X])
    ((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]) X) :
      (Matrix n n R)[X])
    (X : (Matrix n n R)[X])
⊢ Eq (α := (Matrix n n R)[X])
    ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (diagonal fun (x : n) ↦ X) : (Matrix n n R)[X])
    (X : (Matrix n n R)[X])
have rw₁ : Eq (α := (Matrix n n R)[X]) X X
Tactic: rw [← matPolyEquiv_symm_X, AlgEquiv.apply_symm_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
i j : n
k : ℕ
x : R
⊢ Eq (α := (Matrix n n R)[X])
    ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (single i j ((monomial k : (a : R) → R[X]) x)) :
      (Matrix n n R)[X])
    ((monomial k : (a : Matrix n n R) → (Matrix n n R)[X]) (single i j x) : (Matrix n n R)[X])
have simp : Eq (α := (Matrix n n R)[X])
  ((AlgEquiv.symm (polyEquivTensor R (Matrix n n R)) : (a : Matrix n n R ⊗[R] R[X]) → (Matrix n n R)[X])
      (((Algebra.TensorProduct.comm R R[X] (Matrix n n R) : R[X] ⊗[R] Matrix n n R ≃ₐ[R] Matrix n n R ⊗[R] R[X]) :
          (a : R[X] ⊗[R] Matrix n n R) → Matrix n n R ⊗[R] R[X])
        ((monomial k : (a : R) → R[X]) x ⊗ₜ[R] single i j 1)) :
    (Matrix n n R)[X])
  ((monomial k : (a : Matrix n n R) → (Matrix n n R)[X]) (single i j x) : (Matrix n n R)[X])
Tactic: simp only [matPolyEquiv, AlgEquiv.trans_apply, matrixEquivTensor_apply_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
i j : n
k : ℕ
x : R
⊢ Eq (α := (Matrix n n R)[X])
    ((AlgEquiv.symm (polyEquivTensor R (Matrix n n R)) : (a : Matrix n n R ⊗[R] R[X]) → (Matrix n n R)[X])
        (((Algebra.TensorProduct.comm R R[X] (Matrix n n R) : R[X] ⊗[R] Matrix n n R ≃ₐ[R] Matrix n n R ⊗[R] R[X]) :
            (a : R[X] ⊗[R] Matrix n n R) → Matrix n n R ⊗[R] R[X])
          ((monomial k : (a : R) → R[X]) x ⊗ₜ[R] single i j 1)) :
      (Matrix n n R)[X])
    ((monomial k : (a : Matrix n n R) → (Matrix n n R)[X]) (single i j x) : (Matrix n n R)[X])
have a : Eq (α := Matrix n n R ⊗[R] R[X])
  ((polyEquivTensor R (Matrix n n R) : (a : (Matrix n n R)[X]) → Matrix n n R ⊗[R] R[X])
      ((AlgEquiv.symm (polyEquivTensor R (Matrix n n R)) : (a : Matrix n n R ⊗[R] R[X]) → (Matrix n n R)[X])
        (((Algebra.TensorProduct.comm R R[X] (Matrix n n R) : R[X] ⊗[R] Matrix n n R ≃ₐ[R] Matrix n n R ⊗[R] R[X]) :
            (a : R[X] ⊗[R] Matrix n n R) → Matrix n n R ⊗[R] R[X])
          ((monomial k : (a : R) → R[X]) x ⊗ₜ[R] single i j 1))) :
    Matrix n n R ⊗[R] R[X])
  ((polyEquivTensor R (Matrix n n R) : (a : (Matrix n n R)[X]) → Matrix n n R ⊗[R] R[X])
      ((monomial k : (a : Matrix n n R) → (Matrix n n R)[X]) (single i j x)) :
    Matrix n n R ⊗[R] R[X])
Tactic: apply (polyEquivTensor R (Matrix n n R)).injective
-- 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
i j : n
k : ℕ
x : R
⊢ Eq (α := Matrix n n R ⊗[R] R[X])
    ((polyEquivTensor R (Matrix n n R) : (a : (Matrix n n R)[X]) → Matrix n n R ⊗[R] R[X])
        ((AlgEquiv.symm (polyEquivTensor R (Matrix n n R)) : (a : Matrix n n R ⊗[R] R[X]) → (Matrix n n R)[X])
          (((Algebra.TensorProduct.comm R R[X] (Matrix n n R) : R[X] ⊗[R] Matrix n n R ≃ₐ[R] Matrix n n R ⊗[R] R[X]) :
              (a : R[X] ⊗[R] Matrix n n R) → Matrix n n R ⊗[R] R[X])
            ((monomial k : (a : R) → R[X]) x ⊗ₜ[R] single i j 1))) :
      Matrix n n R ⊗[R] R[X])
    ((polyEquivTensor R (Matrix n n R) : (a : (Matrix n n R)[X]) → Matrix n n R ⊗[R] R[X])
        ((monomial k : (a : Matrix n n R) → (Matrix n n R)[X]) (single i j x)) :
      Matrix n n R ⊗[R] R[X])
have a : single i j 1 ⊗ₜ[R] (monomial k : (a : R) → R[X]) x =
  HMul.hMul (α := Matrix n n R ⊗[R] R[X])
    (((↑includeLeft : Matrix n n R →+* Matrix n n R ⊗[R] R[X]) : (a : Matrix n n R) → Matrix n n R ⊗[R] R[X])
        (single i j x) :
      Matrix n n R ⊗[R] R[X])
    (HPow.hPow (α := Matrix n n R ⊗[R] R[X]) (1 ⊗ₜ[R] X) k)
Tactic: simp only [AlgEquiv.apply_symm_apply, Algebra.TensorProduct.comm_tmul,
    polyEquivTensor_apply, eval₂_monomial]
-- 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
i j : n
k : ℕ
x : R
⊢ single i j 1 ⊗ₜ[R] (monomial k : (a : R) → R[X]) x =
    HMul.hMul (α := Matrix n n R ⊗[R] R[X])
      (((↑includeLeft : Matrix n n R →+* Matrix n n R ⊗[R] R[X]) : (a : Matrix n n R) → Matrix n n R ⊗[R] R[X])
          (single i j x) :
        Matrix n n R ⊗[R] R[X])
      (HPow.hPow (α := Matrix n n R ⊗[R] R[X]) (1 ⊗ₜ[R] X) k)
have a : single i j 1 ⊗ₜ[R] (monomial k : (a : R) → R[X]) x =
  HMul.hMul (α := Matrix n n R ⊗[R] R[X]) (β := Matrix n n R ⊗[R] R[X])
    (((↑includeLeft : Matrix n n R →+* Matrix n n R ⊗[R] R[X]) : (a : Matrix n n R) → Matrix n n R ⊗[R] R[X])
        (single i j x) :
      Matrix n n R ⊗[R] R[X])
    (1 ⊗ₜ[R] HPow.hPow (α := R[X]) X k)
Tactic: simp only [one_pow,
    Algebra.TensorProduct.tmul_pow]
-- 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
i j : n
k : ℕ
x : R
⊢ single i j 1 ⊗ₜ[R] (monomial k : (a : R) → R[X]) x =
    HMul.hMul (α := Matrix n n R ⊗[R] R[X]) (β := Matrix n n R ⊗[R] R[X])
      (((↑includeLeft : Matrix n n R →+* Matrix n n R ⊗[R] R[X]) : (a : Matrix n n R) → Matrix n n R ⊗[R] R[X])
          (single i j x) :
        Matrix n n R ⊗[R] R[X])
      (1 ⊗ₜ[R] HPow.hPow (α := R[X]) X k)
have a : HSMul.hSMul (β := Matrix n n R) x (single i j 1) ⊗ₜ[R] HPow.hPow (α := R[X]) X k =
  HMul.hMul (α := Matrix n n R ⊗[R] R[X]) (β := Matrix n n R ⊗[R] R[X])
    (((↑includeLeft : Matrix n n R →+* Matrix n n R ⊗[R] R[X]) : (a : Matrix n n R) → Matrix n n R ⊗[R] R[X])
        (single i j x) :
      Matrix n n R ⊗[R] R[X])
    (1 ⊗ₜ[R] HPow.hPow (α := R[X]) X k)
Tactic: rw [← smul_X_eq_monomial, ← TensorProduct.smul_tmul]
-- 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
i j : n
k : ℕ
x : R
⊢ HSMul.hSMul (β := Matrix n n R) x (single i j 1) ⊗ₜ[R] HPow.hPow (α := R[X]) X k =
    HMul.hMul (α := Matrix n n R ⊗[R] R[X]) (β := Matrix n n R ⊗[R] R[X])
      (((↑includeLeft : Matrix n n R →+* Matrix n n R ⊗[R] R[X]) : (a : Matrix n n R) → Matrix n n R ⊗[R] R[X])
          (single i j x) :
        Matrix n n R ⊗[R] R[X])
      (1 ⊗ₜ[R] HPow.hPow (α := R[X]) X k)
have a : ∀ (i' j_1 : n),
  HSMul.hSMul (β := Matrix n n R) x (single i j 1) i' j_1 =
    ((((LinearMap.mul R (Matrix n n R) : (a : Matrix n n R) → Matrix n n R →ₗ[R] Matrix n n R) (single i j x, 1).1,
              (LinearMap.mul R R[X] : (a : R[X]) → R[X] →ₗ[R] R[X]) (single i j x, 1).2).1 :
          Matrix n n R →ₗ[R] Matrix n n R) :
        (a : Matrix n n R) → Matrix n n R)
      (1, HPow.hPow (α := R[X]) X k).1 i' j_1
Tactic: congr with i'
-- 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
i j : n
k : ℕ
x : R
a :
  ∀ (i' j_1 : n),
    HSMul.hSMul (β := Matrix n n R) x (single i j 1) i' j_1 =
      ((((LinearMap.mul R (Matrix n n R) : (a : Matrix n n R) → Matrix n n R →ₗ[R] Matrix n n R) (single i j x, 1).1,
                (LinearMap.mul R R[X] : (a : R[X]) → R[X] →ₗ[R] R[X]) (single i j x, 1).2).1 :
            Matrix n n R →ₗ[R] Matrix n n R) :
          (a : Matrix n n R) → Matrix n n R)
        (1, HPow.hPow (α := R[X]) X k).1 i' j_1
⊢ HSMul.hSMul (β := Matrix n n R) x (single i j 1) ⊗ₜ[R] HPow.hPow (α := R[X]) X k =
    HMul.hMul (α := Matrix n n R ⊗[R] R[X]) (β := Matrix n n R ⊗[R] R[X])
      (((↑includeLeft : Matrix n n R →+* Matrix n n R ⊗[R] R[X]) : (a : Matrix n n R) → Matrix n n R ⊗[R] R[X])
          (single i j x) :
        Matrix n n R ⊗[R] R[X])
      (1 ⊗ₜ[R] HPow.hPow (α := R[X]) X k)
have a₁ : ∀ (i' : ℕ),
  (HPow.hPow (α := R[X]) X k).coeff i' =
    coeff
      (((((LinearMap.mul R (Matrix n n R) : (a : Matrix n n R) → Matrix n n R →ₗ[R] Matrix n n R) (single i j x, 1).1,
                (LinearMap.mul R R[X] : (a : R[X]) → R[X] →ₗ[R] R[X]) (single i j x, 1).2) :
              (Matrix n n R →ₗ[R] Matrix n n R) × (R[X] →ₗ[R] R[X])).2 :
          (a : R[X]) → R[X])
        (1, HPow.hPow (α := R[X]) X k).2)
      i'
Tactic: congr with i'
-- 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
i j : n
p : R[X]
k : ℕ
⊢ coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (single i j p)) k = single i j (p.coeff k)
have refine_1 : ∀ (p q : R[X]),
  coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (single i j p)) k = single i j (p.coeff k) →
    coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (single i j q)) k = single i j (q.coeff k) →
      coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (single i j (p + q))) k =
        single i j ((p + q).coeff k)
Tactic: refine Polynomial.induction_on' p ?_ ?_
-- 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
i j : n
p : R[X]
k : ℕ
refine_1 :
  ∀ (p q : R[X]),
    coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (single i j p)) k = single i j (p.coeff k) →
      coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (single i j q)) k = single i j (q.coeff k) →
        coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (single i j (p + q))) k =
          single i j ((p + q).coeff k)
⊢ coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (single i j p)) k = single i j (p.coeff k)
have refine_2 : ∀ (n_1 : ℕ) (a : R),
  Eq (α := Matrix n n R)
    (coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (single i j ((monomial n_1 : (a : R) → R[X]) a)))
      k)
    (single i j (coeff ((monomial n_1 : (a : R) → R[X]) a) k))
Tactic: refine Polynomial.induction_on' p ?_ ?_
-- 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
i j : n
p_1 : R[X]
k : ℕ
p q : R[X]
hp : coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (single i j p)) k = single i j (p.coeff k)
hq : coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (single i j q)) k = single i j (q.coeff k)
⊢ coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (single i j (p + q))) k =
    single i j ((p + q).coeff k)
have refine_1 : ∀ (i_1 j_1 : n),
  coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (single i j (p + q))) k i_1 j_1 =
    single i j ((p + q).coeff k) i_1 j_1
Tactic: ext
-- 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
i j : n
p : R[X]
k_1 k : ℕ
x : R
⊢ Eq (α := Matrix n n R)
    (coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (single i j ((monomial k : (a : R) → R[X]) x)))
      k_1)
    (single i j (coeff ((monomial k : (a : R) → R[X]) x) k_1))
have refine_2 : (if k = k_1 then single i j x else 0) = single i j (if k = k_1 then x else 0)
Tactic: simp only [matPolyEquiv_coeff_apply_aux_1, coeff_monomial]
-- 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
i j : n
p : R[X]
k_1 k : ℕ
x : R
⊢ (if k = k_1 then single i j x else 0) = single i j (if k = k_1 then x else 0)
have pos : k = k_1 → single i j x = single i j x
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
i j : n
p : R[X]
k_1 k : ℕ
x : R
pos : k = k_1 → single i j x = single i j x
⊢ (if k = k_1 then single i j x else 0) = single i j (if k = k_1 then x else 0)
have neg : ¬k = k_1 → Eq (α := Matrix n n R) 0 (single i j 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
i j : n
p : R[X]
k_1 k : ℕ
x : R
h : k = k_1
⊢ single i j x = single i j x
have pos : ∀ (x_1 x_2 : n), single i j x x_1 x_2 = single i j x x_1 x_2
Tactic: funext
-- 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
i j : n
p : R[X]
k_1 k : ℕ
x : R
h : ¬k = k_1
⊢ Eq (α := Matrix n n R) 0 (single i j 0)
have neg : ∀ (x x_1 : n), Eq.{u_1 + 1} (α := R) (0 x x_1) (single i j 0 x x_1)
Tactic: funext
-- 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
⊢ coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) m) k i j = (m i j).coeff k
have 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)
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 : 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)
⊢ coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) m) k i j = (m i j).coeff k
have 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
Tactic: refine Matrix.induction_on' m ?_ ?_ ?_