awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (hypothesis)
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)
⊢ 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)
have this : 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
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
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)
this :
  toMvPolynomial b' B φ = fun (i : Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) ↦
    (bind₁ g : (a : MvPolynomial ι R) → MvPolynomial ι' R) (toMvPolynomial b B φ i)
⊢ 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)
have rwa : ∀
  (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)
      (0 : MvPolynomial ι' R))
  (this :
    toMvPolynomial b' B φ = fun (i : Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) ↦
      (bind₁ g : (a : MvPolynomial ι R) → MvPolynomial ι' R) (toMvPolynomial b B φ i)),
  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)
Tactic: rwa [map_zero, RingHom.coe_coe, MvPolynomial.bind₁_bind₁, ← this] at H
Cleared hypotheses: H, this
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
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
have mp : (φ.polyCharpoly b).coeff k = 0 → (φ.polyCharpoly b').coeff k = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
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
⊢ (φ.polyCharpoly b).coeff k = 0 ↔ (φ.polyCharpoly b').coeff k = 0
have mpr : (φ.polyCharpoly b').coeff k = 0 → (φ.polyCharpoly b).coeff k = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
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).coeff (φ.nilRankAux b) ≠ 0
have apply : φ.polyCharpoly b ≠ 0
Tactic: apply Polynomial.trailingCoeff_nonzero_iff_nonzero.mpr
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
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 ≤ φ.nilRankAux b'
have h : (φ.polyCharpoly b).coeff (φ.nilRankAux b') ≠ 0
Tactic: apply Polynomial.natTrailingDegree_le_of_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
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
have h : ¬(φ.polyCharpoly b').coeff (φ.nilRankAux b') = 0
Tactic: rw [Ne, (polyCharpoly_coeff_eq_zero_iff_of_basis φ b b' _).not]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
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
have a : φ.nilRankAux b ≤ (φ.polyCharpoly b').natTrailingDegree
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
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
⊢ φ.nilRankAux b = (φ.polyCharpoly b').natTrailingDegree
have a₁ : (φ.polyCharpoly b').natTrailingDegree ≤ φ.nilRankAux b
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
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 φ.nilRank ≠ 0
have rw : (φ.polyCharpoly b).coeff (φ.polyCharpoly b).natTrailingDegree ≠ 0
Tactic: rw [nilRank_eq_polyCharpoly_natTrailingDegree _ b]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
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
⊢ φ.nilRank ≤ Fintype.card ι
have h : Ne (α := MvPolynomial.{u_2, u_1} (ChooseBasisIndex R L) R)
  (Polynomial.coeff (φ.polyCharpoly (chooseBasis R L)) (Fintype.card ι)) 0
Tactic: apply Polynomial.natTrailingDegree_le_of_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
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)
    (Polynomial.coeff (φ.polyCharpoly (chooseBasis R L)) (Fintype.card ι)) 0
have h : Ne (α := MvPolynomial.{u_2, u_1} (ChooseBasisIndex R L) R) 1 0
Tactic: rw [← Module.finrank_eq_card_basis b, ← polyCharpoly_natDegree φ (chooseBasis R L),
    Polynomial.coeff_natDegree, (polyCharpoly_monic _ _).leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
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
⊢ φ.nilRank ≤ Polynomial.natTrailingDegree.{u_1} (R := R) (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x))
have 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
Tactic: apply Polynomial.natTrailingDegree_le_of_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (hypothesis)
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
⊢ False
have 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)
Tactic: apply_fun (MvPolynomial.eval ((chooseBasis R L).repr x)) at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (hypothesis)
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)
⊢ False
have 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
Tactic: rw [polyCharpoly_coeff_eval, map_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
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
⊢ False
have apply : Ne.{u_1 + 1} (α := Polynomial R) (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) 0
Tactic: apply Polynomial.trailingCoeff_nonzero_iff_nonzero.mpr _ h
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
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
⊢ φ.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)
have 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)
Tactic: rw [IsNilRegular, polyCharpoly_coeff_eval]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
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)
⊢ φ.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)
have 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
Tactic: rw [IsNilRegular, polyCharpoly_coeff_eval]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
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
⊢ φ.IsNilRegular x ↔
    Polynomial.natTrailingDegree.{u_1} (R := R) (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) = φ.nilRank
have 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
Tactic: rw [isNilRegular_def]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
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
⊢ 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
have mp : 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
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
mp :
  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
⊢ 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
have mpr : Polynomial.natTrailingDegree.{u_1} (R := R) (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) = φ.nilRank →
  Ne.{u_1 + 1} (α := R) (Polynomial.coeff (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) φ.nilRank) 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
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
h : Polynomial.natTrailingDegree.{u_1} (R := R) (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) = φ.nilRank
⊢ Ne.{u_1 + 1} (α := R) (Polynomial.coeff (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) φ.nilRank) 0
have mpr : Ne.{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 [← h]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
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
h : Polynomial.natTrailingDegree.{u_1} (R := R) (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) = φ.nilRank
⊢ Ne.{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
have mpr : Ne.{u_1 + 1} (α := Polynomial R) (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) 0
Tactic: apply Polynomial.trailingCoeff_nonzero_iff_nonzero.mpr