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
ij : ιM × ιM
e_f :
  ∀ (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)
⊢ 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:
suffices ∀ kl,
        (toMatrix (basis A bₘ.end) (basis A bₘ).end) (tensorProduct R A M M) ij kl =
        if kl = ij then 1 else 0 by
      rw [Finset.sum_eq_single ij]
      · rw [this, if_pos rfl, X]
      · rintro kl - H
        rw [this, if_neg H, map_zero]
      · grind
-- 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 kl : ιM × ιM
e_f :
  Eq.{u_8 + 1} (α := A)
    ((((Basis.repr (Basis.end (basis A bₘ)) : (a : End A (TensorProduct R A M)) → ιM × ιM →₀ A)
              ((({
                        toFun := fun (a : A) ↦
                          HSMul.hSMul (β := (M →ₗ[R] M) →ₗ[R] TensorProduct R A M →ₗ[A] TensorProduct R A M) a
                            (baseChangeHom R A M M),
                        map_add' := ⋯, map_smul' := ⋯ } :
                      (a : A) → (M →ₗ[R] M) →ₗ[R] TensorProduct R A M →ₗ[A] TensorProduct R A M)
                    1 :
                  (a : M →ₗ[R] M) → TensorProduct R A M →ₗ[A] TensorProduct R A M)
                ((bₘ.end : (a : ιM × ιM) → End R M) kl)) :
            Finsupp.{u_7, u_8} (ιM × ιM) A) :
          (a : ιM × ιM) → A)
        ij :
      A)
    (if kl = ij then 1 else 0 : A)
⊢ 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)

Tactic:
rw [toMatrix_apply, tensorProduct, TensorProduct.AlgebraTensorModule.lift_apply,
      basis_apply, TensorProduct.lift.tmul, coe_restrictScalars]

Premises used: Algebra.TensorProduct.basis_apply, LinearMap.coe_restrictScalars, TensorProduct.lift.tmul, TensorProduct.AlgebraTensorModule.lift_apply, LinearMap.toMatrix_apply, LinearMap.tensorProduct
-- 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 kl : ιM × ιM
e_f :
  Eq.{u_8 + 1} (α := A)
    ((((Basis.repr (Basis.end (basis A bₘ)) : (a : End A (TensorProduct R A M)) → ιM × ιM →₀ A)
              (HSMul.hSMul (α := A) (β := TensorProduct R A M →ₗ[A] TensorProduct R A M) 1
                (baseChange A ((bₘ.end : (a : ιM × ιM) → End R M) kl))) :
            Finsupp.{u_7, u_8} (ιM × ιM) A) :
          (a : ιM × ιM) → A)
        ij :
      A)
    (if kl = ij then 1 else 0 : A)
⊢ Eq.{u_8 + 1} (α := A)
    ((((Basis.repr (Basis.end (basis A bₘ)) : (a : End A (TensorProduct R A M)) → ιM × ιM →₀ A)
              ((({
                        toFun := fun (a : A) ↦
                          HSMul.hSMul (β := (M →ₗ[R] M) →ₗ[R] TensorProduct R A M →ₗ[A] TensorProduct R A M) a
                            (baseChangeHom R A M M),
                        map_add' := ⋯, map_smul' := ⋯ } :
                      (a : A) → (M →ₗ[R] M) →ₗ[R] TensorProduct R A M →ₗ[A] TensorProduct R A M)
                    1 :
                  (a : M →ₗ[R] M) → TensorProduct R A M →ₗ[A] TensorProduct R A M)
                ((bₘ.end : (a : ιM × ιM) → End R M) kl)) :
            Finsupp.{u_7, u_8} (ιM × ιM) A) :
          (a : ιM × ιM) → A)
        ij :
      A)
    (if kl = ij then 1 else 0 : A)

Tactic:
dsimp only [coe_mk, AddHom.coe_mk, smul_apply, baseChangeHom_apply]

Premises used: LinearMap.coe_mk, LinearMap.smul_apply, AddHom.coe_mk, LinearMap.baseChangeHom_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 kl : ιM × ιM
e_f :
  Eq.{u_8 + 1} (α := A)
    ((((Basis.repr (Basis.end (basis A bₘ)) : (a : End A (TensorProduct R A M)) → ιM × ιM →₀ A)
              (baseChange A ((bₘ.end : (a : ιM × ιM) → End R M) kl)) :
            Finsupp.{u_7, u_8} (ιM × ιM) A) :
          (a : ιM × ιM) → A)
        ij :
      A)
    (if kl = ij then 1 else 0 : A)
e_f₁ :
  Eq.{u_8 + 1} (α := A)
    ((((Basis.repr (Basis.end (basis A bₘ)) : (a : End A (TensorProduct R A M)) → ιM × ιM →₀ A)
              ((Basis.end (basis A bₘ) : (a : ιM × ιM) → End A (TensorProduct R A M)) kl) :
            Finsupp.{u_7, u_8} (ιM × ιM) A) :
          (a : ιM × ιM) → A)
        ij :
      A)
    (if kl = ij then 1 else 0 : A)
e_f₂ e_f₃ : Eq.{u_8 + 1} (α := A) (if kl = ij then 1 else 0) (if kl = ij then 1 else 0)
⊢ Eq.{u_8 + 1} (α := A)
    ((((Basis.repr (Basis.end (basis A bₘ)) : (a : End A (TensorProduct R A M)) → ιM × ιM →₀ A)
              (HSMul.hSMul (α := A) (β := TensorProduct R A M →ₗ[A] TensorProduct R A M) 1
                (baseChange A ((bₘ.end : (a : ιM × ιM) → End R M) kl))) :
            Finsupp.{u_7, u_8} (ιM × ιM) A) :
          (a : ιM × ιM) → A)
        ij :
      A)
    (if kl = ij then 1 else 0 : A)

Tactic:
rw [one_smul, Basis.baseChange_end, Basis.repr_self_apply]

Premises used: Module.Basis.repr_self_apply, Module.Basis.baseChange_end, one_smul
-- 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
x : L
rw :
  Eq.{u_1 + 1} (α := Polynomial R)
    (Matrix.charpoly.{u_1, u_7} (n := ιM)
      ((of : (a : ιM → ιM → R) → Matrix ιM ιM R)
        (Function.curry fun (i : ιM × ιM) ↦
          (eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) : (a : MvPolynomial ι R) → R)
            (toMvPolynomial b bₘ.end φ i))))
    (Matrix.charpoly.{u_1, u_7} (n := ιM)
      ((toMatrix bₘ bₘ : (a : M →ₗ[R] M) → Matrix ιM ιM R) ((φ : (a : L) → End R M) x)))
⊢ Polynomial.map (eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R)) (φ.polyCharpolyAux b bₘ) =
    Matrix.charpoly.{u_1, u_7} (n := ιM)
      ((toMatrix bₘ bₘ : (a : M →ₗ[R] M) → Matrix ιM ιM R) ((φ : (a : L) → End R M) x))

Tactic:
rw [polyCharpolyAux, Polynomial.map_map, ← MvPolynomial.eval₂Hom_C_eq_bind₁,
    MvPolynomial.comp_eval₂Hom, charpoly.univ_map_eval₂Hom]

Premises used: LinearMap.polyCharpolyAux, MvPolynomial.comp_eval₂Hom, MvPolynomial.eval₂Hom_C_eq_bind₁, Matrix.charpoly.univ_map_eval₂Hom, 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
x : L
e_M :
  Eq (α := Matrix ιM ιM R)
    ((of : (a : ιM → ιM → R) → Matrix ιM ιM R)
        (Function.curry fun (i : ιM × ιM) ↦
          (eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) : (a : MvPolynomial ι R) → R)
            (toMvPolynomial b bₘ.end φ i)) :
      Matrix ιM ιM R)
    ((toMatrix bₘ bₘ : (a : M →ₗ[R] M) → Matrix ιM ιM R) ((φ : (a : L) → End R M) x) : Matrix ιM ιM R)
⊢ Eq.{u_1 + 1} (α := Polynomial R)
    (Matrix.charpoly.{u_1, u_7} (n := ιM)
      ((of : (a : ιM → ιM → R) → Matrix ιM ιM R)
        (Function.curry fun (i : ιM × ιM) ↦
          (eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) : (a : MvPolynomial ι R) → R)
            (toMvPolynomial b bₘ.end φ i))))
    (Matrix.charpoly.{u_1, u_7} (n := ιM)
      ((toMatrix bₘ bₘ : (a : M →ₗ[R] M) → Matrix ιM ιM R) ((φ : (a : L) → End R M) x)))

Tactic:
congr
-- 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
x : L
e_M :
  ∀ (i j : ιM),
    Eq.{u_1 + 1} (α := R)
      ((of : (a : ιM → ιM → R) → Matrix ιM ιM R)
          (Function.curry fun (i : ιM × ιM) ↦
            (eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) : (a : MvPolynomial ι R) → R)
              (toMvPolynomial b bₘ.end φ i))
          i j :
        R)
      ((toMatrix bₘ bₘ : (a : M →ₗ[R] M) → Matrix ιM ιM R) ((φ : (a : L) → End R M) x) i j : R)
⊢ Eq (α := Matrix ιM ιM R)
    ((of : (a : ιM → ιM → R) → Matrix ιM ιM R)
        (Function.curry fun (i : ιM × ιM) ↦
          (eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) : (a : MvPolynomial ι R) → R)
            (toMvPolynomial b bₘ.end φ i)) :
      Matrix ιM ιM R)
    ((toMatrix bₘ bₘ : (a : M →ₗ[R] M) → Matrix ιM ιM R) ((φ : (a : L) → End R M) x) : Matrix ιM ιM R)

Tactic:
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
x : L
i j : ιM
e_M :
  Eq.{u_1 + 1} (α := R)
    ((((bₘ.end.repr : (a : End R M) → ιM × ιM →₀ R) ((φ : (a : L) → End R M) x) : Finsupp.{u_7, u_1} (ιM × ιM) R) :
          (a : ιM × ιM) → R)
        (i, j) :
      R)
    ((toMatrix bₘ bₘ : (a : M →ₗ[R] M) → Matrix ιM ιM R) ((φ : (a : L) → End R M) x) i j : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((of : (a : ιM → ιM → R) → Matrix ιM ιM R)
        (Function.curry fun (i : ιM × ιM) ↦
          (eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) : (a : MvPolynomial ι R) → R)
            (toMvPolynomial b bₘ.end φ i))
        i j :
      R)
    ((toMatrix bₘ bₘ : (a : M →ₗ[R] M) → Matrix ιM ιM R) ((φ : (a : L) → End R M) x) i j : R)

Tactic:
rw [of_apply, Function.curry_apply, toMvPolynomial_eval_eq_apply, LinearEquiv.symm_apply_apply]

Premises used: LinearEquiv.symm_apply_apply, Matrix.of_apply, Function.curry_apply, LinearMap.toMvPolynomial_eval_eq_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
x : L
i j : ιM
⊢ Eq.{u_1 + 1} (α := R)
    ((((bₘ.end.repr : (a : End R M) → ιM × ιM →₀ R) ((φ : (a : L) → End R M) x) : Finsupp.{u_7, u_1} (ιM × ιM) R) :
          (a : ιM × ιM) → R)
        (i, j) :
      R)
    ((toMatrix bₘ bₘ : (a : M →ₗ[R] M) → Matrix ιM ιM R) ((φ : (a : L) → End R M) x) i j : R)

Tactic:
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
x : L
i : ℕ
⊢ Eq.{u_1 + 1} (α := R)
    ((eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) : (a : MvPolynomial ι R) → R)
        ((φ.polyCharpolyAux b bₘ).coeff i) :
      R)
    (Polynomial.coeff
        (Matrix.charpoly.{u_1, u_7} (n := ιM)
          ((toMatrix bₘ bₘ : (a : M →ₗ[R] M) → Matrix ιM ιM R) ((φ : (a : L) → End R M) x)))
        i :
      R)

Tactic:
simp [← polyCharpolyAux_map_eq_toMatrix_charpoly φ b bₘ x]

Premises used: LinearMap.polyCharpolyAux_map_eq_toMatrix_charpoly
-- 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
inst_9 : Module.Finite R M
inst_10 : Free R M
x : L
⊢ Nontrivial R

Tactic:
nontriviality R
-- 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
inst_9 : Module.Finite R M
inst_10 : Free R M
x : L
h : Nontrivial R
rw :
  Eq.{u_1 + 1} (α := Polynomial R)
    (Matrix.charpoly.{u_1, u_7} (n := ιM)
      ((toMatrix bₘ bₘ : (a : M →ₗ[R] M) → Matrix ιM ιM R) ((φ : (a : L) → End R M) x)))
    (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x))
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := Polynomial R) (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x))
    (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x))
⊢ Polynomial.map (eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R)) (φ.polyCharpolyAux b bₘ) =
    charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)

Tactic:
rw [polyCharpolyAux_map_eq_toMatrix_charpoly, LinearMap.charpoly_toMatrix]

Premises used: LinearMap.charpoly_toMatrix, LinearMap.polyCharpolyAux_map_eq_toMatrix_charpoly
-- 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
inst_9 : Module.Finite R M
inst_10 : Free R M
x : L
i : ℕ
⊢ Nontrivial R

Tactic:
nontriviality R
-- 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
inst_9 : Module.Finite R M
inst_10 : Free R M
x : L
i : ℕ
h : Nontrivial R
rw :
  (eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) : (a : MvPolynomial ι R) → R)
      ((φ.polyCharpolyAux b bₘ).coeff i) =
    (Polynomial.map (eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R)) (φ.polyCharpolyAux b bₘ)).coeff i
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := R)
    ((eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) : (a : MvPolynomial ι R) → R)
        ((φ.polyCharpolyAux b bₘ).coeff i) :
      R)
    ((eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) : (a : MvPolynomial ι R) → R)
        ((φ.polyCharpolyAux b bₘ).coeff i) :
      R)
⊢ Eq.{u_1 + 1} (α := R)
    ((eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) : (a : MvPolynomial ι R) → R)
        ((φ.polyCharpolyAux b bₘ).coeff i) :
      R)
    (Polynomial.coeff (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) i : R)

Tactic:
rw [← polyCharpolyAux_map_eq_charpoly φ b bₘ x, Polynomial.coeff_map]

Premises used: Polynomial.coeff_map, LinearMap.polyCharpolyAux_map_eq_charpoly
-- 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
inst_9 : Module.Finite R M
inst_10 : Free R M
x : ι → R
⊢ Polynomial.map (eval x) (φ.polyCharpolyAux b bₘ) =
    charpoly.{u_1, u_3} (M := M)
      ((φ : (a : L) → End R M)
        ((b.repr.symm : (a : ι →₀ R) → L) ((Equiv.symm Finsupp.equivFunOnFinite : (a : ι → R) → ι →₀ R) x : ι →₀ R)))

Tactic:
simp only [← polyCharpolyAux_map_eq_charpoly φ b bₘ, LinearEquiv.apply_symm_apply,
    Finsupp.equivFunOnFinite, Equiv.coe_fn_symm_mk, Finsupp.coe_mk]

Premises used: Equiv.coe_fn_symm_mk, Finsupp.equivFunOnFinite, LinearMap.polyCharpolyAux_map_eq_charpoly, LinearEquiv.apply_symm_apply, Finsupp.coe_mk
-- 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
inst_11 : Module.Finite A (A ⊗[R] M)
inst_12 : Free A (A ⊗[R] M)
x : ι → A
rw :
  Eq (α := Polynomial A) (Polynomial.map (AlgHom.toRingHom (aeval x)) (φ.polyCharpolyAux b bₘ))
    (Polynomial.map (RingHom.comp (eval x) (MvPolynomial.map (algebraMap R A))) (φ.polyCharpolyAux b bₘ))
⊢ Eq (α := Polynomial A) (Polynomial.map (AlgHom.toRingHom (aeval x)) (φ.polyCharpolyAux b bₘ))
    (charpoly (M := A ⊗[R] M)
      ((tensorProduct R A M M ∘ₗ baseChange A φ : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M)
        ((LinearEquiv.symm (Basis.repr (basis A b)) : (a : ι →₀ A) → A ⊗[R] L)
          ((Equiv.symm Finsupp.equivFunOnFinite : (a : ι → A) → ι →₀ A) x))))

Tactic:
rw [← polyCharpolyAux_map_eval (tensorProduct R A M M ∘ₗ baseChange A φ) _ (basis A bₘ),
    polyCharpolyAux_baseChange, Polynomial.map_map]

Premises used: LinearMap.baseChange, LinearMap.polyCharpolyAux_map_eval, LinearMap.polyCharpolyAux_baseChange, LinearMap.comp, Algebra.TensorProduct.basis, Polynomial.map_map, LinearMap.tensorProduct
-- 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
inst_11 : Module.Finite A (A ⊗[R] M)
inst_12 : Free A (A ⊗[R] M)
x : ι → A
e_f :
  Eq (α := MvPolynomial ι R →+* A) (AlgHom.toRingHom (aeval x))
    (RingHom.comp (eval x) (MvPolynomial.map (algebraMap R A)))
⊢ Eq (α := Polynomial A) (Polynomial.map (AlgHom.toRingHom (aeval x)) (φ.polyCharpolyAux b bₘ))
    (Polynomial.map (RingHom.comp (eval x) (MvPolynomial.map (algebraMap R A))) (φ.polyCharpolyAux b bₘ))

Tactic:
congr
-- 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
inst_11 : Module.Finite A (A ⊗[R] M)
inst_12 : Free A (A ⊗[R] M)
x : ι → A
⊢ Eq (α := MvPolynomial ι R →+* A) (AlgHom.toRingHom (aeval x))
    (RingHom.comp (eval x) (MvPolynomial.map (algebraMap R A)))

Tactic:
DFunLike.ext _ _ fun f ↦ (MvPolynomial.eval_map (algebraMap R A) x f).symm

Premises used: MvPolynomial.eval_map, Algebra.algebraMap, DFunLike.ext, Eq.symm
-- 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
inst_11 : Module.Finite A (A ⊗[R] M)
inst_12 : Free A (A ⊗[R] M)
x : ι → A
⊢ Eq (α := MvPolynomial ι R →+* A) (AlgHom.toRingHom (aeval x))
    (RingHom.comp (eval x) (MvPolynomial.map (algebraMap R A)))

Tactic:
exact DFunLike.ext _ _ fun f ↦ (MvPolynomial.eval_map (algebraMap R A) x f).symm

Premises used: DFunLike.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
ιM' : Type u_8
inst_9 : Fintype ιM'
inst_10 : DecidableEq ιM'
bₘ' : Basis ιM' R M
f : Polynomial (MvPolynomial ι R) → Polynomial (MvPolynomial ι R) := Polynomial.map (AlgHom.toRingHom (aeval X))
simp : Function.Injective (α := Polynomial (MvPolynomial ι R)) (Polynomial.map (RingHom.id (MvPolynomial ι R)))
⊢ Function.Injective f

Tactic:
simp only [f, aeval_X_left, AlgHom.toRingHom_eq_coe, AlgHom.id_toRingHom]

Premises used: MvPolynomial.aeval_X_left, AlgHom.toRingHom_eq_coe, AlgHom.id_toRingHom