awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Module.Free R A
inst_4 : Module.Finite R A
f : A
I : Ideal R
inst_5 : I.IsPrime
h : Subsingleton R
this : Subsingleton (A ⊗[R] I.ResidueField)
⊢ IsNilpotent (R := A ⊗[R] I.ResidueField)
      ((algebraMap A (A ⊗[R] I.ResidueField) : (a : A) → A ⊗[R] I.ResidueField) f : A ⊗[R] I.ResidueField) ↔
    ∀ i < Module.finrank R A,
      coeff (LinearMap.charpoly.{u_1, u_2} (M := A) ((Algebra.lmul R A : (a : A) → Module.End R A) f)) i ∈ I

Tactic:
simp [Subsingleton.elim I ⊤, Subsingleton.elim (f ⊗ₜ[R] (1 : I.ResidueField)) 0]

Premises used: TensorProduct.tmul, Subsingleton.elim, Top.top, OfNat.ofNat
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Module.Free R A
inst_4 : Module.Finite R A
f : A
I : Ideal R
inst_5 : I.IsPrime
h : Nontrivial R
rw : Module.finrank.{u_1, u_1} I.ResidueField I.ResidueField * Module.finrank R A = Module.finrank R A
rw₁ : 1 * Module.finrank R A = Module.finrank R A
rw₂ rw₃ : Module.finrank R A = Module.finrank R A
⊢ Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A

Tactic:
rw [Module.finrank_tensorProduct, Module.finrank_self, one_mul]

Premises used: Module.finrank_tensorProduct, Module.finrank_self, one_mul
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Module.Free R A
inst_4 : Module.Finite R A
f : A
I : Ideal R
inst_5 : I.IsPrime
h : Nontrivial R
⊢ Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A

Tactic:
have : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A := by
    rw [Module.finrank_tensorProduct, Module.finrank_self, one_mul]
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Module.Free R A
inst_4 : Module.Finite R A
f : A
I : Ideal R
inst_5 : I.IsPrime
h : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
inr :
  IsNilpotent (R := I.ResidueField ⊗[R] A)
      ((Algebra.TensorProduct.comm R A I.ResidueField : (a : A ⊗[R] I.ResidueField) → I.ResidueField ⊗[R] A)
          ((algebraMap A (A ⊗[R] I.ResidueField) : (a : A) → A ⊗[R] I.ResidueField) f) :
        I.ResidueField ⊗[R] A) ↔
    ∀ i < Module.finrank R A,
      coeff (LinearMap.charpoly.{u_1, u_2} (M := A) ((Algebra.lmul R A : (a : A) → Module.End R A) f)) i ∈ I
⊢ IsNilpotent (R := A ⊗[R] I.ResidueField)
      ((algebraMap A (A ⊗[R] I.ResidueField) : (a : A) → A ⊗[R] I.ResidueField) f : A ⊗[R] I.ResidueField) ↔
    ∀ i < Module.finrank R A,
      coeff (LinearMap.charpoly.{u_1, u_2} (M := A) ((Algebra.lmul R A : (a : A) → Module.End R A) f)) i ∈ I

Tactic:
rw [← IsNilpotent.map_iff (Algebra.TensorProduct.comm R A I.ResidueField).injective]

Premises used: Ideal.ResidueField, Algebra.TensorProduct.comm, IsNilpotent.map_iff, AlgEquiv.injective
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Module.Free R A
inst_4 : Module.Finite R A
f : A
I : Ideal R
inst_5 : I.IsPrime
h : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
inr :
  IsNilpotent (R := I.ResidueField ⊗[R] A) (1 ⊗ₜ[R] f) ↔
    ∀ i < Module.finrank R A,
      coeff (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)) i ∈ I
⊢ IsNilpotent (R := I.ResidueField ⊗[R] A)
      ((Algebra.TensorProduct.comm R A I.ResidueField : (a : A ⊗[R] I.ResidueField) → I.ResidueField ⊗[R] A)
          ((algebraMap A (A ⊗[R] I.ResidueField) : (a : A) → A ⊗[R] I.ResidueField) f) :
        I.ResidueField ⊗[R] A) ↔
    ∀ i < Module.finrank R A,
      coeff (LinearMap.charpoly.{u_1, u_2} (M := A) ((Algebra.lmul R A : (a : A) → Module.End R A) f)) i ∈ I

Tactic:
simp only [Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self, RingHom.id_apply,
    Algebra.coe_lmul_eq_mul, Algebra.TensorProduct.comm_tmul]

Premises used: Algebra.TensorProduct.algebraMap_apply, RingHom.id_apply, Algebra.algebraMap_self, Algebra.TensorProduct.comm_tmul, Algebra.coe_lmul_eq_mul
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Module.Free R A
inst_4 : Module.Finite R A
f : A
I : Ideal R
inst_5 : I.IsPrime
h : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
inr :
  Polynomial.map (algebraMap R I.ResidueField)
        (LinearMap.charpoly.{u_1, u_2} (M := A) ((Algebra.lmul R A : (a : A) → Module.End R A) f)) =
      HPow.hPow (α := I.ResidueField[X]) X (Module.finrank I.ResidueField (I.ResidueField ⊗[R] A)) ↔
    ∀ i < Module.finrank R A,
      coeff (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)) i ∈ I
⊢ IsNilpotent (R := I.ResidueField ⊗[R] A) (1 ⊗ₜ[R] f) ↔
    ∀ i < Module.finrank R A,
      coeff (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)) i ∈ I

Tactic:
rw [← IsNilpotent.map_iff (Algebra.lmul_injective (R := I.ResidueField)),
    LinearMap.isNilpotent_iff_charpoly, ← Algebra.baseChange_lmul, LinearMap.charpoly_baseChange]

Premises used: Algebra.lmul_injective, LinearMap.isNilpotent_iff_charpoly, IsNilpotent.map_iff, Algebra.baseChange_lmul, LinearMap.charpoly_baseChange
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Module.Free R A
inst_4 : Module.Finite R A
f : A
I : Ideal R
inst_5 : I.IsPrime
h : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
inr :
  Polynomial.map (algebraMap R I.ResidueField)
        (LinearMap.charpoly.{u_1, u_2} (M := A) ((Algebra.lmul R A : (a : A) → Module.End R A) f)) =
      HPow.hPow (α := I.ResidueField[X]) X
        (natDegree.{u_1} (R := R)
          (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f))) ↔
    ∀
      i <
        natDegree.{u_1} (R := R) (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)),
      coeff (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)) i ∈ I
⊢ Polynomial.map (algebraMap R I.ResidueField)
        (LinearMap.charpoly.{u_1, u_2} (M := A) ((Algebra.lmul R A : (a : A) → Module.End R A) f)) =
      HPow.hPow (α := I.ResidueField[X]) X (Module.finrank I.ResidueField (I.ResidueField ⊗[R] A)) ↔
    ∀ i < Module.finrank R A,
      coeff (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)) i ∈ I

Tactic:
simp_rw [this, ← ((LinearMap.mul R A) f).charpoly_natDegree]

Premises used: LinearMap.charpoly_natDegree, LinearMap.mul, DFunLike.coe
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Module.Free R A
inst_4 : Module.Finite R A
f : A
I : Ideal R
inst_5 : I.IsPrime
h : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
inr :
  Polynomial.map (algebraMap R I.ResidueField)
        (LinearMap.charpoly.{u_1, u_2} (M := A) ((Algebra.lmul R A : (a : A) → Module.End R A) f)) =
      HPow.hPow (α := I.ResidueField[X]) X
        (natDegree.{u_1} (R := R)
          (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f))) →
    ∀
      i <
        natDegree.{u_1} (R := R) (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)),
      coeff (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)) i ∈ I
inr₁ :
  (∀
      i <
        natDegree.{u_1} (R := R) (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)),
      coeff (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)) i ∈ I) →
    Polynomial.map (algebraMap R I.ResidueField)
        (LinearMap.charpoly.{u_1, u_2} (M := A) ((Algebra.lmul R A : (a : A) → Module.End R A) f)) =
      HPow.hPow (α := I.ResidueField[X]) X
        (natDegree.{u_1} (R := R)
          (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)))
⊢ Polynomial.map (algebraMap R I.ResidueField)
        (LinearMap.charpoly.{u_1, u_2} (M := A) ((Algebra.lmul R A : (a : A) → Module.End R A) f)) =
      HPow.hPow (α := I.ResidueField[X]) X
        (natDegree.{u_1} (R := R)
          (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f))) ↔
    ∀
      i <
        natDegree.{u_1} (R := R) (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)),
      coeff (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)) i ∈ I

Tactic:
constructor
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Module.Free R A
inst_4 : Module.Finite R A
f : A
I : Ideal R
inst_5 : I.IsPrime
h : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
e :
  Polynomial.map (algebraMap R I.ResidueField)
      (LinearMap.charpoly.{u_1, u_2} (M := A) ((Algebra.lmul R A : (a : A) → Module.End R A) f)) =
    HPow.hPow (α := I.ResidueField[X]) X
      (natDegree.{u_1} (R := R) (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)))
i : ℕ
hi : i < natDegree.{u_1} (R := R) (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f))
⊢ coeff
      (Polynomial.map (algebraMap R I.ResidueField)
        (LinearMap.charpoly.{u_1, u_2} (M := A) ((Algebra.lmul R A : (a : A) → Module.End R A) f)))
      i =
    (HPow.hPow (α := I.ResidueField[X]) X
          (natDegree.{u_1} (R := R)
            (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)))).coeff
      i

Tactic:
replace e := congr(($e).coeff i)
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Module.Free R A
inst_4 : Module.Finite R A
f : A
I : Ideal R
inst_5 : I.IsPrime
h : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
i : ℕ
hi : i < natDegree.{u_1} (R := R) (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f))
e :
  coeff
      (Polynomial.map (algebraMap R I.ResidueField)
        (LinearMap.charpoly.{u_1, u_2} (M := A) ((Algebra.lmul R A : (a : A) → Module.End R A) f)))
      i =
    (HPow.hPow (α := I.ResidueField[X]) X
          (natDegree.{u_1} (R := R)
            (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)))).coeff
      i
⊢ coeff (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)) i ∈ I

Tactic:
simpa only [Algebra.coe_lmul_eq_mul, coeff_map, coeff_X_pow, hi.ne, ↓reduceIte,
      ← RingHom.mem_ker, Ideal.ker_algebraMap_residueField] using e

Premises used: Ideal.ker_algebraMap_residueField, Polynomial.coeff_map, Polynomial.coeff_X_pow, RingHom.mem_ker, reduceIte, Algebra.coe_lmul_eq_mul, LT.lt.ne
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Module.Free R A
inst_4 : Module.Finite R A
f : A
I : Ideal R
inst_5 : I.IsPrime
h : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
H :
  ∀ i < natDegree.{u_1} (R := R) (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)),
    coeff (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)) i ∈ I
inr :
  ∀ (i : ℕ),
    coeff
        (Polynomial.map (algebraMap R I.ResidueField)
          (LinearMap.charpoly.{u_1, u_2} (M := A) ((Algebra.lmul R A : (a : A) → Module.End R A) f)))
        i =
      (HPow.hPow (α := I.ResidueField[X]) X
            (natDegree.{u_1} (R := R)
              (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)))).coeff
        i
⊢ Polynomial.map (algebraMap R I.ResidueField)
      (LinearMap.charpoly.{u_1, u_2} (M := A) ((Algebra.lmul R A : (a : A) → Module.End R A) f)) =
    HPow.hPow (α := I.ResidueField[X]) X
      (natDegree.{u_1} (R := R) (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)))

Tactic:
ext i
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Module.Free R A
inst_4 : Module.Finite R A
f : A
I : Ideal R
inst_5 : I.IsPrime
h : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
H :
  ∀ i < natDegree.{u_1} (R := R) (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)),
    coeff (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)) i ∈ I
i : ℕ
inr :
  ∀
    (hi :
      i =
        natDegree.{u_1} (R := R)
          (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f))),
    coeff
        (Polynomial.map (algebraMap R I.ResidueField)
          (LinearMap.charpoly.{u_1, u_2} (M := A) ((Algebra.lmul R A : (a : A) → Module.End R A) f)))
        i =
      (HPow.hPow (α := I.ResidueField[X]) X
            (natDegree.{u_1} (R := R)
              (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)))).coeff
        i
inr₁ :
  ∀
    (hi :
      i ≠
        natDegree.{u_1} (R := R)
          (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f))),
    coeff
        (Polynomial.map (algebraMap R I.ResidueField)
          (LinearMap.charpoly.{u_1, u_2} (M := A) ((Algebra.lmul R A : (a : A) → Module.End R A) f)))
        i =
      (HPow.hPow (α := I.ResidueField[X]) X
            (natDegree.{u_1} (R := R)
              (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)))).coeff
        i
⊢ coeff
      (Polynomial.map (algebraMap R I.ResidueField)
        (LinearMap.charpoly.{u_1, u_2} (M := A) ((Algebra.lmul R A : (a : A) → Module.End R A) f)))
      i =
    (HPow.hPow (α := I.ResidueField[X]) X
          (natDegree.{u_1} (R := R)
            (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)))).coeff
      i

Tactic:
obtain (hi | hi) := eq_or_ne i ((LinearMap.mul R A) f).charpoly.natDegree

Premises used: eq_or_ne, LinearMap.mul, Polynomial.natDegree, DFunLike.coe, LinearMap.charpoly
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Module.Free R A
inst_4 : Module.Finite R A
f : A
I : Ideal R
inst_5 : I.IsPrime
h : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
H :
  ∀ i < natDegree.{u_1} (R := R) (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)),
    coeff (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)) i ∈ I
i : ℕ
hi : i = natDegree.{u_1} (R := R) (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f))
inr :
  Eq (α := I.ResidueField)
    ((algebraMap R I.ResidueField : (a : R) → I.ResidueField)
      (coeff (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f))
        (natDegree.{u_1} (R := R)
          (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)))))
    1
⊢ coeff
      (Polynomial.map (algebraMap R I.ResidueField)
        (LinearMap.charpoly.{u_1, u_2} (M := A) ((Algebra.lmul R A : (a : A) → Module.End R A) f)))
      i =
    (HPow.hPow (α := I.ResidueField[X]) X
          (natDegree.{u_1} (R := R)
            (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)))).coeff
      i

Tactic:
simp only [Algebra.coe_lmul_eq_mul, hi, coeff_map, coeff_X_pow, ↓reduceIte]

Premises used: Polynomial.coeff_map, Polynomial.coeff_X_pow, reduceIte, Algebra.coe_lmul_eq_mul
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Module.Free R A
inst_4 : Module.Finite R A
f : A
I : Ideal R
inst_5 : I.IsPrime
h : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
H :
  ∀ i < natDegree.{u_1} (R := R) (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)),
    coeff (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)) i ∈ I
i : ℕ
hi : i = natDegree.{u_1} (R := R) (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f))
inr :
  Eq (α := I.ResidueField)
    ((algebraMap R I.ResidueField : (a : R) → I.ResidueField)
      (leadingCoeff (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f))))
    1
inr₁ : Eq (α := I.ResidueField) ((algebraMap R I.ResidueField : (a : R) → I.ResidueField) 1) 1
inr₂ inr₃ : Eq.{u_1 + 1} (α := I.ResidueField) 1 1
⊢ Eq (α := I.ResidueField)
    ((algebraMap R I.ResidueField : (a : R) → I.ResidueField)
      (coeff (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f))
        (natDegree.{u_1} (R := R)
          (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)))))
    1

Tactic:
rw [← Polynomial.leadingCoeff, ((LinearMap.mul R A) f).charpoly_monic, map_one]

Premises used: LinearMap.charpoly_monic, Polynomial.leadingCoeff, map_one, LinearMap.mul, DFunLike.coe
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Module.Free R A
inst_4 : Module.Finite R A
f : A
I : Ideal R
inst_5 : I.IsPrime
h : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
H :
  ∀ i < natDegree.{u_1} (R := R) (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)),
    coeff (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)) i ∈ I
i : ℕ
hi : i ≠ natDegree.{u_1} (R := R) (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f))
inr :
  ∀
    (hi :
      i <
        natDegree.{u_1} (R := R)
          (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f))),
    coeff
        (Polynomial.map (algebraMap R I.ResidueField)
          (LinearMap.charpoly.{u_1, u_2} (M := A) ((Algebra.lmul R A : (a : A) → Module.End R A) f)))
        i =
      (HPow.hPow (α := I.ResidueField[X]) X
            (natDegree.{u_1} (R := R)
              (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)))).coeff
        i
inr₁ :
  ∀
    (hi :
      natDegree.{u_1} (R := R) (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)) <
        i),
    coeff
        (Polynomial.map (algebraMap R I.ResidueField)
          (LinearMap.charpoly.{u_1, u_2} (M := A) ((Algebra.lmul R A : (a : A) → Module.End R A) f)))
        i =
      (HPow.hPow (α := I.ResidueField[X]) X
            (natDegree.{u_1} (R := R)
              (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)))).coeff
        i
⊢ coeff
      (Polynomial.map (algebraMap R I.ResidueField)
        (LinearMap.charpoly.{u_1, u_2} (M := A) ((Algebra.lmul R A : (a : A) → Module.End R A) f)))
      i =
    (HPow.hPow (α := I.ResidueField[X]) X
          (natDegree.{u_1} (R := R)
            (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)))).coeff
      i

Tactic:
obtain (hi | hi) := lt_or_gt_of_ne hi

Premises used: lt_or_gt_of_ne
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Module.Free R A
inst_4 : Module.Finite R A
f : A
I : Ideal R
inst_5 : I.IsPrime
h : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
H :
  ∀ i < natDegree.{u_1} (R := R) (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)),
    coeff (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)) i ∈ I
i : ℕ
hi_1 :
  i ≠ natDegree.{u_1} (R := R) (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f))
hi : i < natDegree.{u_1} (R := R) (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f))
⊢ coeff
      (Polynomial.map (algebraMap R I.ResidueField)
        (LinearMap.charpoly.{u_1, u_2} (M := A) ((Algebra.lmul R A : (a : A) → Module.End R A) f)))
      i =
    (HPow.hPow (α := I.ResidueField[X]) X
          (natDegree.{u_1} (R := R)
            (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)))).coeff
      i

Tactic:
simpa [hi.ne, ← RingHom.mem_ker, Ideal.ker_algebraMap_residueField] using H i hi

Premises used: Ideal.ker_algebraMap_residueField, RingHom.mem_ker, LT.lt.ne
-- Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Module.Free R A
inst_4 : Module.Finite R A
f : A
I : Ideal R
inst_5 : I.IsPrime
h : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
H :
  ∀ i < natDegree.{u_1} (R := R) (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)),
    coeff (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)) i ∈ I
i : ℕ
hi_1 :
  i ≠ natDegree.{u_1} (R := R) (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f))
hi : natDegree.{u_1} (R := R) (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)) < i
⊢ coeff
      (Polynomial.map (algebraMap R I.ResidueField)
        (LinearMap.charpoly.{u_1, u_2} (M := A) ((Algebra.lmul R A : (a : A) → Module.End R A) f)))
      i =
    (HPow.hPow (α := I.ResidueField[X]) X
          (natDegree.{u_1} (R := R)
            (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)))).coeff
      i

Tactic:
simp [hi.ne', coeff_eq_zero_of_natDegree_lt hi]

Premises used: LT.lt.ne', Polynomial.coeff_eq_zero_of_natDegree_lt