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
ι' : Type u_6
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 ι'
inst_7 : DecidableEq ι
inst_8 : DecidableEq ι'
inst_9 : Free R M
inst_10 : Module.Finite R M
b : Basis ι R L
b' : Basis ι' R L
k : ℕ
B : Basis.{u_3, u_1, u_3} (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R (End R M) :=
  Basis.end (Free.chooseBasis R M)
H :
  Eq (α := MvPolynomial ι R)
    (((↑(bind₁ (toMvPolynomial b B φ)) :
            MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R →+* MvPolynomial ι R) :
          (a : MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R) → MvPolynomial ι R)
        (Polynomial.coeff (charpoly.univ R (Free.ChooseBasisIndex R M)) k) :
      MvPolynomial ι R)
    (0 : MvPolynomial ι R)
g : (i : ι) → MvPolynomial ι' R := toMvPolynomial b' b id
⊢ Eq (α := MvPolynomial ι' R)
    ((bind₁ g : (a : MvPolynomial ι R) → MvPolynomial ι' R)
        (((↑(bind₁ (toMvPolynomial b B φ)) :
              MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R →+* MvPolynomial ι R) :
            (a : MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R) → MvPolynomial ι R)
          (Polynomial.coeff (charpoly.univ R (Free.ChooseBasisIndex R M)) k)) :
      MvPolynomial ι' R)
    ((bind₁ g : (a : MvPolynomial ι R) → MvPolynomial ι' R) 0 : MvPolynomial ι' R)

Tactic:
apply_fun (MvPolynomial.bind₁ g) at H

Premises used: MvPolynomial.bind₁
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
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 ι'
inst_7 : DecidableEq ι
inst_8 : DecidableEq ι'
inst_9 : Free R M
inst_10 : Module.Finite R M
b : Basis ι R L
b' : Basis ι' R L
k : ℕ
B : Basis.{u_3, u_1, u_3} (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R (End R M) :=
  Basis.end (Free.chooseBasis R M)
g : (i : ι) → MvPolynomial ι' R := toMvPolynomial b' b id
H :
  Eq (α := MvPolynomial ι' R)
    ((bind₁ g : (a : MvPolynomial ι R) → MvPolynomial ι' R)
        (((↑(bind₁ (toMvPolynomial b B φ)) :
              MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R →+* MvPolynomial ι R) :
            (a : MvPolynomial (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) R) → MvPolynomial ι R)
          (Polynomial.coeff (charpoly.univ R (Free.ChooseBasisIndex R M)) k)) :
      MvPolynomial ι' R)
    ((bind₁ g : (a : MvPolynomial ι R) → MvPolynomial ι' R) 0 : MvPolynomial ι' R)
⊢ toMvPolynomial b' B φ = fun (i : Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) ↦
    (bind₁ g : (a : MvPolynomial ι R) → MvPolynomial ι' R) (toMvPolynomial b B φ i)

Tactic:
have : toMvPolynomial b' B φ = fun i ↦ (MvPolynomial.bind₁ g) (toMvPolynomial b B φ i) :=
    funext <| toMvPolynomial_comp b' b B φ LinearMap.id
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
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 ι'
inst_7 : DecidableEq ι
inst_8 : DecidableEq ι'
inst_9 : Free R M
inst_10 : Module.Finite R M
b : Basis ι R L
b' : Basis ι' R L
k : ℕ
mp : (φ.polyCharpoly b).coeff k = 0 → (φ.polyCharpoly b').coeff k = 0
mpr : (φ.polyCharpoly b').coeff k = 0 → (φ.polyCharpoly b).coeff k = 0
⊢ (φ.polyCharpoly b).coeff k = 0 ↔ (φ.polyCharpoly b').coeff k = 0

Tactic:
constructor
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
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 ι'
inst_7 : DecidableEq ι
inst_8 : DecidableEq ι'
inst_9 : Free R M
inst_10 : Module.Finite R M
b : Basis ι R L
b' : Basis ι' R L
k : ℕ
⊢ (φ.polyCharpoly b).coeff k = 0 → (φ.polyCharpoly b').coeff k = 0

Tactic:
apply polyCharpoly_coeff_eq_zero_of_basis

Premises used: LinearMap.polyCharpoly_coeff_eq_zero_of_basis
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
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 ι'
inst_7 : DecidableEq ι
inst_8 : DecidableEq ι'
inst_9 : Free R M
inst_10 : Module.Finite R M
b : Basis ι R L
b' : Basis ι' R L
k : ℕ
⊢ (φ.polyCharpoly b').coeff k = 0 → (φ.polyCharpoly b).coeff k = 0

Tactic:
apply polyCharpoly_coeff_eq_zero_of_basis

Premises used: LinearMap.polyCharpoly_coeff_eq_zero_of_basis
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
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 : DecidableEq ι
inst_7 : Free R M
inst_8 : Module.Finite R M
b : Basis ι R L
inst_9 : Nontrivial R
apply : φ.polyCharpoly b ≠ 0
⊢ (φ.polyCharpoly b).coeff (φ.nilRankAux b) ≠ 0

Tactic:
apply Polynomial.trailingCoeff_nonzero_iff_nonzero.mpr

Premises used: Iff.mpr, Polynomial.trailingCoeff_nonzero_iff_nonzero
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
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 : DecidableEq ι
inst_7 : Free R M
inst_8 : Module.Finite R M
b : Basis ι R L
inst_9 : Nontrivial R
⊢ φ.polyCharpoly b ≠ 0

Tactic:
apply polyCharpoly_ne_zero

Premises used: LinearMap.polyCharpoly_ne_zero
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
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 ι'
inst_7 : DecidableEq ι
inst_8 : DecidableEq ι'
inst_9 : Free R M
inst_10 : Module.Finite R M
inst_11 : Nontrivial R
b : Basis ι R L
b' : Basis ι' R L
h : (φ.polyCharpoly b).coeff (φ.nilRankAux b') ≠ 0
⊢ φ.nilRankAux b ≤ φ.nilRankAux b'

Tactic:
apply Polynomial.natTrailingDegree_le_of_ne_zero

Premises used: Polynomial.natTrailingDegree_le_of_ne_zero
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
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 ι'
inst_7 : DecidableEq ι
inst_8 : DecidableEq ι'
inst_9 : Free R M
inst_10 : Module.Finite R M
inst_11 : Nontrivial R
b : Basis ι R L
b' : Basis ι' R L
h : ¬(φ.polyCharpoly b').coeff (φ.nilRankAux b') = 0
⊢ (φ.polyCharpoly b).coeff (φ.nilRankAux b') ≠ 0

Tactic:
rw [Ne, (polyCharpoly_coeff_eq_zero_iff_of_basis φ b b' _).not]

Premises used: Iff.not, Ne, LinearMap.polyCharpoly_coeff_eq_zero_iff_of_basis
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
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 ι'
inst_7 : DecidableEq ι
inst_8 : DecidableEq ι'
inst_9 : Free R M
inst_10 : Module.Finite R M
inst_11 : Nontrivial R
b : Basis ι R L
b' : Basis ι' R L
⊢ ¬(φ.polyCharpoly b').coeff (φ.nilRankAux b') = 0

Tactic:
apply polyCharpoly_coeff_nilRankAux_ne_zero

Premises used: LinearMap.polyCharpoly_coeff_nilRankAux_ne_zero
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
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 ι'
inst_7 : DecidableEq ι
inst_8 : DecidableEq ι'
inst_9 : Free R M
inst_10 : Module.Finite R M
inst_11 : Nontrivial R
b : Basis ι R L
b' : Basis ι' R L
a : φ.nilRankAux b ≤ (φ.polyCharpoly b').natTrailingDegree
a₁ : (φ.polyCharpoly b').natTrailingDegree ≤ φ.nilRankAux b
⊢ φ.nilRankAux b = (φ.polyCharpoly b').natTrailingDegree

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
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 ι'
inst_7 : DecidableEq ι
inst_8 : DecidableEq ι'
inst_9 : Free R M
inst_10 : Module.Finite R M
inst_11 : Nontrivial R
b : Basis ι R L
b' : Basis ι' R L
⊢ φ.nilRankAux b ≤ (φ.polyCharpoly b').natTrailingDegree

Tactic:
apply nilRankAux_le

Premises used: LinearMap.nilRankAux_le
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
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 ι'
inst_7 : DecidableEq ι
inst_8 : DecidableEq ι'
inst_9 : Free R M
inst_10 : Module.Finite R M
inst_11 : Nontrivial R
b : Basis ι R L
b' : Basis ι' R L
⊢ (φ.polyCharpoly b').natTrailingDegree ≤ φ.nilRankAux b

Tactic:
apply nilRankAux_le

Premises used: LinearMap.nilRankAux_le
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
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 : DecidableEq ι
inst_7 : Free R M
inst_8 : Module.Finite R M
inst_9 : Module.Finite R L
inst_10 : Free R L
inst_11 : Nontrivial R
b : Basis ι R L
⊢ φ.nilRank = (φ.polyCharpoly b).natTrailingDegree

Tactic:
apply nilRankAux_basis_indep

Premises used: LinearMap.nilRankAux_basis_indep
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
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 : DecidableEq ι
inst_7 : Free R M
inst_8 : Module.Finite R M
b : Basis ι R L
inst_9 : Module.Finite R L
inst_10 : Free R L
inst_11 : Nontrivial R
rw : (φ.polyCharpoly b).coeff (φ.polyCharpoly b).natTrailingDegree ≠ 0
⊢ (φ.polyCharpoly b).coeff φ.nilRank ≠ 0

Tactic:
rw [nilRank_eq_polyCharpoly_natTrailingDegree _ b]

Premises used: LinearMap.nilRank_eq_polyCharpoly_natTrailingDegree
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
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 : DecidableEq ι
inst_7 : Free R M
inst_8 : Module.Finite R M
b : Basis ι R L
inst_9 : Module.Finite R L
inst_10 : Free R L
inst_11 : Nontrivial R
⊢ (φ.polyCharpoly b).coeff (φ.polyCharpoly b).natTrailingDegree ≠ 0

Tactic:
apply polyCharpoly_coeff_nilRankAux_ne_zero

Premises used: LinearMap.polyCharpoly_coeff_nilRankAux_ne_zero
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
inst_9 : Nontrivial R
ι : Type u_8
inst_10 : Fintype ι
b : Basis ι R M
h :
  Ne (α := MvPolynomial.{u_2, u_1} (ChooseBasisIndex R L) R)
    (Polynomial.coeff (φ.polyCharpoly (chooseBasis R L)) (Fintype.card ι)) 0
⊢ φ.nilRank ≤ Fintype.card ι

Tactic:
apply Polynomial.natTrailingDegree_le_of_ne_zero

Premises used: Polynomial.natTrailingDegree_le_of_ne_zero
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
inst_9 : Nontrivial R
ι : Type u_8
inst_10 : Fintype ι
b : Basis ι R M
h : Ne (α := MvPolynomial.{u_2, u_1} (ChooseBasisIndex R L) R) 1 0
⊢ Ne (α := MvPolynomial.{u_2, u_1} (ChooseBasisIndex R L) R)
    (Polynomial.coeff (φ.polyCharpoly (chooseBasis R L)) (Fintype.card ι)) 0

Tactic:
rw [← Module.finrank_eq_card_basis b, ← polyCharpoly_natDegree φ (chooseBasis R L),
    Polynomial.coeff_natDegree, (polyCharpoly_monic _ _).leadingCoeff]

Premises used: Polynomial.coeff_natDegree, Module.finrank_eq_card_basis, LinearMap.polyCharpoly_monic, Polynomial.Monic.leadingCoeff, LinearMap.polyCharpoly_natDegree, Module.Free.chooseBasis
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
inst_9 : Nontrivial R
ι : Type u_8
inst_10 : Fintype ι
b : Basis ι R M
⊢ Ne (α := MvPolynomial.{u_2, u_1} (ChooseBasisIndex R L) R) 1 0

Tactic:
apply one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
inst_9 : Nontrivial R
⊢ φ.nilRank ≤ finrank R M

Tactic:
simpa only [finrank_eq_card_chooseBasisIndex R M] using nilRank_le_card φ (chooseBasis R M)

Premises used: Module.finrank_eq_card_chooseBasisIndex, LinearMap.nilRank_le_card, Module.Free.chooseBasis
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
inst_9 : Nontrivial R
x : L
h :
  Ne (α := MvPolynomial.{u_2, u_1} (ChooseBasisIndex R L) R)
    (Polynomial.coeff (φ.polyCharpoly (chooseBasis R L))
      (Polynomial.natTrailingDegree.{u_1} (R := R) (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x))))
    0
⊢ φ.nilRank ≤ Polynomial.natTrailingDegree.{u_1} (R := R) (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x))

Tactic:
apply Polynomial.natTrailingDegree_le_of_ne_zero

Premises used: Polynomial.natTrailingDegree_le_of_ne_zero
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
inst_9 : Nontrivial R
x : L
h :
  Eq (α := MvPolynomial.{u_2, u_1} (ChooseBasisIndex R L) R)
    (Polynomial.coeff (φ.polyCharpoly (chooseBasis R L))
      (Polynomial.natTrailingDegree.{u_1} (R := R) (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x))))
    0
⊢ Eq.{u_1 + 1} (α := R)
    ((eval
            (⇑((Basis.repr (chooseBasis R L) : (a : L) → ChooseBasisIndex R L →₀ R) x :
                  Finsupp.{u_2, u_1} (ChooseBasisIndex R L) R) :
              (a : ChooseBasisIndex R L) → R) :
          (a : MvPolynomial (ChooseBasisIndex R L) R) → R)
        (Polynomial.coeff (φ.polyCharpoly (chooseBasis R L))
          (Polynomial.natTrailingDegree.{u_1} (R := R) (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)))) :
      R)
    ((eval
            (⇑((Basis.repr (chooseBasis R L) : (a : L) → ChooseBasisIndex R L →₀ R) x :
                  Finsupp.{u_2, u_1} (ChooseBasisIndex R L) R) :
              (a : ChooseBasisIndex R L) → R) :
          (a : MvPolynomial (ChooseBasisIndex R L) R) → R)
        0 :
      R)

Tactic:
apply_fun (MvPolynomial.eval ((chooseBasis R L).repr x)) at h

Premises used: Module.Basis.repr, MvPolynomial.eval, DFunLike.coe, Module.Free.chooseBasis
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
inst_9 : Nontrivial R
x : L
h :
  Eq.{u_1 + 1} (α := R)
    ((eval
            (⇑((Basis.repr (chooseBasis R L) : (a : L) → ChooseBasisIndex R L →₀ R) x :
                  Finsupp.{u_2, u_1} (ChooseBasisIndex R L) R) :
              (a : ChooseBasisIndex R L) → R) :
          (a : MvPolynomial (ChooseBasisIndex R L) R) → R)
        (Polynomial.coeff (φ.polyCharpoly (chooseBasis R L))
          (Polynomial.natTrailingDegree.{u_1} (R := R) (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)))) :
      R)
    ((eval
            (⇑((Basis.repr (chooseBasis R L) : (a : L) → ChooseBasisIndex R L →₀ R) x :
                  Finsupp.{u_2, u_1} (ChooseBasisIndex R L) R) :
              (a : ChooseBasisIndex R L) → R) :
          (a : MvPolynomial (ChooseBasisIndex R L) R) → R)
        0 :
      R)
⊢ Eq.{u_1 + 1} (α := R)
    (Polynomial.coeff (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x))
      (Polynomial.natTrailingDegree.{u_1} (R := R) (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x))))
    0

Tactic:
rw [polyCharpoly_coeff_eval, map_zero] at h

Premises used: map_zero, LinearMap.polyCharpoly_coeff_eval
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
inst_9 : Nontrivial R
x : L
h :
  Eq.{u_1 + 1} (α := R)
    (Polynomial.coeff (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x))
      (Polynomial.natTrailingDegree.{u_1} (R := R) (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x))))
    0
apply : Ne.{u_1 + 1} (α := Polynomial R) (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) 0
⊢ False

Tactic:
apply Polynomial.trailingCoeff_nonzero_iff_nonzero.mpr _ h

Premises used: Iff.mpr, Polynomial.trailingCoeff_nonzero_iff_nonzero
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
inst_9 : Nontrivial R
x : L
h :
  Eq.{u_1 + 1} (α := R)
    (Polynomial.coeff (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x))
      (Polynomial.natTrailingDegree.{u_1} (R := R) (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x))))
    0
⊢ Ne.{u_1 + 1} (α := Polynomial R) (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) 0

Tactic:
apply (LinearMap.charpoly_monic _).ne_zero

Premises used: LinearMap.charpoly_monic, Polynomial.Monic.ne_zero
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
x : L
⊢ φ.IsNilRegular x ↔
    Ne.{u_1 + 1} (α := R) (Polynomial.coeff (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) φ.nilRank) 0

Tactic:
Iff.rfl

Premises used: Iff.rfl, LinearMap.IsNilRegular
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
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 : DecidableEq ι
inst_7 : Free R M
inst_8 : Module.Finite R M
b : Basis ι R L
inst_9 : Module.Finite R L
inst_10 : Free R L
x : L
rw :
  Ne.{u_1 + 1} (α := R) (Polynomial.coeff (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) φ.nilRank) 0 ↔
    Ne.{u_1 + 1} (α := R)
      ((eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) : (a : MvPolynomial ι R) → R)
          ((φ.polyCharpoly b).coeff φ.nilRank) :
        R)
      (0 : R)
rw₁ rw₂ :
  Ne.{u_1 + 1} (α := R) (Polynomial.coeff (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) φ.nilRank) 0 ↔
    Ne.{u_1 + 1} (α := R) (Polynomial.coeff (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) φ.nilRank) 0
⊢ φ.IsNilRegular x ↔
    Ne.{u_1 + 1} (α := R)
      ((eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) : (a : MvPolynomial ι R) → R)
          ((φ.polyCharpoly b).coeff φ.nilRank) :
        R)
      (0 : R)

Tactic:
rw [IsNilRegular, polyCharpoly_coeff_eval]

Premises used: LinearMap.IsNilRegular, LinearMap.polyCharpoly_coeff_eval
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
x : L
inst_9 : Nontrivial R
rw :
  Ne.{u_1 + 1} (α := R) (Polynomial.coeff (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) φ.nilRank) 0 ↔
    Polynomial.natTrailingDegree.{u_1} (R := R) (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) = φ.nilRank
⊢ φ.IsNilRegular x ↔
    Polynomial.natTrailingDegree.{u_1} (R := R) (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) = φ.nilRank

Tactic:
rw [isNilRegular_def]

Premises used: LinearMap.isNilRegular_def