awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ
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
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
-- 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 : ℕ
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
have 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
Tactic: simp only [Algebra.coe_lmul_eq_mul, hi, coeff_map, coeff_X_pow, ↓reduceIte]
-- 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 : ℕ
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))
⊢ 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
have 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
Tactic: rw [← Polynomial.leadingCoeff, ((LinearMap.mul R A) f).charpoly_monic, map_one]
-- 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 : ℕ
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
⊢ 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
have inr₁ : Eq (α := I.ResidueField) ((algebraMap R I.ResidueField : (a : R) → I.ResidueField) 1) 1
Tactic: rw [← Polynomial.leadingCoeff, ((LinearMap.mul R A) f).charpoly_monic, map_one]
-- 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 : ℕ
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
⊢ 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
have inr₂ : Eq.{u_1 + 1} (α := I.ResidueField) 1 1
Tactic: rw [← Polynomial.leadingCoeff, ((LinearMap.mul R A) f).charpoly_monic, map_one]
-- 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 : ℕ
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
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) := lt_or_gt_of_ne hi
-- 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 : ℕ
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
⊢ 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 :
    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: obtain (hi | hi) := lt_or_gt_of_ne hi
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_2
A : Type u_1
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
f : A
s : Set A
x : PrimeSpectrum R
⊢ Membership.mem (γ := Set (PrimeSpectrum R))
      (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus s \ zeroLocus {f})) x ↔
    ¬IsNilpotent (R :=
        TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField)
        ((algebraMap A
                (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
                  x.asIdeal.ResidueField) :
              (a : A) → (A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)
            f :
          TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField)
have mp : Membership.mem (γ := Set (PrimeSpectrum R))
    (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus s \ zeroLocus {f})) x →
  ¬IsNilpotent (R :=
      TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField)
      ((algebraMap A
              (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
                x.asIdeal.ResidueField) :
            (a : A) → (A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)
          f :
        TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_2
A : Type u_1
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
f : A
s : Set A
x : PrimeSpectrum R
mp :
  Membership.mem (γ := Set (PrimeSpectrum R))
      (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus s \ zeroLocus {f})) x →
    ¬IsNilpotent (R :=
        TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField)
        ((algebraMap A
                (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
                  x.asIdeal.ResidueField) :
              (a : A) → (A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)
            f :
          TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField)
⊢ Membership.mem (γ := Set (PrimeSpectrum R))
      (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus s \ zeroLocus {f})) x ↔
    ¬IsNilpotent (R :=
        TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField)
        ((algebraMap A
                (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
                  x.asIdeal.ResidueField) :
              (a : A) → (A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)
            f :
          TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField)
have mpr : ¬IsNilpotent (R :=
      TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField)
      ((algebraMap A
              (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
                x.asIdeal.ResidueField) :
            (a : A) → (A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)
          f :
        TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField) →
  Membership.mem (γ := Set (PrimeSpectrum R))
    (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus s \ zeroLocus {f})) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (hypothesis)
Goal:
R : Type u_2
A : Type u_1
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
f : A
s : Set A
q : PrimeSpectrum A
hqg : Membership.mem (γ := Set (PrimeSpectrum A)) (zeroLocus s) q
hqf : q ∉ zeroLocus {f}
H :
  IsNilpotent (R :=
    TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
      (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q))))
    ((algebraMap A
            (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
              (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q)))) :
          (a : A) → (A ⧸ Ideal.span s) ⊗[R] (comap (algebraMap R A) q).asIdeal.ResidueField)
        f :
      TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
        (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q))))
⊢ False
have hqg₁ : s ⊆ (↑q.asIdeal : Set A)
Tactic: simp only [mem_zeroLocus, Set.singleton_subset_iff, SetLike.mem_coe] at hqg hqf
Cleared hypotheses: hqg, hqf
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (hypothesis)
Goal:
R : Type u_2
A : Type u_1
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
f : A
s : Set A
q : PrimeSpectrum A
hqg : Membership.mem (γ := Set (PrimeSpectrum A)) (zeroLocus s) q
hqf : q ∉ zeroLocus {f}
H :
  IsNilpotent (R :=
    TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
      (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q))))
    ((algebraMap A
            (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
              (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q)))) :
          (a : A) → (A ⧸ Ideal.span s) ⊗[R] (comap (algebraMap R A) q).asIdeal.ResidueField)
        f :
      TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
        (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q))))
hqg₁ : s ⊆ (↑q.asIdeal : Set A)
⊢ False
have hqf₁ : f ∉ q.asIdeal
Tactic: simp only [mem_zeroLocus, Set.singleton_subset_iff, SetLike.mem_coe] at hqg hqf
Cleared hypotheses: hqg, hqf
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_2
A : Type u_1
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
f : A
s : Set A
q : PrimeSpectrum A
H :
  IsNilpotent (R :=
    TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
      (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q))))
    ((algebraMap A
            (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
              (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q)))) :
          (a : A) → (A ⧸ Ideal.span s) ⊗[R] (comap (algebraMap R A) q).asIdeal.ResidueField)
        f :
      TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
        (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q))))
hqg : s ⊆ (↑q.asIdeal : Set A)
hqf : f ∉ q.asIdeal
⊢ LE.le (α := Ideal A) (Ideal.span s)
    (RingHom.ker (F := A →+* q.asIdeal.ResidueField) (algebraMap A q.asIdeal.ResidueField))
have rwa : s ⊆ (↑(RingHom.ker (F := A →+* q.asIdeal.ResidueField) (algebraMap A q.asIdeal.ResidueField)) : Set A)
Tactic: rwa [Ideal.span_le, Ideal.ker_algebraMap_residueField]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (hypothesis)
Goal:
R : Type u_2
A : Type u_1
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
f : A
s : Set A
q : PrimeSpectrum A
H :
  IsNilpotent (R :=
    TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
      (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q))))
    ((algebraMap A
            (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
              (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q)))) :
          (a : A) → (A ⧸ Ideal.span s) ⊗[R] (comap (algebraMap R A) q).asIdeal.ResidueField)
        f :
      TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
        (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q))))
hqg : s ⊆ (↑q.asIdeal : Set A)
hqf : f ∉ q.asIdeal
⊢ False
have hs : LE.le (α := Ideal A) (Ideal.span s)
  (RingHom.ker (F := A →+* q.asIdeal.ResidueField) (algebraMap A q.asIdeal.ResidueField))
Tactic: have hs : Ideal.span s ≤ RingHom.ker (algebraMap A q.asIdeal.ResidueField) := by
      rwa [Ideal.span_le, Ideal.ker_algebraMap_residueField]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (hypothesis)
Goal:
R : Type u_2
A : Type u_1
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
f : A
s : Set A
q : PrimeSpectrum A
H :
  IsNilpotent (R :=
    TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
      (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q))))
    ((algebraMap A
            (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
              (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q)))) :
          (a : A) → (A ⧸ Ideal.span s) ⊗[R] (comap (algebraMap R A) q).asIdeal.ResidueField)
        f :
      TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
        (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q))))
hqg : s ⊆ (↑q.asIdeal : Set A)
hqf : f ∉ q.asIdeal
hs :
  LE.le (α := Ideal A) (Ideal.span s)
    (RingHom.ker (F := A →+* q.asIdeal.ResidueField) (algebraMap A q.asIdeal.ResidueField))
F : TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
    (Ideal.ResidueField (Ideal.comap (F := R →+* A) (algebraMap R A) q.asIdeal)) →ₐ[A]
  q.asIdeal.ResidueField :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this :
  IsNilpotent.{u_1} (R := q.asIdeal.ResidueField)
    ((F : (a : (A ⧸ Ideal.span s) ⊗[R] (comap (algebraMap R A) q).asIdeal.ResidueField) → q.asIdeal.ResidueField)
        ((algebraMap A
              (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
                (Ideal.ResidueField (asIdeal (comap (algebraMap R A) q)))) :
            (a : A) → (A ⧸ Ideal.span s) ⊗[R] (comap (algebraMap R A) q).asIdeal.ResidueField)
          f) :
      q.asIdeal.ResidueField)
⊢ False
have this₁ : f ∈ q.asIdeal
Tactic: rw [AlgHom.commutes, isNilpotent_iff_eq_zero, ← RingHom.mem_ker,
      Ideal.ker_algebraMap_residueField] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (hypothesis)
Goal:
R : Type u_2
A : Type u_1
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
f : A
s : Set A
x : PrimeSpectrum R
H :
  ¬IsNilpotent (R :=
      TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField)
      ((algebraMap A
              (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
                x.asIdeal.ResidueField) :
            (a : A) → (A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)
          f :
        TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField)
⊢ Membership.mem (γ := Set (PrimeSpectrum R))
    (Set.image (α := PrimeSpectrum A) (comap (algebraMap R A)) (zeroLocus s \ zeroLocus {f})) x
have H₁ : ¬∀
    ⦃I :
      Ideal
        (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
          x.asIdeal.ResidueField)⦄,
    Membership.mem (γ :=
        Set
          (Ideal
            (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
              x.asIdeal.ResidueField)))
        {J :
          Ideal
            (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
              x.asIdeal.ResidueField) |
          J.IsPrime}
        I →
      Membership.mem (α :=
        TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField) I
        ((algebraMap A
                (TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s))
                  x.asIdeal.ResidueField) :
              (a : A) → (A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)
            f :
          TensorProduct.{u_2, u_1, u_2} R (HasQuotient.Quotient A (B := Ideal A) (Ideal.span s)) x.asIdeal.ResidueField)
Tactic: rw [← mem_nilradical, nilradical_eq_sInf, Ideal.mem_sInf] at H
Cleared hypotheses: H