awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Charpoly.BaseChange
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
A : Type u_3
inst_5 : CommRing A
inst_6 : Algebra R A
f : M ≃ₗ[R] M
⊢ Eq.{u_3 + 1} (α := A)
    (↑(((LinearEquiv.det (R := A) (M := TensorProduct R A M) : (TensorProduct R A M ≃ₗ[A] TensorProduct R A M) →* Aˣ) :
            (a : TensorProduct R A M ≃ₗ[A] TensorProduct R A M) → Aˣ)
          (baseChange R A M M f)) :
      A)
    (↑(((Units.map (↑(algebraMap R A) : R →* A) : MonoidHom.{u_1, u_3} Rˣ Aˣ) : (a : Rˣ) → Aˣ)
          ((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f)) :
      A)

Tactic:
simp [LinearMap.det_baseChange]

Premises used: LinearMap.det_baseChange
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
⊢ f.charpoly =
    Matrix.charpoly.{u, v} (n := ChooseBasisIndex R M)
      ((toMatrix (chooseBasis R M) (chooseBasis R M) :
          (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
        f)

Tactic:
rfl

Premises used: LinearMap.charpoly, rfl
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
inst_5 : StrongRankCondition R
⊢ charpoly.{u, v} (M := M) 0 = HPow.hPow (α := R[X]) X (Module.finrank R M)

Tactic:
simp [charpoly, Module.finrank_eq_card_chooseBasisIndex]

Premises used: Module.finrank_eq_card_chooseBasisIndex, LinearMap.charpoly
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
inst_5 : StrongRankCondition R
⊢ charpoly.{u, v} (M := M) 1 = HSub.hSub (α := R[X]) X 1 ^ Module.finrank R M

Tactic:
simp [charpoly, Module.finrank_eq_card_chooseBasisIndex, Matrix.charpoly_one]

Premises used: Matrix.charpoly_one, Module.finrank_eq_card_chooseBasisIndex, LinearMap.charpoly
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : Module.End R M
μ : R
⊢ charpoly (f - HSMul.hSMul (β := Module.End R M) μ 1) =
    (charpoly f).comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) μ : R[X]))

Tactic:
simpa [LinearMap.charpoly, smul_eq_mul_diagonal] using Matrix.charpoly_sub_scalar ..

Premises used: Matrix.charpoly_sub_scalar, Matrix.smul_eq_mul_diagonal, LinearMap.charpoly
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
⊢ f.charpoly.Monic

Tactic:
Matrix.charpoly_monic _

Premises used: Matrix.charpoly_monic, LinearMap.charpoly
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : StrongRankCondition R
⊢ ∀ (R : Type u) [inst : Semiring R] [InvariantBasisNumber R], Nontrivial R

Tactic:
haveI := nontrivial_of_invariantBasisNumber
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : StrongRankCondition R
this : ∀ (R : Type u) [inst : Semiring R] [InvariantBasisNumber R], Nontrivial R
rw :
  natDegree.{u} (R := R)
      (Matrix.charpoly.{u, v} (n := ChooseBasisIndex R M)
        ((toMatrix (chooseBasis R M) (chooseBasis R M) :
            (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
          f)) =
    finrank R M
rw₁ : Fintype.card.{v} (ChooseBasisIndex R M) = finrank R M
rw₂ rw₃ : Fintype.card.{v} (ChooseBasisIndex R M) = Fintype.card.{v} (ChooseBasisIndex R M)
⊢ f.charpoly.natDegree = finrank R M

Tactic:
rw [charpoly, Matrix.charpoly_natDegree_eq_dim, finrank_eq_card_chooseBasisIndex]

Premises used: Module.finrank_eq_card_chooseBasisIndex, Matrix.charpoly_natDegree_eq_dim, LinearMap.charpoly
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
apply :
  Eq (α := Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
    (((↑(algEquivMatrix (chooseBasis R M)) :
            Module.End R M ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) :
          (a : Module.End R M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
        ((aeval f : (a : R[X]) → M →ₗ[R] M) f.charpoly) :
      Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
    (0 : Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
⊢ Eq.{v + 1} (α := M →ₗ[R] M) ((aeval f : (a : R[X]) → M →ₗ[R] M) f.charpoly : M →ₗ[R] M) (0 : M →ₗ[R] M)

Tactic:
apply (LinearEquiv.map_eq_zero_iff (algEquivMatrix (chooseBasis R M)).toLinearEquiv).1

Premises used: LinearEquiv.map_eq_zero_iff, AlgEquiv.toLinearEquiv, Iff.mp, algEquivMatrix, Module.Free.chooseBasis
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
rw :
  Eq (α := Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
    (((aeval
              (((↑(algEquivMatrix (chooseBasis R M)) :
                    Module.End R M →ₐ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) :
                  (a : Module.End R M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
                f) :
            R[X] →ₐ[R] Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) :
          (a : R[X]) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
        (Matrix.charpoly.{u, v} (n := ChooseBasisIndex R M)
          ((toMatrix (chooseBasis R M) (chooseBasis R M) :
              (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
            f)) :
      Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
    (0 : Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
⊢ Eq (α := Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
    (((↑(algEquivMatrix (chooseBasis R M)) :
            Module.End R M ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) :
          (a : Module.End R M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
        ((aeval f : (a : R[X]) → M →ₗ[R] M) f.charpoly) :
      Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
    (0 : Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)

Tactic:
rw [AlgEquiv.toLinearEquiv_apply, ← AlgEquiv.coe_algHom, ← Polynomial.aeval_algHom_apply _ _ _,
    charpoly_def]

Premises used: LinearMap.charpoly_def, AlgEquiv.coe_algHom, Polynomial.aeval_algHom_apply, AlgEquiv.toLinearEquiv_apply
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
⊢ Eq (α := Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
    (((aeval
              (((↑(algEquivMatrix (chooseBasis R M)) :
                    Module.End R M →ₐ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) :
                  (a : Module.End R M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
                f) :
            R[X] →ₐ[R] Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) :
          (a : R[X]) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
        (Matrix.charpoly.{u, v} (n := ChooseBasisIndex R M)
          ((toMatrix (chooseBasis R M) (chooseBasis R M) :
              (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
            f)) :
      Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
    (0 : Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)

Tactic:
Matrix.aeval_self_charpoly _

Premises used: Matrix.aeval_self_charpoly
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
⊢ Eq (α := Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
    (((aeval
              (((↑(algEquivMatrix (chooseBasis R M)) :
                    Module.End R M →ₐ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) :
                  (a : Module.End R M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
                f) :
            R[X] →ₐ[R] Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) :
          (a : R[X]) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
        (Matrix.charpoly.{u, v} (n := ChooseBasisIndex R M)
          ((toMatrix (chooseBasis R M) (chooseBasis R M) :
              (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
            f)) :
      Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
    (0 : Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)

Tactic:
exact Matrix.aeval_self_charpoly _

Premises used: Matrix.aeval_self_charpoly
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
⊢ IsIntegral R f

Tactic:
⟨f.charpoly, ⟨charpoly_monic f, aeval_self_charpoly f⟩⟩

Premises used: LinearMap.charpoly_monic, RingHom.IsIntegralElem, LinearMap.aeval_self_charpoly, IsIntegral, And.intro, Exists.intro, LinearMap.charpoly
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
K : Type u
M : Type v
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : M →ₗ[K] M
⊢ minpoly K f ∣ f.charpoly

Tactic:
minpoly.dvd _ _ (aeval_self_charpoly f)

Premises used: LinearMap.aeval_self_charpoly, minpoly.dvd
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
p : R[X]
⊢ Eq.{v + 1} (α := M →ₗ[R] M) ((aeval f : (a : R[X]) → M →ₗ[R] M) p : M →ₗ[R] M)
    ((aeval f : (a : R[X]) → M →ₗ[R] M) (p %ₘ f.charpoly) : M →ₗ[R] M)

Tactic:
(aeval_modByMonic_eq_self_of_root f.aeval_self_charpoly).symm

Premises used: Polynomial.aeval_modByMonic_eq_self_of_root, LinearMap.aeval_self_charpoly, Eq.symm
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
k : ℕ
rw : f ^ k = (aeval f : (a : R[X]) → M →ₗ[R] M) (HPow.hPow (α := R[X]) X k)
rw₁ : f ^ k = HPow.hPow (α := M →ₗ[R] M) ((aeval f : (a : R[X]) → M →ₗ[R] M) X : M →ₗ[R] M) k
rw₂ rw₃ : f ^ k = f ^ k
⊢ f ^ k = (aeval f : (a : R[X]) → M →ₗ[R] M) (HPow.hPow (α := R[X]) X k %ₘ f.charpoly)

Tactic:
rw [← aeval_eq_aeval_mod_charpoly, map_pow, aeval_X]

Premises used: map_pow, LinearMap.aeval_eq_aeval_mod_charpoly, Polynomial.aeval_X
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : Nontrivial R
hf : Function.Injective (α := M) (β := M) (⇑f : (a : M) → M)
h : coeff (minpoly R f) 0 = 0
obtain : ∀ (P : R[X]) (hP : minpoly R f = X * P), False
⊢ False

Tactic:
obtain ⟨P, hP⟩ := X_dvd_iff.2 h

Premises used: Iff.mpr, Polynomial.X_dvd_iff
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : Nontrivial R
hf : Function.Injective (α := M) (β := M) (⇑f : (a : M) → M)
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
rw : P.degree < (P * X).degree
⊢ P.degree < degree (minpoly R f)

Tactic:
rw [hP, mul_comm]

Premises used: mul_comm
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : Nontrivial R
hf : Function.Injective (α := M) (β := M) (⇑f : (a : M) → M)
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
⊢ P.degree < (P * X).degree

Tactic:
degree_lt_degree_mul_X fun h => ?_

Premises used: Polynomial.degree_lt_degree_mul_X
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : Nontrivial R
hf : Function.Injective (α := M) (β := M) (⇑f : (a : M) → M)
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
refine : ∀ (h : P = 0), False
⊢ P.degree < (P * X).degree

Tactic:
refine degree_lt_degree_mul_X fun h => ?_

Premises used: Polynomial.degree_lt_degree_mul_X
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : Nontrivial R
hf : Function.Injective (α := M) (β := M) (⇑f : (a : M) → M)
h_1 : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
h : P = 0
⊢ Eq (α := R[X]) (minpoly R f) 0

Tactic:
rw [h, mul_zero] at hP

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : Nontrivial R
hf : Function.Injective (α := M) (β := M) (⇑f : (a : M) → M)
h_1 : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
h : P = 0
hP₁ : Eq (α := R[X]) (minpoly R f) 0
⊢ P = 0

Tactic:
rw [h, mul_zero] at hP

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : Nontrivial R
hf : Function.Injective (α := M) (β := M) (⇑f : (a : M) → M)
h_1 : coeff (minpoly R f) 0 = 0
P : R[X]
hP : Eq (α := R[X]) (minpoly R f) 0
h : P = 0
⊢ False

Tactic:
minpoly.ne_zero (isIntegral f) hP

Premises used: LinearMap.isIntegral, minpoly.ne_zero
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : Nontrivial R
hf : Function.Injective (α := M) (β := M) (⇑f : (a : M) → M)
h_1 : coeff (minpoly R f) 0 = 0
P : R[X]
hP : Eq (α := R[X]) (minpoly R f) 0
h : P = 0
⊢ False

Tactic:
exact minpoly.ne_zero (isIntegral f) hP

Premises used: LinearMap.isIntegral, minpoly.ne_zero
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : Nontrivial R
hf : Function.Injective (α := M) (β := M) (⇑f : (a : M) → M)
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
⊢ P.degree < degree (minpoly R f)

Tactic:
have hdegP : P.degree < (minpoly R f).degree := by
    rw [hP, mul_comm]
    refine degree_lt_degree_mul_X fun h => ?_
    rw [h, mul_zero] at hP
    exact minpoly.ne_zero (isIntegral f) hP
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : Nontrivial R
hf : Function.Injective (α := M) (β := M) (⇑f : (a : M) → M)
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : P.degree < degree (minpoly R f)
this : Monic (minpoly R f)
rwa : ∀ (this : leadingCoeff (minpoly R f) = 1), P.Monic
rwa₁ : ∀ (this : (X * P).leadingCoeff = 1), P.Monic
rwa₂ : ∀ (this : (P * X).leadingCoeff = 1), P.Monic
rwa₃ : ∀ (this : P.leadingCoeff = 1), P.Monic
rwa₄ rwa₅ rwa₆ rwa₇ : ∀ (this : P.Monic), P.Monic
⊢ P.Monic

Tactic:
rwa [Monic.def, hP, mul_comm, leadingCoeff_mul_X, ← Monic.def] at this

Premises used: Polynomial.leadingCoeff_mul_X, mul_comm, Polynomial.Monic.def
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : Nontrivial R
hf : Function.Injective (α := M) (β := M) (⇑f : (a : M) → M)
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : P.degree < degree (minpoly R f)
suffices : Monic (minpoly R f)
⊢ P.Monic

Tactic:
suffices (minpoly R f).Monic by
      rwa [Monic.def, hP, mul_comm, leadingCoeff_mul_X, ← Monic.def] at this
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : Nontrivial R
hf : Function.Injective (α := M) (β := M) (⇑f : (a : M) → M)
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : P.degree < degree (minpoly R f)
⊢ Monic (minpoly R f)

Tactic:
minpoly.monic (isIntegral f)

Premises used: minpoly.monic, LinearMap.isIntegral
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : Nontrivial R
hf : Function.Injective (α := M) (β := M) (⇑f : (a : M) → M)
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : P.degree < degree (minpoly R f)
⊢ Monic (minpoly R f)

Tactic:
exact minpoly.monic (isIntegral f)

Premises used: minpoly.monic, LinearMap.isIntegral
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : Nontrivial R
hf : Function.Injective (α := M) (β := M) (⇑f : (a : M) → M)
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : P.degree < degree (minpoly R f)
⊢ P.Monic

Tactic:
have hPmonic : P.Monic := by
    suffices (minpoly R f).Monic by
      rwa [Monic.def, hP, mul_comm, leadingCoeff_mul_X, ← Monic.def] at this
    exact minpoly.monic (isIntegral f)
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : Nontrivial R
hf : Function.Injective (α := M) (β := M) (⇑f : (a : M) → M)
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : P.degree < degree (minpoly R f)
hPmonic : P.Monic
⊢ Eq.{v + 1} (α := M →ₗ[R] M) ((aeval f : (a : R[X]) → M →ₗ[R] M) (minpoly R f) : M →ₗ[R] M) (0 : M →ₗ[R] M)

Tactic:
have hzero : aeval f (minpoly R f) = 0 := minpoly.aeval _ _
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : Nontrivial R
hf : Function.Injective (α := M) (β := M) (⇑f : (a : M) → M)
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : P.degree < degree (minpoly R f)
hPmonic : P.Monic
hzero : Eq.{v + 1} (α := M →ₗ[R] M) ((aeval f : (a : R[X]) → M →ₗ[R] M) (minpoly R f) : M →ₗ[R] M) (0 : M →ₗ[R] M)
⊢ ∀ (x : M), Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) P : M →ₗ[R] M) : (a : M) → M) x : M) (0 : M)

Tactic:
simp only [hP, Module.End.mul_eq_comp, LinearMap.ext_iff, hf, aeval_X, map_eq_zero_iff, coe_comp,
    map_mul, zero_apply, Function.comp_apply] at hzero

Premises used: LinearMap.zero_apply, Module.End.mul_eq_comp, LinearMap.ext_iff, map_mul, LinearMap.coe_comp, map_eq_zero_iff, Function.comp_apply, Polynomial.aeval_X
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : Nontrivial R
hf : Function.Injective (α := M) (β := M) (⇑f : (a : M) → M)
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : P.degree < degree (minpoly R f)
hPmonic : P.Monic
hzero : ∀ (x : M), Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) P : M →ₗ[R] M) : (a : M) → M) x : M) (0 : M)
⊢ False

Tactic:
not_le.2 hdegP (minpoly.min _ _ hPmonic (LinearMap.ext hzero))

Premises used: not_le, Iff.mpr, LinearMap.ext, minpoly.min
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : Nontrivial R
hf : Function.Injective (α := M) (β := M) (⇑f : (a : M) → M)
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : P.degree < degree (minpoly R f)
hPmonic : P.Monic
hzero : ∀ (x : M), Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) P : M →ₗ[R] M) : (a : M) → M) x : M) (0 : M)
⊢ False

Tactic:
exact not_le.2 hdegP (minpoly.min _ _ hPmonic (LinearMap.ext hzero))

Premises used: not_le, Iff.mpr, LinearMap.ext, minpoly.min
-- Module: Mathlib.LinearAlgebra.Charpoly.Basic
Goal:
R : Type u_2
M : Type u_1
inst : CommRing R
inst_1 : Ring M
inst_2 : Algebra R M
inst_3 : Module.Finite R M
inst_4 : Module.Free R M
α : M
⊢ Eq (α := Module.End R M)
    ((lmul R M : (a : M) → Module.End R M)
        ((aeval α : (a : R[X]) → M) (LinearMap.charpoly.{u_2, u_1} (M := M) ((lmul R M : (a : M) → Module.End R M) α)) :
          M) :
      Module.End R M)
    ((lmul R M : (a : M) → Module.End R M) 0 : Module.End R M)

Tactic:
simpa [← aeval_algHom_apply] using LinearMap.aeval_self_charpoly <| Algebra.lmul _ _ α

Premises used: Algebra.lmul, LinearMap.aeval_self_charpoly, Polynomial.aeval_algHom_apply, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Charpoly.ToMatrix
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst_5 : DecidableEq ι
inst_6 : Fintype ι
b : Basis ι R M
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.LinearAlgebra.Charpoly.ToMatrix
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst_5 : DecidableEq ι
inst_6 : Fintype ι
b : Basis ι R M
h : Nontrivial R
set :
  let b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M;
  Eq.{u_1 + 1} (α := R[X]) (Matrix.charpoly.{u_1, w} (n := ι) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix ι ι R) f))
    (Matrix.charpoly.{u_1, u_2} (n := ChooseBasisIndex R M)
      ((toMatrix b' b' : (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f))
⊢ Eq.{u_1 + 1} (α := R[X]) (Matrix.charpoly.{u_1, w} (n := ι) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix ι ι R) f))
    (Matrix.charpoly.{u_1, u_2} (n := ChooseBasisIndex R M)
      ((toMatrix (chooseBasis R M) (chooseBasis R M) :
          (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
        f))

Tactic:
set b' := chooseBasis R M

Premises used: Module.Free.chooseBasis