awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
p : Ideal R
inst_2 : p.IsPrime
obtain :
  ∀ (r : R)
    (hr :
      Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
        (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
            { asIdeal := p, isPrime := ⋯ } 1 :
          (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl)),
    ∃ r ∉ p, IsIdempotentElem r ∧ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q
⊢ ∃ r ∉ p, IsIdempotentElem r ∧ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q
have obtain₁ : ∀ (r : R)
  (hr :
    Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
      (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
          { asIdeal := p, isPrime := sorry } 1 :
        (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl))
  (this :
    Eq (α := Localization (M := R) p.primeCompl)
      ((algebraMap R (Localization (M := R) p.primeCompl) : (a : R) → Localization p.primeCompl) r :
        Localization (M := R) p.primeCompl)
      (1 : Localization (M := R) p.primeCompl)),
  ∃ r ∉ p, IsIdempotentElem r ∧ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q
Tactic: classical
  obtain ⟨r, hr⟩ := PrimeSpectrum.toPiLocalization_bijective.2 (Pi.single ⟨p, inferInstance⟩ 1)
  have : algebraMap R (Localization p.primeCompl) r = 1 := by
    simpa [PrimeSpectrum.toPiLocalization,
      -FaithfulSMul.algebraMap_eq_one_iff] using funext_iff.mp hr ⟨p, inferInstance⟩
  refine ⟨r, ?_, ?_, ?_⟩
  · rw [← IsLocalization.AtPrime.to_map_mem_maximal_iff (Localization.AtPrime p) p, this]
    simp
  · apply PrimeSpectrum.toPiLocalization_bijective.injective
    simp [map_mul, hr, ← Pi.single_mul]
  · intro q hq e
    have : PrimeSpectrum.mk q inferInstance ≠ ⟨p, inferInstance⟩ := ne_of_apply_ne (·.1) e
    have : (algebraMap R (Localization.AtPrime q)) r = 0 := by
      simpa [PrimeSpectrum.toPiLocalization, this,
        -FaithfulSMul.algebraMap_eq_zero_iff] using funext_iff.mp hr ⟨q, inferInstance⟩
    rw [← IsLocalization.AtPrime.to_map_mem_maximal_iff (Localization.AtPrime q) q, this]
    simp
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
p : Ideal R
inst_2 : p.IsPrime
obtain :
  ∀ (r : R)
    (hr :
      Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
        (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
            { asIdeal := p, isPrime := ⋯ } 1 :
          (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl)),
    ∃ r ∉ p, IsIdempotentElem r ∧ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q
obtain₁ :
  ∀ (r : R)
    (hr :
      Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
        (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
            { asIdeal := p, isPrime := ⋯ } 1 :
          (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl))
    (this :
      Eq (α := Localization (M := R) p.primeCompl)
        ((algebraMap R (Localization (M := R) p.primeCompl) : (a : R) → Localization p.primeCompl) r :
          Localization (M := R) p.primeCompl)
        (1 : Localization (M := R) p.primeCompl)),
    ∃ r ∉ p, IsIdempotentElem r ∧ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q
⊢ ∃ r ∉ p, IsIdempotentElem r ∧ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q
have refine_1 : ∀ (r : R)
  (hr :
    Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
      (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
          { asIdeal := p, isPrime := sorry } 1 :
        (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl))
  (this :
    Eq (α := Localization (M := R) p.primeCompl)
      ((algebraMap R (Localization (M := R) p.primeCompl) : (a : R) → Localization p.primeCompl) r :
        Localization (M := R) p.primeCompl)
      (1 : Localization (M := R) p.primeCompl)),
  r ∉ p
Tactic: classical
  obtain ⟨r, hr⟩ := PrimeSpectrum.toPiLocalization_bijective.2 (Pi.single ⟨p, inferInstance⟩ 1)
  have : algebraMap R (Localization p.primeCompl) r = 1 := by
    simpa [PrimeSpectrum.toPiLocalization,
      -FaithfulSMul.algebraMap_eq_one_iff] using funext_iff.mp hr ⟨p, inferInstance⟩
  refine ⟨r, ?_, ?_, ?_⟩
  · rw [← IsLocalization.AtPrime.to_map_mem_maximal_iff (Localization.AtPrime p) p, this]
    simp
  · apply PrimeSpectrum.toPiLocalization_bijective.injective
    simp [map_mul, hr, ← Pi.single_mul]
  · intro q hq e
    have : PrimeSpectrum.mk q inferInstance ≠ ⟨p, inferInstance⟩ := ne_of_apply_ne (·.1) e
    have : (algebraMap R (Localization.AtPrime q)) r = 0 := by
      simpa [PrimeSpectrum.toPiLocalization, this,
        -FaithfulSMul.algebraMap_eq_zero_iff] using funext_iff.mp hr ⟨q, inferInstance⟩
    rw [← IsLocalization.AtPrime.to_map_mem_maximal_iff (Localization.AtPrime q) q, this]
    simp
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
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
⊢ 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
have inl : Subsingleton R →
  (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: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
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
inl :
  Subsingleton R →
    (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)
⊢ 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
have inr : Nontrivial R →
  (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: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (hypothesis)
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
⊢ 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
have this : Subsingleton (A ⊗[R] I.ResidueField)
Tactic: have := (algebraMap R (A ⊗[R] I.ResidueField)).codomain_trivial
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
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
have rw : Module.finrank.{u_1, u_1} I.ResidueField I.ResidueField * Module.finrank R A = Module.finrank R A
Tactic: rw [Module.finrank_tensorProduct, Module.finrank_self, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
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
⊢ Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
have rw₁ : 1 * Module.finrank R A = Module.finrank R A
Tactic: rw [Module.finrank_tensorProduct, Module.finrank_self, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
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
⊢ Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
have rw₂ : Module.finrank R A = Module.finrank R A
Tactic: rw [Module.finrank_tensorProduct, Module.finrank_self, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (hypothesis)
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
⊢ 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
have this : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
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
⊢ 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
have 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
Tactic: rw [← IsNilpotent.map_iff (Algebra.TensorProduct.comm R A I.ResidueField).injective]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
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
⊢ 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
have 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
Tactic: simp only [Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self, RingHom.id_apply,
    Algebra.coe_lmul_eq_mul, Algebra.TensorProduct.comm_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
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
⊢ 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
have 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
Tactic: rw [← IsNilpotent.map_iff (Algebra.lmul_injective (R := I.ResidueField)),
    LinearMap.isNilpotent_iff_charpoly, ← Algebra.baseChange_lmul, LinearMap.charpoly_baseChange]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
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
⊢ 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
have 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
Tactic: simp_rw [this, ← ((LinearMap.mul R A) f).charpoly_natDegree]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
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
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
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
        (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
have 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)))
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (hypothesis)
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 (LinearMap.charpoly.{u_1, u_2} (M := A) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) f)) i ∈ I
have 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
Tactic: replace e := congr(($e).coeff i)
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
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
⊢ 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)))
have 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
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
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 : ℕ
⊢ 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
have 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
Tactic: obtain (hi | hi) := eq_or_ne i ((LinearMap.mul R A) f).charpoly.natDegree