awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hg : g.Monic
t : Finset R
ht : Eq (α := Set (PrimeSpectrum R)) (comap C '' (zeroLocus {g} \ zeroLocus {f})) (zeroLocus (↑t : Set R))ᶜ
⊢ IsCompact.{u_1} (X := PrimeSpectrum R) (⋃ (i : (↑(↑t : Set R) : Type u_1)), (zeroLocus {(↑i : R)})ᶜ)
have h : ∀ (i : (↑(↑t : Set R) : Type u_1)), IsCompact (X := PrimeSpectrum R) (zeroLocus {(↑i : R)})ᶜ
Tactic: apply isCompact_iUnion
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hg : g.Monic
⊢ IsOpen (X := PrimeSpectrum R) (comap C '' (zeroLocus {g} \ zeroLocus {f}))
have obtain : ∀ (t : Finset R)
  (ht : Eq (α := Set (PrimeSpectrum R)) (comap C '' (zeroLocus {g} \ zeroLocus {f})) (zeroLocus (↑t : Set R))ᶜ),
  IsOpen (X := PrimeSpectrum R) (comap C '' (zeroLocus {g} \ zeroLocus {f}))
Tactic: obtain ⟨t, ht⟩ := exists_image_comap_of_monic f g hg
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
hg : g.Monic
t : Finset R
ht : Eq (α := Set (PrimeSpectrum R)) (comap C '' (zeroLocus {g} \ zeroLocus {f})) (zeroLocus (↑t : Set R))ᶜ
⊢ IsOpen (X := PrimeSpectrum R) (comap C '' (zeroLocus {g} \ zeroLocus {f}))
have rw : IsOpen (X := PrimeSpectrum R) (zeroLocus (↑t : Set R))ᶜ
Tactic: rw [ht]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
⊢ x ∈ comap C '' (↑(basicOpen f) : Set (PrimeSpectrum (MvPolynomial σ R))) ↔ ∃ (i : σ →₀ ℕ), coeff i f ∉ x.asIdeal
have trans : x ∈ comap C '' (↑(basicOpen f) : Set (PrimeSpectrum (MvPolynomial σ R))) ↔
  Ne (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
    ((map (algebraMap R x.asIdeal.ResidueField) : (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField) f :
      MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
    (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
Tactic: trans f.map (algebraMap R x.asIdeal.ResidueField) ≠ 0
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
trans :
  x ∈ comap C '' (↑(basicOpen f) : Set (PrimeSpectrum (MvPolynomial σ R))) ↔
    Ne (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      ((map (algebraMap R x.asIdeal.ResidueField) : (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField) f :
        MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
⊢ x ∈ comap C '' (↑(basicOpen f) : Set (PrimeSpectrum (MvPolynomial σ R))) ↔ ∃ (i : σ →₀ ℕ), coeff i f ∉ x.asIdeal
have trans₁ : Ne (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
    ((map (algebraMap R x.asIdeal.ResidueField) : (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField) f :
      MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
    (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField) ↔
  ∃ (i : σ →₀ ℕ), coeff i f ∉ x.asIdeal
Tactic: trans f.map (algebraMap R x.asIdeal.ResidueField) ≠ 0
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
⊢ x ∈ comap C '' (↑(basicOpen f) : Set (PrimeSpectrum (MvPolynomial σ R))) ↔
    Ne (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      ((map (algebraMap R x.asIdeal.ResidueField) : (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField) f :
        MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
have refine : IsNilpotent (R := MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)
    ((algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField) :
          (a : MvPolynomial σ R) → MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)
        f :
      MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField) ↔
  Eq (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
    ((map (algebraMap R x.asIdeal.ResidueField) : (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField) f :
      MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
    (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
Tactic: refine (mem_image_comap_basicOpen _ _).trans (not_iff_not.mpr ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField :=
  scalarRTensorAlgEquiv
⊢ IsNilpotent (R := MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)
      ((algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField) :
            (a : MvPolynomial σ R) → MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)
          f :
        MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField) ↔
    Eq (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      ((map (algebraMap R x.asIdeal.ResidueField) : (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField) f :
        MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
have rw : Eq (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
    ((e : (a : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField) → MvPolynomial σ x.asIdeal.ResidueField)
        ((algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField) :
            (a : MvPolynomial σ R) → MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)
          f) :
      MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
    (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField) ↔
  Eq (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
    ((map (algebraMap R x.asIdeal.ResidueField) : (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField) f :
      MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
    (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
Tactic: rw [← IsNilpotent.map_iff e.injective, isNilpotent_iff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField :=
  scalarRTensorAlgEquiv
⊢ Eq (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      ((e : (a : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField) → MvPolynomial σ x.asIdeal.ResidueField)
          ((algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField) :
              (a : MvPolynomial σ R) → MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)
            f) :
        MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField) ↔
    Eq (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      ((map (algebraMap R x.asIdeal.ResidueField) : (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField) f :
        MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
have change : Eq (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
    (((↑e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField →ₐ[R] MvPolynomial σ x.asIdeal.ResidueField).comp
            (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)) :
          (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField)
        f :
      MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
    (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField) ↔
  Eq (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
    ((map (algebraMap R x.asIdeal.ResidueField) : (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField) f :
      MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
    (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
Tactic: change (e.toAlgHom.toRingHom).comp (algebraMap _ _) f = 0 ↔ MvPolynomial.map _ f = 0
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField :=
  scalarRTensorAlgEquiv
⊢ Eq (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      (((↑e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField →ₐ[R] MvPolynomial σ x.asIdeal.ResidueField).comp
              (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)) :
            (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField)
          f :
        MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField) ↔
    Eq (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      ((map (algebraMap R x.asIdeal.ResidueField) : (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField) f :
        MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
have a : Eq (α := MvPolynomial σ R →+* MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
  ((↑e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField →ₐ[R] MvPolynomial σ x.asIdeal.ResidueField).comp
    (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)))
  (map (algebraMap R x.asIdeal.ResidueField))
Tactic: congr!
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField :=
  scalarRTensorAlgEquiv
⊢ Eq (α := MvPolynomial σ R →+* MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
    ((↑e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField →ₐ[R] MvPolynomial σ x.asIdeal.ResidueField).comp
      (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)))
    (map (algebraMap R x.asIdeal.ResidueField))
have a : ∀ (x_1 : R) (m : σ →₀ ℕ),
  Eq.{u_2 + 1} (α := x.asIdeal.ResidueField)
    (coeff m
      ((RingHom.comp (β := MvPolynomial σ R)
            ((↑e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField →ₐ[R] MvPolynomial σ x.asIdeal.ResidueField).comp
              (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)))
            C :
          (a : R) → MvPolynomial σ x.asIdeal.ResidueField)
        x_1))
    (coeff m
      ((RingHom.comp (map (algebraMap R x.asIdeal.ResidueField)) C : (a : R) → MvPolynomial σ x.asIdeal.ResidueField)
        x_1))
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField :=
  scalarRTensorAlgEquiv
a :
  ∀ (x_1 : R) (m : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := x.asIdeal.ResidueField)
      (coeff m
        ((RingHom.comp (β := MvPolynomial σ R)
              ((↑e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField →ₐ[R] MvPolynomial σ x.asIdeal.ResidueField).comp
                (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)))
              C :
            (a : R) → MvPolynomial σ x.asIdeal.ResidueField)
          x_1))
      (coeff m
        ((RingHom.comp (map (algebraMap R x.asIdeal.ResidueField)) C : (a : R) → MvPolynomial σ x.asIdeal.ResidueField)
          x_1))
⊢ Eq (α := MvPolynomial σ R →+* MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
    ((↑e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField →ₐ[R] MvPolynomial σ x.asIdeal.ResidueField).comp
      (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)))
    (map (algebraMap R x.asIdeal.ResidueField))
have a₁ : ∀ (i : σ) (m : σ →₀ ℕ),
  Eq.{u_2 + 1} (α := x.asIdeal.ResidueField)
    (coeff m
      (((↑e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField →ₐ[R] MvPolynomial σ x.asIdeal.ResidueField).comp
            (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)) :
          (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField)
        (X i)))
    (coeff m
      ((map (algebraMap R x.asIdeal.ResidueField) : (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField)
        (X i)))
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
⊢ x ∈ comap C '' (↑(basicOpen f) : Set (PrimeSpectrum (MvPolynomial σ R))) ↔ ∃ (i : σ →₀ ℕ), coeff i f ∉ x.asIdeal
have trans : x ∈ comap C '' (↑(basicOpen f) : Set (PrimeSpectrum (MvPolynomial σ R))) ↔
  Ne (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
    ((map (algebraMap R x.asIdeal.ResidueField) : (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField) f :
      MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
    (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
Tactic: classical
  trans f.map (algebraMap R x.asIdeal.ResidueField) ≠ 0
  · refine (mem_image_comap_basicOpen _ _).trans (not_iff_not.mpr ?_)
    let e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField ≃ₐ[R]
        MvPolynomial σ x.asIdeal.ResidueField := scalarRTensorAlgEquiv
    rw [← IsNilpotent.map_iff e.injective, isNilpotent_iff_eq_zero]
    change (e.toAlgHom.toRingHom).comp (algebraMap _ _) f = 0 ↔ MvPolynomial.map _ f = 0
    congr!
    ext
    · simp [scalarRTensorAlgEquiv, e, coeff_map,
        Algebra.smul_def, apply_ite (f := algebraMap _ _)]
    · simp [e, scalarRTensorAlgEquiv, coeff_map, coeff_X']
  · simp [MvPolynomial.ext_iff, coeff_map]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
trans :
  x ∈ comap C '' (↑(basicOpen f) : Set (PrimeSpectrum (MvPolynomial σ R))) ↔
    Ne (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      ((map (algebraMap R x.asIdeal.ResidueField) : (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField) f :
        MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
      (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
⊢ x ∈ comap C '' (↑(basicOpen f) : Set (PrimeSpectrum (MvPolynomial σ R))) ↔ ∃ (i : σ →₀ ℕ), coeff i f ∉ x.asIdeal
have trans₁ : Ne (α := MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
    ((map (algebraMap R x.asIdeal.ResidueField) : (a : MvPolynomial σ R) → MvPolynomial σ x.asIdeal.ResidueField) f :
      MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField)
    (0 : MvPolynomial.{u_1, u_2} σ x.asIdeal.ResidueField) ↔
  ∃ (i : σ →₀ ℕ), coeff i f ∉ x.asIdeal
Tactic: classical
  trans f.map (algebraMap R x.asIdeal.ResidueField) ≠ 0
  · refine (mem_image_comap_basicOpen _ _).trans (not_iff_not.mpr ?_)
    let e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField ≃ₐ[R]
        MvPolynomial σ x.asIdeal.ResidueField := scalarRTensorAlgEquiv
    rw [← IsNilpotent.map_iff e.injective, isNilpotent_iff_eq_zero]
    change (e.toAlgHom.toRingHom).comp (algebraMap _ _) f = 0 ↔ MvPolynomial.map _ f = 0
    congr!
    ext
    · simp [scalarRTensorAlgEquiv, e, coeff_map,
        Algebra.smul_def, apply_ite (f := algebraMap _ _)]
    · simp [e, scalarRTensorAlgEquiv, coeff_map, coeff_X']
  · simp [MvPolynomial.ext_iff, coeff_map]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
f : MvPolynomial σ R
⊢ comap C '' (↑(basicOpen f) : Set (PrimeSpectrum (MvPolynomial σ R))) =
    (zeroLocus (Set.range fun (m : σ →₀ ℕ) ↦ coeff m f))ᶜ
have h : ∀ (p : PrimeSpectrum R),
  p ∈ comap C '' (↑(basicOpen f) : Set (PrimeSpectrum (MvPolynomial σ R))) ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (Set.range fun (m : σ →₀ ℕ) ↦ coeff m f))ᶜ p
Tactic: ext p
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
f : MvPolynomial σ R
p : PrimeSpectrum R
⊢ p ∈ comap C '' (↑(basicOpen f) : Set (PrimeSpectrum (MvPolynomial σ R))) ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (Set.range fun (m : σ →₀ ℕ) ↦ coeff m f))ᶜ p
have h : (∃ (i : σ →₀ ℕ), coeff i f ∉ p.asIdeal) ↔
  Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (Set.range fun (m : σ →₀ ℕ) ↦ coeff m f))ᶜ p
Tactic: rw [mem_image_comap_C_basicOpen]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
U : Set (PrimeSpectrum (MvPolynomial σ R))
hU : IsOpen U
⊢ IsOpen (comap C '' U)
have obtain : ∀ (S : Set (Set (PrimeSpectrum (MvPolynomial σ R))))
  (hS : S ⊆ Set.range fun (r : MvPolynomial σ R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum (MvPolynomial σ R))))
  (hU : IsOpen (⋃₀ S)), IsOpen (comap C '' ⋃₀ S)
Tactic: obtain ⟨S, hS, rfl⟩ := isTopologicalBasis_basic_opens.open_eq_sUnion hU
Cleared hypotheses: U, hU
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
S : Set (Set (PrimeSpectrum (MvPolynomial σ R)))
hS : S ⊆ Set.range fun (r : MvPolynomial σ R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum (MvPolynomial σ R)))
hU : IsOpen (⋃₀ S)
⊢ IsOpen (comap C '' ⋃₀ S)
have rw : IsOpen (⋃₀ (Set.image (comap C) '' S))
Tactic: rw [Set.image_sUnion]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
S : Set (Set (PrimeSpectrum (MvPolynomial σ R)))
hS : S ⊆ Set.range fun (r : MvPolynomial σ R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum (MvPolynomial σ R)))
hU : IsOpen (⋃₀ S)
⊢ IsOpen (⋃₀ (Set.image (comap C) '' S))
have h : ∀ t ∈ Set.image (comap C) '' S, IsOpen t
Tactic: apply isOpen_sUnion
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
S : Set (Set (PrimeSpectrum (MvPolynomial σ R)))
hS : S ⊆ Set.range fun (r : MvPolynomial σ R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum (MvPolynomial σ R)))
hU : IsOpen (⋃₀ S)
t : Set (PrimeSpectrum (MvPolynomial σ R))
ht : t ∈ S
⊢ IsOpen (comap C '' t)
have h : ∀ (r : MvPolynomial σ R)
  (ht : (fun (r : MvPolynomial σ R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum (MvPolynomial σ R)))) r ∈ S),
  IsOpen.{u_2} (X := PrimeSpectrum R)
    (Set.image (α := PrimeSpectrum (MvPolynomial σ R)) (comap C)
      ((fun (r : MvPolynomial σ R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum (MvPolynomial σ R)))) r))
Tactic: obtain ⟨r, rfl⟩ := hS ht
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
S : Set (Set (PrimeSpectrum (MvPolynomial σ R)))
hS : S ⊆ Set.range fun (r : MvPolynomial σ R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum (MvPolynomial σ R)))
hU : IsOpen (⋃₀ S)
r : MvPolynomial σ R
ht : (fun (r : MvPolynomial σ R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum (MvPolynomial σ R)))) r ∈ S
⊢ IsOpen.{u_2} (X := PrimeSpectrum R)
    (Set.image (α := PrimeSpectrum (MvPolynomial σ R)) (comap C)
      ((fun (r : MvPolynomial σ R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum (MvPolynomial σ R)))) r))
have h : IsOpen.{u_2} (X := PrimeSpectrum R) (zeroLocus (Set.range fun (m : σ →₀ ℕ) ↦ coeff m r))ᶜ
Tactic: simp only [image_comap_C_basicOpen]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
x : PrimeSpectrum R
⊢ ∃ (a : PrimeSpectrum (MvPolynomial σ R)), comap C a = x
have refine : comap (S := MvPolynomial σ R) C (comap (eval₂Hom (RingHom.id R) 0) x) = x
Tactic: refine ⟨comap (eval₂Hom (.id _) 0) x, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
x : PrimeSpectrum R
⊢ Eq (α := R →+* R) (RingHom.comp (β := MvPolynomial σ R) (eval₂Hom (RingHom.id R) 0) C) (RingHom.id R)
have a : ∀ (x : R),
  Eq (α := R) ((RingHom.comp (β := MvPolynomial σ R) (eval₂Hom (RingHom.id R) 0) C : (a : R) → R) x : R)
    ((RingHom.id R : (a : R) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
x : PrimeSpectrum R
⊢ comap (S := MvPolynomial σ R) C (comap (eval₂Hom (RingHom.id R) 0) x) = x
have rw : comap (RingHom.comp (β := MvPolynomial σ R) (eval₂Hom (RingHom.id R) 0) C) x = x
Tactic: rw [← comap_comp_apply, (show (eval₂Hom (.id _) 0).comp C = .id R by ext; simp),
    comap_id]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
x : PrimeSpectrum R
rw : comap (RingHom.comp (β := MvPolynomial σ R) (eval₂Hom (RingHom.id R) 0) C) x = x
⊢ comap (S := MvPolynomial σ R) C (comap (eval₂Hom (RingHom.id R) 0) x) = x
have rw₁ : comap (RingHom.id R) x = x
Tactic: rw [← comap_comp_apply, (show (eval₂Hom (.id _) 0).comp C = .id R by ext; simp),
    comap_id]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Polynomial (goal)
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_1
x : PrimeSpectrum R
rw : comap (RingHom.comp (β := MvPolynomial σ R) (eval₂Hom (RingHom.id R) 0) C) x = x
rw₁ : comap (RingHom.id R) x = x
⊢ comap (S := MvPolynomial σ R) C (comap (eval₂Hom (RingHom.id R) 0) x) = x
have rw₂ : (fun (x : PrimeSpectrum R) ↦ x) x = x
Tactic: rw [← comap_comp_apply, (show (eval₂Hom (.id _) 0).comp C = .id R by ext; simp),
    comap_id]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
s : Set R
⊢ comap f ⁻¹' zeroLocus s = zeroLocus ((⇑f : (a : R) → S) '' s)
have h : ∀ (x : PrimeSpectrum S),
  x ∈ comap f ⁻¹' zeroLocus s ↔ Membership.mem (γ := Set (PrimeSpectrum S)) (zeroLocus ((⇑f : (a : R) → S) '' s)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
R : Type u
S : Type v
S' : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring S'
f : R →+* S
e : R ≃+* S
x : PrimeSpectrum R
⊢ comap e.toRingHom (comap e.symm.toRingHom x) = x
have rw : comap (RingHom.id R) x = x
Tactic: rw [← comap_comp_apply, RingEquiv.toRingHom_eq_coe,
      RingEquiv.toRingHom_eq_coe, RingEquiv.symm_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
x x_1 : (i : ι) × PrimeSpectrum (R i)
i : ι
p : PrimeSpectrum (R i)
j : ι
q : PrimeSpectrum (R j)
eq :
  Eq (α := PrimeSpectrum ((i : ι) → R i)) (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))
    (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) j q))
⊢ Eq (α := (i : ι) × PrimeSpectrum (R i)) (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p)
    (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) j q)
have inl : ∀ (q : PrimeSpectrum (R i))
  (eq :
    Eq (α := PrimeSpectrum ((i : ι) → R i)) (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))
      (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i q))),
  Eq (α := (i : ι) × PrimeSpectrum (R i)) (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p)
    (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i q)
Tactic: obtain rfl | ne := eq_or_ne i j
Cleared hypotheses: j, q, eq