awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
P : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring P
f : R →+* S
g : S →+* P
⊢ mapPiLocalization (g.comp f) = (mapPiLocalization g).comp (mapPiLocalization f)
have a : ∀ (x : PiLocalization R) (x_1 : PrimeSpectrum P),
  Eq.{u_3 + 1} (α := Localization (M := P) x_1.asIdeal.primeCompl)
    ((mapPiLocalization (g.comp f) : (a : PiLocalization R) → PiLocalization P) x x_1 :
      Localization (M := P) x_1.asIdeal.primeCompl)
    (((mapPiLocalization g).comp (mapPiLocalization f) : (a : PiLocalization R) → PiLocalization P) x x_1 :
      Localization (M := P) x_1.asIdeal.primeCompl)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f_1 : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f_1 : (a : R) → S)
f : R ≃+* S := RingEquiv.ofBijective f_1 hf
refine_3 :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := PiLocalization R) (β := PiLocalization S)
    (⇑(mapPiLocalization f_1) : (a : PiLocalization R) → PiLocalization S)
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := PiLocalization R) (β := PiLocalization S)
    (⇑(mapPiLocalization f_1) : (a : PiLocalization R) → PiLocalization S)
have refine_1 : Eq (α := PiLocalization S →+* PiLocalization S)
  (RingHom.comp (β := PiLocalization R) (mapPiLocalization (↑f : R →+* S)) (mapPiLocalization (↑f.symm : S →+* R)))
  (RingHom.id (PiLocalization S))
Tactic: let e := RingEquiv.ofRingHom (mapPiLocalization (f : R →+* S)) (mapPiLocalization f.symm) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f_1 : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f_1 : (a : R) → S)
f : R ≃+* S := RingEquiv.ofBijective f_1 hf
refine_3 :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := PiLocalization R) (β := PiLocalization S)
    (⇑(mapPiLocalization f_1) : (a : PiLocalization R) → PiLocalization S)
refine_1 :
  Eq (α := PiLocalization S →+* PiLocalization S)
    (RingHom.comp (β := PiLocalization R) (mapPiLocalization (↑f : R →+* S)) (mapPiLocalization (↑f.symm : S →+* R)))
    (RingHom.id (PiLocalization S))
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := PiLocalization R) (β := PiLocalization S)
    (⇑(mapPiLocalization f_1) : (a : PiLocalization R) → PiLocalization S)
have refine_2 : Eq (α := PiLocalization R →+* PiLocalization R)
  (RingHom.comp (β := PiLocalization S) (mapPiLocalization (↑f.symm : S →+* R)) (mapPiLocalization (↑f : R →+* S)))
  (RingHom.id (PiLocalization R))
Tactic: let e := RingEquiv.ofRingHom (mapPiLocalization (f : R →+* S)) (mapPiLocalization f.symm) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f_1 : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f_1 : (a : R) → S)
f : R ≃+* S := RingEquiv.ofBijective f_1 hf
⊢ Eq (α := PiLocalization S →+* PiLocalization S)
    (RingHom.comp (β := PiLocalization R) (mapPiLocalization (↑f : R →+* S)) (mapPiLocalization (↑f.symm : S →+* R)))
    (RingHom.id (PiLocalization S))
have refine_1 : Eq (α := PiLocalization S →+* PiLocalization S)
  (mapPiLocalization (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : R →+* S) (↑f.symm : S →+* R)))
  (RingHom.id (PiLocalization S))
Tactic: rw [← mapPiLocalization_comp, RingEquiv.comp_symm, mapPiLocalization_id]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f_1 : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f_1 : (a : R) → S)
f : R ≃+* S := RingEquiv.ofBijective f_1 hf
refine_1 :
  Eq (α := PiLocalization S →+* PiLocalization S)
    (mapPiLocalization (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : R →+* S) (↑f.symm : S →+* R)))
    (RingHom.id (PiLocalization S))
⊢ Eq (α := PiLocalization S →+* PiLocalization S)
    (RingHom.comp (β := PiLocalization R) (mapPiLocalization (↑f : R →+* S)) (mapPiLocalization (↑f.symm : S →+* R)))
    (RingHom.id (PiLocalization S))
have refine_1₁ : Eq (α := PiLocalization S →+* PiLocalization S) (mapPiLocalization (RingHom.id S)) (RingHom.id (PiLocalization S))
Tactic: rw [← mapPiLocalization_comp, RingEquiv.comp_symm, mapPiLocalization_id]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f_1 : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f_1 : (a : R) → S)
f : R ≃+* S := RingEquiv.ofBijective f_1 hf
refine_1 :
  Eq (α := PiLocalization S →+* PiLocalization S)
    (mapPiLocalization (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : R →+* S) (↑f.symm : S →+* R)))
    (RingHom.id (PiLocalization S))
refine_1₁ :
  Eq (α := PiLocalization S →+* PiLocalization S) (mapPiLocalization (RingHom.id S)) (RingHom.id (PiLocalization S))
⊢ Eq (α := PiLocalization S →+* PiLocalization S)
    (RingHom.comp (β := PiLocalization R) (mapPiLocalization (↑f : R →+* S)) (mapPiLocalization (↑f.symm : S →+* R)))
    (RingHom.id (PiLocalization S))
have refine_1₂ : Eq.{u_2 + 1} (α := PiLocalization S →+* PiLocalization S) (RingHom.id (PiLocalization S))
  (RingHom.id (PiLocalization S))
Tactic: rw [← mapPiLocalization_comp, RingEquiv.comp_symm, mapPiLocalization_id]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f_1 : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f_1 : (a : R) → S)
f : R ≃+* S := RingEquiv.ofBijective f_1 hf
⊢ Eq (α := PiLocalization R →+* PiLocalization R)
    (RingHom.comp (β := PiLocalization S) (mapPiLocalization (↑f.symm : S →+* R)) (mapPiLocalization (↑f : R →+* S)))
    (RingHom.id (PiLocalization R))
have refine_2 : Eq (α := PiLocalization R →+* PiLocalization R)
  (mapPiLocalization (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f.symm : S →+* R) (↑f : R →+* S)))
  (RingHom.id (PiLocalization R))
Tactic: rw [← mapPiLocalization_comp, RingEquiv.symm_comp, mapPiLocalization_id]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f_1 : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f_1 : (a : R) → S)
f : R ≃+* S := RingEquiv.ofBijective f_1 hf
refine_2 :
  Eq (α := PiLocalization R →+* PiLocalization R)
    (mapPiLocalization (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f.symm : S →+* R) (↑f : R →+* S)))
    (RingHom.id (PiLocalization R))
⊢ Eq (α := PiLocalization R →+* PiLocalization R)
    (RingHom.comp (β := PiLocalization S) (mapPiLocalization (↑f.symm : S →+* R)) (mapPiLocalization (↑f : R →+* S)))
    (RingHom.id (PiLocalization R))
have refine_2₁ : Eq (α := PiLocalization R →+* PiLocalization R) (mapPiLocalization (RingHom.id R)) (RingHom.id (PiLocalization R))
Tactic: rw [← mapPiLocalization_comp, RingEquiv.symm_comp, mapPiLocalization_id]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f_1 : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f_1 : (a : R) → S)
f : R ≃+* S := RingEquiv.ofBijective f_1 hf
refine_2 :
  Eq (α := PiLocalization R →+* PiLocalization R)
    (mapPiLocalization (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f.symm : S →+* R) (↑f : R →+* S)))
    (RingHom.id (PiLocalization R))
refine_2₁ :
  Eq (α := PiLocalization R →+* PiLocalization R) (mapPiLocalization (RingHom.id R)) (RingHom.id (PiLocalization R))
⊢ Eq (α := PiLocalization R →+* PiLocalization R)
    (RingHom.comp (β := PiLocalization S) (mapPiLocalization (↑f.symm : S →+* R)) (mapPiLocalization (↑f : R →+* S)))
    (RingHom.id (PiLocalization R))
have refine_2₂ : Eq.{u_1 + 1} (α := PiLocalization R →+* PiLocalization R) (RingHom.id (PiLocalization R))
  (RingHom.id (PiLocalization R))
Tactic: rw [← mapPiLocalization_comp, RingEquiv.symm_comp, mapPiLocalization_id]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
ι : Type u_5
R : ι → Type u_4
inst : (i : ι) → CommSemiring (R i)
inst_1 : ∀ (i : ι), Nontrivial.{u_4} (R i)
inst_2 : Infinite ι
surj :
  Function.Surjective (α := (i : ι) → R i) (β := PiLocalization ((i : ι) → R i))
    (⇑(toPiLocalization ((i : ι) → R i)) : (a : (i : ι) → R i) → PiLocalization ((i : ι) → R i))
⊢ Function.Surjective (α := (i : ι) → R i) (β := MaximalSpectrum.PiLocalization ((i : ι) → R i))
    (⇑(MaximalSpectrum.toPiLocalization ((i : ι) → R i)) :
      (a : (i : ι) → R i) → MaximalSpectrum.PiLocalization ((i : ι) → R i))
have rw : Function.Surjective (α := (i : ι) → R i) (β := MaximalSpectrum.PiLocalization ((i : ι) → R i))
  (⇑(↑(AlgHom.comp (piLocalizationToMaximal ((i : ι) → R i)) (toPiLocalization ((i : ι) → R i))) :
        ((i : ι) → R i) →+* MaximalSpectrum.PiLocalization ((i : ι) → R i)) :
    (a : (i : ι) → R i) → MaximalSpectrum.PiLocalization ((i : ι) → R i))
Tactic: rw [← AlgHom.coe_toRingHom, ← piLocalizationToMaximal_comp_toPiLocalization]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
surj : Function.Surjective (α := R) (β := PiLocalization R) (⇑(toPiLocalization R) : (a : R) → PiLocalization R)
⊢ Finite.{u_1 + 1} (PrimeSpectrum R)
have surj₁ : Function.Surjective (α := R) (β := PiLocalization (PiLocalization R))
  (Function.comp (β := PiLocalization R)
    (⇑(mapPiLocalization (AlgHom.toRingHom (toPiLocalization R))) :
      (a : PiLocalization R) → PiLocalization (PiLocalization R))
    (⇑(toPiLocalization R) : (a : R) → PiLocalization R))
Tactic: replace surj := (mapPiLocalization_bijective _ ⟨toPiLocalization_injective R, surj⟩).2.comp surj
Cleared hypotheses: surj
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
surj :
  Function.Surjective (α := R) (β := PiLocalization (PiLocalization R))
    (Function.comp (β := PiLocalization R)
      (⇑(mapPiLocalization (AlgHom.toRingHom (toPiLocalization R))) :
        (a : PiLocalization R) → PiLocalization (PiLocalization R))
      (⇑(toPiLocalization R) : (a : R) → PiLocalization R))
⊢ Finite.{u_1 + 1} (PrimeSpectrum R)
have surj₁ : Function.Surjective (α := R) (β := PiLocalization (PiLocalization R))
  (Function.comp (β := PiLocalization R)
    (⇑(AlgHom.toRingHom (toPiLocalization (PiLocalization R))) :
      (a : PiLocalization R) → PiLocalization (PiLocalization R))
    (⇑(AlgHom.toRingHom (toPiLocalization R)) : (a : R) → PiLocalization R))
Tactic: rw [← AlgHom.coe_toRingHom,
    ← RingHom.coe_comp, mapPiLocalization_naturality, RingHom.coe_comp] at surj
Cleared hypotheses: surj
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Topology (goal)
Goal:
R : Type u
inst : CommRing R
⊢ Eq.{u + 1} (α := Set (PrimeSpectrum R)) (range toPrimeSpectrum)
    {x : PrimeSpectrum R | IsClosed (X := PrimeSpectrum R) {x}}
have simp : Eq.{u + 1} (α := Set (PrimeSpectrum R)) (range toPrimeSpectrum) {x : PrimeSpectrum R | x.asIdeal.IsMaximal}
Tactic: simp only [isClosed_singleton_iff_isMaximal]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Topology (goal)
Goal:
R : Type u
inst : CommRing R
⊢ Eq.{u + 1} (α := Set (PrimeSpectrum R)) (range toPrimeSpectrum) {x : PrimeSpectrum R | x.asIdeal.IsMaximal}
have h : ∀ (x : Ideal R) (isPrime : x.IsPrime),
  Membership.mem (γ := Set (PrimeSpectrum R)) (range toPrimeSpectrum)
      { asIdeal := x, isPrime := isPrime : PrimeSpectrum R } ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) {x : PrimeSpectrum R | x.asIdeal.IsMaximal}
      { asIdeal := x, isPrime := isPrime : PrimeSpectrum R }
Tactic: ext ⟨x, _⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
⊢ Nonempty.{u + 1} (PrimeSpectrum R) ↔ Nontrivial R
have refine_1 : Nonempty.{u + 1} (PrimeSpectrum R) → ∀ (p : PrimeSpectrum R) (h : Eq.{u + 1} (α := R) 0 1), p.asIdeal = ⊤
Tactic: refine ⟨fun ⟨p⟩ ↦ ⟨0, 1, fun h ↦ p.2.ne_top ?_⟩, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
refine_1 : Nonempty.{u + 1} (PrimeSpectrum R) → ∀ (p : PrimeSpectrum R) (h : Eq.{u + 1} (α := R) 0 1), p.asIdeal = ⊤
⊢ Nonempty.{u + 1} (PrimeSpectrum R) ↔ Nontrivial R
have refine_2 : ∀ (h : Nontrivial R), Nonempty.{u + 1} (PrimeSpectrum R)
Tactic: refine ⟨fun ⟨p⟩ ↦ ⟨0, 1, fun h ↦ p.2.ne_top ?_⟩, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
h : Nontrivial R
⊢ Nonempty.{u + 1} (PrimeSpectrum R)
have refine_2 : ∀ (I : Ideal R) (hI : I.IsMaximal), Nonempty.{u + 1} (PrimeSpectrum R)
Tactic: obtain ⟨I, hI⟩ := Ideal.exists_maximal R
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
⊢ IsEmpty.{u + 1} (PrimeSpectrum R) ↔ Subsingleton R
have contrapose! : Nonempty.{u + 1} (PrimeSpectrum R) ↔ Nontrivial R
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
⊢ Function.Bijective (α := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)) (primeSpectrumProdOfSum R S)
have left : Function.Injective (α := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)) (primeSpectrumProdOfSum R S)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
left : Function.Injective (α := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)) (primeSpectrumProdOfSum R S)
⊢ Function.Bijective (α := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)) (primeSpectrumProdOfSum R S)
have right : Function.Surjective (α := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)) (primeSpectrumProdOfSum R S)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
I : Ideal R
hI : I.IsPrime
I' : Ideal R
hI' : I'.IsPrime
h :
  Eq (α := PrimeSpectrum (R × S)) (primeSpectrumProdOfSum R S (Sum.inl { asIdeal := I, isPrime := hI }))
    (primeSpectrumProdOfSum R S (Sum.inl { asIdeal := I', isPrime := hI' }))
⊢ Eq (α := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)) (Sum.inl { asIdeal := I, isPrime := hI })
    (Sum.inl { asIdeal := I', isPrime := hI' })
have h₁ : I = I' ∧ True
Tactic: simp only [mk.injEq, Ideal.prod_inj, primeSpectrumProdOfSum] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
I : Ideal R
hI : I.IsPrime
J' : Ideal S
hJ' : J'.IsPrime
h :
  primeSpectrumProdOfSum R S (Sum.inl { asIdeal := I, isPrime := hI }) =
    primeSpectrumProdOfSum R S (Sum.inr { asIdeal := J', isPrime := hJ' : PrimeSpectrum S })
⊢ Sum.inl { asIdeal := I, isPrime := hI } = Sum.inr { asIdeal := J', isPrime := hJ' : PrimeSpectrum S }
have h₁ : I = ⊤ ∧ ⊤ = J'
Tactic: simp only [mk.injEq, Ideal.prod_inj, primeSpectrumProdOfSum] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
J : Ideal S
hJ : J.IsPrime
I' : Ideal R
hI' : I'.IsPrime
h :
  primeSpectrumProdOfSum R S (Sum.inr { asIdeal := J, isPrime := hJ }) =
    primeSpectrumProdOfSum R S (Sum.inl { asIdeal := I', isPrime := hI' : PrimeSpectrum R })
⊢ Sum.inr { asIdeal := J, isPrime := hJ } = Sum.inl { asIdeal := I', isPrime := hI' : PrimeSpectrum R }
have h₁ : ⊤ = I' ∧ J = ⊤
Tactic: simp only [mk.injEq, Ideal.prod_inj, primeSpectrumProdOfSum] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
J : Ideal S
hJ : J.IsPrime
J' : Ideal S
hJ' : J'.IsPrime
h :
  Eq (α := PrimeSpectrum (R × S)) (primeSpectrumProdOfSum R S (Sum.inr { asIdeal := J, isPrime := hJ }))
    (primeSpectrumProdOfSum R S (Sum.inr { asIdeal := J', isPrime := hJ' }))
⊢ Eq (α := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)) (Sum.inr { asIdeal := J, isPrime := hJ })
    (Sum.inr { asIdeal := J', isPrime := hJ' })
have h₁ : True ∧ J = J'
Tactic: simp only [mk.injEq, Ideal.prod_inj, primeSpectrumProdOfSum] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
I : Ideal (R × S)
hI : I.IsPrime
⊢ ∃ (a : Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)), primeSpectrumProdOfSum R S a = { asIdeal := I, isPrime := hI }
have right : ∀ (p : Ideal R) (hp : p.IsPrime) (hI : Ideal.IsPrime (α := R × S) (p.prod ⊤)),
  ∃ (a : Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)),
    primeSpectrumProdOfSum R S a = { asIdeal := p.prod ⊤, isPrime := hI }
Tactic: rcases (Ideal.ideal_prod_prime I).mp hI with (⟨p, ⟨hp, rfl⟩⟩ | ⟨p, ⟨hp, rfl⟩⟩)
Cleared hypotheses: I, hI
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
I : Ideal (R × S)
hI : I.IsPrime
right :
  ∀ (p : Ideal R) (hp : p.IsPrime) (hI : Ideal.IsPrime (α := R × S) (p.prod ⊤)),
    ∃ (a : Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)),
      primeSpectrumProdOfSum R S a = { asIdeal := p.prod ⊤, isPrime := hI }
⊢ ∃ (a : Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)), primeSpectrumProdOfSum R S a = { asIdeal := I, isPrime := hI }
have right₁ : ∀ (p : Ideal S) (hp : p.IsPrime) (hI : Ideal.IsPrime (α := R × S) (Ideal.prod ⊤ p)),
  ∃ (a : Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)),
    primeSpectrumProdOfSum R S a = { asIdeal := Ideal.prod ⊤ p, isPrime := hI }
Tactic: rcases (Ideal.ideal_prod_prime I).mp hI with (⟨p, ⟨hp, rfl⟩⟩ | ⟨p, ⟨hp, rfl⟩⟩)
Cleared hypotheses: I, hI
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
x : PrimeSpectrum R
⊢ Eq (α := Ideal (R × S))
    (asIdeal
      ((Equiv.symm (primeSpectrumProd R S) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        (Sum.inl x)))
    (x.asIdeal.prod ⊤)
have mk : ∀ (asIdeal : Ideal R) (isPrime : asIdeal.IsPrime),
  Eq (α := Ideal (R × S))
    (PrimeSpectrum.asIdeal
      ((Equiv.symm (primeSpectrumProd R S) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        (Sum.inl { asIdeal := asIdeal, isPrime := isPrime })))
    ({ asIdeal := asIdeal, isPrime := isPrime }.asIdeal.prod ⊤)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
x : PrimeSpectrum S
⊢ Eq (α := Ideal (R × S))
    (asIdeal
      ((Equiv.symm (primeSpectrumProd R S) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        (Sum.inr x)))
    (Ideal.prod ⊤ x.asIdeal)
have mk : ∀ (asIdeal : Ideal S) (isPrime : asIdeal.IsPrime),
  Eq (α := Ideal (R × S))
    (PrimeSpectrum.asIdeal
      ((Equiv.symm (primeSpectrumProd R S) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        (Sum.inr { asIdeal := asIdeal, isPrime := isPrime })))
    (Ideal.prod ⊤ { asIdeal := asIdeal, isPrime := isPrime }.asIdeal)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
s : Set R
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑(Ideal.span s) : Set R)) (zeroLocus s)
have h : ∀ (x : PrimeSpectrum R),
  Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑(Ideal.span s) : Set R)) x ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus s) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
t : Set (PrimeSpectrum R)
⊢ (↑(vanishingIdeal t) : Set R) = {f : R | ∀ x ∈ t, f ∈ x.asIdeal}
have h : ∀ (f : R), f ∈ (↑(vanishingIdeal t) : Set R) ↔ Membership.mem (γ := Set R) {f : R | ∀ x ∈ t, f ∈ x.asIdeal} f
Tactic: ext f
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
t : Set (PrimeSpectrum R)
f : R
⊢ f ∈ (↑(vanishingIdeal t) : Set R) ↔ Membership.mem (γ := Set R) {f : R | ∀ x ∈ t, f ∈ x.asIdeal} f
have h : (∀ (i : PrimeSpectrum R), Membership.mem (γ := Submodule R R) (⨅ (_ : i ∈ t), i.asIdeal) f) ↔
  Membership.mem (γ := Set R) {f : R | ∀ x ∈ t, f ∈ x.asIdeal} f
Tactic: rw [vanishingIdeal, SetLike.mem_coe, Submodule.mem_iInf]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
t : Set (PrimeSpectrum R)
f : R
⊢ (∀ (i : PrimeSpectrum R), Membership.mem (γ := Submodule R R) (⨅ (_ : i ∈ t), i.asIdeal) f) ↔
    Membership.mem (γ := Set R) {f : R | ∀ x ∈ t, f ∈ x.asIdeal} f
have h : ∀ (a : PrimeSpectrum R), Membership.mem (γ := Submodule R R) (⨅ (_ : a ∈ t), a.asIdeal) f ↔ a ∈ t → f ∈ a.asIdeal
Tactic: apply forall_congr'
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
t : Set (PrimeSpectrum R)
f : R
x : PrimeSpectrum R
⊢ Membership.mem (γ := Submodule R R) (⨅ (_ : x ∈ t), x.asIdeal) f ↔ x ∈ t → f ∈ x.asIdeal
have h : (∀ (i : x ∈ t), f ∈ x.asIdeal) ↔ x ∈ t → f ∈ x.asIdeal
Tactic: rw [Submodule.mem_iInf]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
t : Set (PrimeSpectrum R)
f : R
⊢ f ∈ vanishingIdeal t ↔ ∀ x ∈ t, f ∈ x.asIdeal
have rw : f ∈ (↑(vanishingIdeal t) : Set R) ↔ ∀ x ∈ t, f ∈ x.asIdeal
Tactic: rw [← SetLike.mem_coe, coe_vanishingIdeal, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
t : Set (PrimeSpectrum R)
f : R
rw : f ∈ (↑(vanishingIdeal t) : Set R) ↔ ∀ x ∈ t, f ∈ x.asIdeal
⊢ f ∈ vanishingIdeal t ↔ ∀ x ∈ t, f ∈ x.asIdeal
have rw₁ : Membership.mem (γ := Set R) {f : R | ∀ x ∈ t, f ∈ x.asIdeal} f ↔ ∀ x ∈ t, f ∈ x.asIdeal
Tactic: rw [← SetLike.mem_coe, coe_vanishingIdeal, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
t : Set (PrimeSpectrum R)
f : R
rw : f ∈ (↑(vanishingIdeal t) : Set R) ↔ ∀ x ∈ t, f ∈ x.asIdeal
rw₁ : Membership.mem (γ := Set R) {f : R | ∀ x ∈ t, f ∈ x.asIdeal} f ↔ ∀ x ∈ t, f ∈ x.asIdeal
⊢ f ∈ vanishingIdeal t ↔ ∀ x ∈ t, f ∈ x.asIdeal
have rw₂ : (∀ x ∈ t, f ∈ x.asIdeal) ↔ ∀ x ∈ t, f ∈ x.asIdeal
Tactic: rw [← SetLike.mem_coe, coe_vanishingIdeal, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
⊢ GaloisConnection (fun (s : Set R) ↦ zeroLocus s) fun (t : (Set (PrimeSpectrum R))ᵒᵈ) ↦ (↑(vanishingIdeal t) : Set R)
have ideal_gc : GaloisConnection (β := Ideal R) Ideal.span SetLike.coe
Tactic: have ideal_gc : GaloisConnection Ideal.span _ := (Submodule.gi R R).gc
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f : R
⊢ Membership.mem (γ := Ideal R) (vanishingIdeal (zeroLocus (↑I : Set R))) f ↔ f ∈ I.radical
have rw : (∀ (x : PrimeSpectrum R), Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) x → f ∈ x.asIdeal) ↔
  ∀ (p : Submodule R R), Membership.mem (γ := Set (Submodule R R)) {J : Ideal R | I ≤ J ∧ J.IsPrime} p → f ∈ p
Tactic: rw [mem_vanishingIdeal, Ideal.radical_eq_sInf, Submodule.mem_sInf]