awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
rw :
  Polynomial.map
      (↑(bind₁
            (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := End A (TensorProduct R A M)) (basis A b)
              (Basis.end (basis A bₘ)) (tensorProduct R A M M ∘ₗ baseChange A φ))) :
        MvPolynomial (ιM × ιM) A →+* MvPolynomial ι A)
      (Polynomial.map (R := MvPolynomial.{u_7, u_1} (ιM × ιM) R) (MvPolynomial.map (algebraMap R A))
        (charpoly.univ R ιM)) =
    Polynomial.map (MvPolynomial.map (algebraMap R A))
      (Polynomial.map (↑(bind₁ (toMvPolynomial b bₘ.end φ)) : MvPolynomial (ιM × ιM) R →+* MvPolynomial ι R)
        (charpoly.univ R ιM))
⊢ Polynomial.map
      (↑(bind₁
            (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := End A (TensorProduct R A M)) (basis A b)
              (Basis.end (basis A bₘ)) (tensorProduct R A M M ∘ₗ baseChange A φ))) :
        MvPolynomial (ιM × ιM) A →+* MvPolynomial ι A)
      (charpoly.univ A ιM) =
    Polynomial.map (MvPolynomial.map (algebraMap R A))
      (Polynomial.map (↑(bind₁ (toMvPolynomial b bₘ.end φ)) : MvPolynomial (ιM × ιM) R →+* MvPolynomial ι R)
        (charpoly.univ R ιM))

Tactic:
rw [← charpoly.univ_map_map _ (algebraMap R A)]

Premises used: Matrix.charpoly.univ_map_map, Algebra.algebraMap
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
simp :
  Polynomial.map (R := MvPolynomial.{u_7, u_1} (ιM × ιM) R)
      (RingHom.comp
        (↑(bind₁
              (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := End A (TensorProduct R A M)) (basis A b)
                (Basis.end (basis A bₘ)) (tensorProduct R A M M ∘ₗ baseChange A φ))) :
          MvPolynomial (ιM × ιM) A →+* MvPolynomial ι A)
        (MvPolynomial.map (algebraMap R A)))
      (charpoly.univ R ιM) =
    Polynomial.map
      (RingHom.comp (MvPolynomial.map (algebraMap R A))
        (↑(bind₁ (toMvPolynomial b bₘ.end φ)) : MvPolynomial (ιM × ιM) R →+* MvPolynomial ι R))
      (charpoly.univ R ιM)
⊢ Polynomial.map
      (↑(bind₁
            (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := End A (TensorProduct R A M)) (basis A b)
              (Basis.end (basis A bₘ)) (tensorProduct R A M M ∘ₗ baseChange A φ))) :
        MvPolynomial (ιM × ιM) A →+* MvPolynomial ι A)
      (Polynomial.map (R := MvPolynomial.{u_7, u_1} (ιM × ιM) R) (MvPolynomial.map (algebraMap R A))
        (charpoly.univ R ιM)) =
    Polynomial.map (MvPolynomial.map (algebraMap R A))
      (Polynomial.map (↑(bind₁ (toMvPolynomial b bₘ.end φ)) : MvPolynomial (ιM × ιM) R →+* MvPolynomial ι R)
        (charpoly.univ R ιM))

Tactic:
simp only [Polynomial.map_map]

Premises used: Polynomial.map_map
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
e_f :
  RingHom.comp
      (↑(bind₁
            (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := End A (TensorProduct R A M)) (basis A b)
              (Basis.end (basis A bₘ)) (tensorProduct R A M M ∘ₗ baseChange A φ))) :
        MvPolynomial (ιM × ιM) A →+* MvPolynomial ι A)
      (MvPolynomial.map (algebraMap R A)) =
    RingHom.comp (MvPolynomial.map (algebraMap R A))
      (↑(bind₁ (toMvPolynomial b bₘ.end φ)) : MvPolynomial (ιM × ιM) R →+* MvPolynomial ι R)
⊢ Polynomial.map (R := MvPolynomial.{u_7, u_1} (ιM × ιM) R)
      (RingHom.comp
        (↑(bind₁
              (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := End A (TensorProduct R A M)) (basis A b)
                (Basis.end (basis A bₘ)) (tensorProduct R A M M ∘ₗ baseChange A φ))) :
          MvPolynomial (ιM × ιM) A →+* MvPolynomial ι A)
        (MvPolynomial.map (algebraMap R A)))
      (charpoly.univ R ιM) =
    Polynomial.map
      (RingHom.comp (MvPolynomial.map (algebraMap R A))
        (↑(bind₁ (toMvPolynomial b bₘ.end φ)) : MvPolynomial (ιM × ιM) R →+* MvPolynomial ι R))
      (charpoly.univ R ιM)

Tactic:
congr 1
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
e_f :
  ∀ (r : R),
    Eq (α := MvPolynomial ι A)
      ((RingHom.comp
              (↑(bind₁
                    (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := End A (TensorProduct R A M)) (basis A b)
                      (Basis.end (basis A bₘ)) (tensorProduct R A M M ∘ₗ baseChange A φ))) :
                MvPolynomial (ιM × ιM) A →+* MvPolynomial ι A)
              (MvPolynomial.map (algebraMap R A)) :
            (a : MvPolynomial (ιM × ιM) R) → MvPolynomial ι A)
          ((C : (a : R) → MvPolynomial (ιM × ιM) R) r) :
        MvPolynomial ι A)
      ((RingHom.comp (MvPolynomial.map (algebraMap R A))
              (↑(bind₁ (toMvPolynomial b bₘ.end φ)) : MvPolynomial (ιM × ιM) R →+* MvPolynomial ι R) :
            (a : MvPolynomial (ιM × ιM) R) → MvPolynomial ι A)
          ((C : (a : R) → MvPolynomial (ιM × ιM) R) r) :
        MvPolynomial ι A)
e_f₁ :
  ∀ (i : ιM × ιM),
    Eq (α := MvPolynomial ι A)
      ((RingHom.comp
              (↑(bind₁
                    (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := End A (TensorProduct R A M)) (basis A b)
                      (Basis.end (basis A bₘ)) (tensorProduct R A M M ∘ₗ baseChange A φ))) :
                MvPolynomial (ιM × ιM) A →+* MvPolynomial ι A)
              (MvPolynomial.map (algebraMap R A)) :
            (a : MvPolynomial (ιM × ιM) R) → MvPolynomial ι A)
          (X i) :
        MvPolynomial ι A)
      ((RingHom.comp (MvPolynomial.map (algebraMap R A))
              (↑(bind₁ (toMvPolynomial b bₘ.end φ)) : MvPolynomial (ιM × ιM) R →+* MvPolynomial ι R) :
            (a : MvPolynomial (ιM × ιM) R) → MvPolynomial ι A)
          (X i) :
        MvPolynomial ι A)
⊢ RingHom.comp
      (↑(bind₁
            (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := End A (TensorProduct R A M)) (basis A b)
              (Basis.end (basis A bₘ)) (tensorProduct R A M M ∘ₗ baseChange A φ))) :
        MvPolynomial (ιM × ιM) A →+* MvPolynomial ι A)
      (MvPolynomial.map (algebraMap R A)) =
    RingHom.comp (MvPolynomial.map (algebraMap R A))
      (↑(bind₁ (toMvPolynomial b bₘ.end φ)) : MvPolynomial (ιM × ιM) R →+* MvPolynomial ι R)

Tactic:
apply MvPolynomial.ringHom_ext

Premises used: MvPolynomial.ringHom_ext
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
r : R
⊢ Eq (α := MvPolynomial ι A)
    ((RingHom.comp
            (↑(bind₁
                  (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := End A (TensorProduct R A M)) (basis A b)
                    (Basis.end (basis A bₘ)) (tensorProduct R A M M ∘ₗ baseChange A φ))) :
              MvPolynomial (ιM × ιM) A →+* MvPolynomial ι A)
            (MvPolynomial.map (algebraMap R A)) :
          (a : MvPolynomial (ιM × ιM) R) → MvPolynomial ι A)
        ((C : (a : R) → MvPolynomial (ιM × ιM) R) r) :
      MvPolynomial ι A)
    ((RingHom.comp (MvPolynomial.map (algebraMap R A))
            (↑(bind₁ (toMvPolynomial b bₘ.end φ)) : MvPolynomial (ιM × ιM) R →+* MvPolynomial ι R) :
          (a : MvPolynomial (ιM × ιM) R) → MvPolynomial ι A)
        ((C : (a : R) → MvPolynomial (ιM × ιM) R) r) :
      MvPolynomial ι A)

Tactic:
simp only [RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, map_C, bind₁_C_right]

Premises used: RingHom.coe_coe, MvPolynomial.bind₁_C_right, MvPolynomial.map_C, RingHom.coe_comp, Function.comp_apply
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
ij : ιM × ιM
e_f :
  Eq (α := MvPolynomial ι A)
    (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := End A (TensorProduct R A M)) (basis A b) (Basis.end (basis A bₘ))
      (tensorProduct R A M M ∘ₗ baseChange A φ) ij)
    ((MvPolynomial.map (algebraMap R A) : (a : MvPolynomial ι R) → MvPolynomial ι A) (toMvPolynomial b bₘ.end φ ij))
⊢ Eq (α := MvPolynomial ι A)
    ((RingHom.comp
            (↑(bind₁
                  (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := End A (TensorProduct R A M)) (basis A b)
                    (Basis.end (basis A bₘ)) (tensorProduct R A M M ∘ₗ baseChange A φ))) :
              MvPolynomial (ιM × ιM) A →+* MvPolynomial ι A)
            (MvPolynomial.map (algebraMap R A)) :
          (a : MvPolynomial (ιM × ιM) R) → MvPolynomial ι A)
        (X ij) :
      MvPolynomial ι A)
    ((RingHom.comp (MvPolynomial.map (algebraMap R A))
            (↑(bind₁ (toMvPolynomial b bₘ.end φ)) : MvPolynomial (ιM × ιM) R →+* MvPolynomial ι R) :
          (a : MvPolynomial (ιM × ιM) R) → MvPolynomial ι A)
        (X ij) :
      MvPolynomial ι A)

Tactic:
simp only [RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, map_X, bind₁_X_right]

Premises used: RingHom.coe_coe, RingHom.coe_comp, Function.comp_apply, MvPolynomial.bind₁_X_right, MvPolynomial.map_X
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
ij : ιM × ιM
e_f :
  Eq (α := MvPolynomial ι A)
    ((bind₁
            (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (basis A b)
              (basis A bₘ.end) (baseChange A φ)) :
          (a : MvPolynomial (ιM × ιM) A) → MvPolynomial ι A)
        (toMvPolynomial (M₁ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (M₂ := End A (TensorProduct R A M))
          (basis A bₘ.end) (Basis.end (basis A bₘ)) (tensorProduct R A M M) ij) :
      MvPolynomial ι A)
    (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (basis A b)
        (basis A bₘ.end) (baseChange A φ) ij :
      MvPolynomial ι A)
⊢ Eq (α := MvPolynomial ι A)
    (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := End A (TensorProduct R A M)) (basis A b) (Basis.end (basis A bₘ))
      (tensorProduct R A M M ∘ₗ baseChange A φ) ij)
    ((MvPolynomial.map (algebraMap R A) : (a : MvPolynomial ι R) → MvPolynomial ι A) (toMvPolynomial b bₘ.end φ ij))

Tactic:
rw [toMvPolynomial_comp _ (basis A (Basis.end bₘ)), ← toMvPolynomial_baseChange]

Premises used: LinearMap.toMvPolynomial_baseChange, Module.Basis.end, LinearMap.toMvPolynomial_comp, Algebra.TensorProduct.basis
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
ij : ιM × ιM
this :
  Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    (toMvPolynomial (M₁ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (M₂ := End A (TensorProduct R A M))
      (basis A bₘ.end) (Basis.end (basis A bₘ)) (tensorProduct R A M M) ij)
    (X ij)
rw :
  Eq (α := MvPolynomial ι A)
    ((bind₁
            (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (basis A b)
              (basis A bₘ.end) (baseChange A φ)) :
          (a : MvPolynomial (ιM × ιM) A) → MvPolynomial ι A)
        (X ij) :
      MvPolynomial ι A)
    (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (basis A b)
        (basis A bₘ.end) (baseChange A φ) ij :
      MvPolynomial ι A)
rw₁ rw₂ :
  Eq (α := MvPolynomial ι A)
    (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (basis A b)
      (basis A bₘ.end) (baseChange A φ) ij)
    (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (basis A b)
      (basis A bₘ.end) (baseChange A φ) ij)
⊢ Eq (α := MvPolynomial ι A)
    ((bind₁
            (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (basis A b)
              (basis A bₘ.end) (baseChange A φ)) :
          (a : MvPolynomial (ιM × ιM) A) → MvPolynomial ι A)
        (toMvPolynomial (M₁ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (M₂ := End A (TensorProduct R A M))
          (basis A bₘ.end) (Basis.end (basis A bₘ)) (tensorProduct R A M M) ij) :
      MvPolynomial ι A)
    (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (basis A b)
        (basis A bₘ.end) (baseChange A φ) ij :
      MvPolynomial ι A)

Tactic:
rw [this, bind₁_X_right]

Premises used: MvPolynomial.bind₁_X_right
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
ij : ιM × ιM
e_f :
  Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    (toMvPolynomial (M₁ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (M₂ := End A (TensorProduct R A M))
      (basis A bₘ.end) (Basis.end (basis A bₘ)) (tensorProduct R A M M) ij)
    (X ij)
⊢ Eq (α := MvPolynomial ι A)
    ((bind₁
            (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (basis A b)
              (basis A bₘ.end) (baseChange A φ)) :
          (a : MvPolynomial (ιM × ιM) A) → MvPolynomial ι A)
        (toMvPolynomial (M₁ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (M₂ := End A (TensorProduct R A M))
          (basis A bₘ.end) (Basis.end (basis A bₘ)) (tensorProduct R A M M) ij) :
      MvPolynomial ι A)
    (toMvPolynomial (M₁ := TensorProduct R A L) (M₂ := TensorProduct.{u_1, u_8, u_3} R A (End R M)) (basis A b)
        (basis A bₘ.end) (baseChange A φ) ij :
      MvPolynomial ι A)

Tactic:
suffices toMvPolynomial (M₂ := (Module.End A (TensorProduct R A M)))
        (basis A bₘ.end) (basis A bₘ).end (tensorProduct R A M M) ij = X ij by
      rw [this, bind₁_X_right]
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
ij : ιM × ιM
this :
  ∀ (kl : ιM × ιM),
    Eq.{u_8 + 1} (α := A)
      ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
            (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
          (tensorProduct R A M M) ij kl :
        A)
      (if kl = ij then 1 else 0 : A)
rw :
  Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    ((monomial (Finsupp.single ij 1) : (a : A) → MvPolynomial (ιM × ιM) A)
        ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
            (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
          (tensorProduct R A M M) ij ij) :
      MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    (X ij : MvPolynomial.{u_7, u_8} (ιM × ιM) A)
h₀ :
  ∀ (b : ιM × ιM),
    Membership.mem (γ := Finset (ιM × ιM)) Finset.univ b →
      b ≠ ij →
        Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
          ((monomial (Finsupp.single b 1) : (a : A) → MvPolynomial (ιM × ιM) A)
              ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
                  (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
                (tensorProduct R A M M) ij b) :
            MvPolynomial.{u_7, u_8} (ιM × ιM) A)
          (0 : MvPolynomial.{u_7, u_8} (ιM × ιM) A)
h₁ :
  ij ∉ Finset.univ →
    Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
      ((monomial (Finsupp.single ij 1) : (a : A) → MvPolynomial (ιM × ιM) A)
          ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
              (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
            (tensorProduct R A M M) ij ij) :
        MvPolynomial.{u_7, u_8} (ιM × ιM) A)
      (0 : MvPolynomial.{u_7, u_8} (ιM × ιM) A)
⊢ Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    (∑ j : ιM × ιM,
      (monomial (Finsupp.single j 1) : (a : A) → MvPolynomial (ιM × ιM) A)
        ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
            (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
          (tensorProduct R A M M) ij j))
    (X ij)

Tactic:
rw [Finset.sum_eq_single ij]

Premises used: Finset.sum_eq_single
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
ij : ιM × ιM
this :
  ∀ (kl : ιM × ιM),
    Eq.{u_8 + 1} (α := A)
      ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
            (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
          (tensorProduct R A M M) ij kl :
        A)
      (if kl = ij then 1 else 0 : A)
rw :
  Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    ((monomial (Finsupp.single ij 1) : (a : A) → MvPolynomial (ιM × ιM) A) (if ij = ij then 1 else 0)) (X ij)
rw₁ :
  Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    ((monomial (Finsupp.single ij 1) : (a : A) → MvPolynomial (ιM × ιM) A) 1) (X ij)
rw₂ rw₃ :
  Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    ((monomial (Finsupp.single ij 1) : (a : A) → MvPolynomial (ιM × ιM) A) 1)
    ((monomial (Finsupp.single ij 1) : (a : A) → MvPolynomial (ιM × ιM) A) 1)
⊢ Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    ((monomial (Finsupp.single ij 1) : (a : A) → MvPolynomial (ιM × ιM) A)
        ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
            (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
          (tensorProduct R A M M) ij ij) :
      MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    (X ij : MvPolynomial.{u_7, u_8} (ιM × ιM) A)

Tactic:
rw [this, if_pos rfl, X]

Premises used: MvPolynomial.X, if_pos, rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
ij : ιM × ιM
this :
  ∀ (kl : ιM × ιM),
    Eq.{u_8 + 1} (α := A)
      ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
            (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
          (tensorProduct R A M M) ij kl :
        A)
      (if kl = ij then 1 else 0 : A)
kl : ιM × ιM
H : kl ≠ ij
h₀ :
  Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    ((monomial (Finsupp.single kl 1) : (a : A) → MvPolynomial (ιM × ιM) A) (if kl = ij then 1 else 0)) 0
h₁ :
  Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    ((monomial (Finsupp.single kl 1) : (a : A) → MvPolynomial (ιM × ιM) A) 0) 0
h₂ h₃ : Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A) 0 0
⊢ Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    ((monomial (Finsupp.single kl 1) : (a : A) → MvPolynomial (ιM × ιM) A)
        ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
            (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
          (tensorProduct R A M M) ij kl) :
      MvPolynomial.{u_7, u_8} (ιM × ιM) A)
    (0 : MvPolynomial.{u_7, u_8} (ιM × ιM) A)

Tactic:
rw [this, if_neg H, map_zero]

Premises used: map_zero, if_neg
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Fintype ι
inst_6 : Fintype ιM
inst_7 : DecidableEq ι
inst_8 : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst_9 : CommRing A
inst_10 : Algebra R A
ij : ιM × ιM
this :
  ∀ (kl : ιM × ιM),
    Eq.{u_8 + 1} (α := A)
      ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
            (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
          (tensorProduct R A M M) ij kl :
        A)
      (if kl = ij then 1 else 0 : A)
⊢ ij ∉ Finset.univ →
    Eq (α := MvPolynomial.{u_7, u_8} (ιM × ιM) A)
      ((monomial (Finsupp.single ij 1) : (a : A) → MvPolynomial (ιM × ιM) A)
          ((toMatrix (basis A bₘ.end) (Basis.end (basis A bₘ)) :
              (a : TensorProduct R A (End R M) →ₗ[A] End A (TensorProduct R A M)) → Matrix (ιM × ιM) (ιM × ιM) A)
            (tensorProduct R A M M) ij ij) :
        MvPolynomial.{u_7, u_8} (ιM × ιM) A)
      (0 : MvPolynomial.{u_7, u_8} (ιM × ιM) A)

Tactic:
grind