awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
h :
  Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal} ∧
    LE.le (α := Ideal R) (sInf {I : Ideal R | I.IsMaximal}) (nilradical R)
fin : Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I : Ideal R
hI : I.IsPrime
le : ∃ i ∈ fin.toFinset (s := {I : Ideal R | I.IsMaximal}), id i ≤ I
M : Ideal R
hM : Membership.mem (γ := Set (Ideal R)) {I : Ideal R | I.IsMaximal} M
hMI : id M ≤ I
⊢ I.IsMaximal
have rwa : M.IsMaximal
Tactic: rwa [← hM.eq_of_le hI.1 hMI]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
h :
  Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal} ∧
    LE.le (α := Ideal R) (sInf {I : Ideal R | I.IsMaximal}) (nilradical R)
fin : Set.Finite.{u} (α := Ideal R) {I : Ideal R | I.IsMaximal}
le : LE.le (α := Ideal R) (sInf {I : Ideal R | I.IsMaximal}) (nilradical R)
⊢ Set.Finite.{u} (α := Ideal R) {x : Ideal R | x.IsPrime} ∧ ∀ (I : Ideal R), I.IsPrime → I.IsMaximal
have hpm : ∀ (I : Ideal R) (hI : I.IsPrime), I.IsMaximal
Tactic: have hpm (I : Ideal R) (hI : I.IsPrime) : I.IsMaximal := by
    replace le := le.trans (nilradical_le_prime I)
    rw [← fin.coe_toFinset, ← Finset.inf_id_eq_sInf, hI.inf_le'] at le
    have ⟨M, hM, hMI⟩ := le
    rw [fin.mem_toFinset] at hM
    rwa [← hM.eq_of_le hI.1 hMI]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
⊢ Continuous (comap f)
have simp : ∀ (s : Set (PrimeSpectrum R)), (∃ (s_1 : Set R), s = zeroLocus s_1) → ∃ (s_1 : Set S), comap f ⁻¹' s = zeroLocus s_1
Tactic: simp only [continuous_iff_isClosed, isClosed_iff_zeroLocus]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
p q : PrimeSpectrum S
h : Eq (α := PrimeSpectrum R) (comap (algebraMap R S) p) (comap (algebraMap R S) q)
⊢ p = q
have h₁ : Eq.{v + 1} (α := Ideal S)
  ((fun (x : PrimeSpectrum R) ↦ (Ideal.map (F := R →+* S) (algebraMap R S) x.asIdeal : Ideal S))
    (comap (algebraMap R S) p))
  ((fun (x : PrimeSpectrum R) ↦ (Ideal.map (F := R →+* S) (algebraMap R S) x.asIdeal : Ideal S))
    (comap (algebraMap R S) q))
Tactic: replace h := _root_.congr_arg (fun x : PrimeSpectrum R => Ideal.map (algebraMap R S) x.asIdeal) h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
p q : PrimeSpectrum S
h :
  Eq.{v + 1} (α := Ideal S)
    (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.comap (F := R →+* S) (algebraMap R S) p.asIdeal))
    (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.comap (F := R →+* S) (algebraMap R S) q.asIdeal))
⊢ p = q
have h₁ : p.asIdeal = q.asIdeal
Tactic: rw [IsLocalization.map_under M S, IsLocalization.map_under M S] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
⊢ Eq (α := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S)))
    {p : PrimeSpectrum R | Disjoint (↑M : Set R) (↑p.asIdeal : Set R)}
have refine_1 : ∀ (x : PrimeSpectrum R),
  Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S))) x →
    Membership.mem (γ := Set (PrimeSpectrum R)) {p : PrimeSpectrum R | Disjoint (↑M : Set R) (↑p.asIdeal : Set R)} x
Tactic: refine Set.ext fun x ↦ ⟨?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
refine_1 :
  ∀ (x : PrimeSpectrum R),
    Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S))) x →
      Membership.mem (γ := Set (PrimeSpectrum R)) {p : PrimeSpectrum R | Disjoint (↑M : Set R) (↑p.asIdeal : Set R)} x
⊢ Eq (α := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S)))
    {p : PrimeSpectrum R | Disjoint (↑M : Set R) (↑p.asIdeal : Set R)}
have refine_2 : ∀ (x : PrimeSpectrum R)
  (h :
    Membership.mem (γ := Set (PrimeSpectrum R)) {p : PrimeSpectrum R | Disjoint (↑M : Set R) (↑p.asIdeal : Set R)} x),
  Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S))) x
Tactic: refine Set.ext fun x ↦ ⟨?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
x : PrimeSpectrum R
h : Membership.mem (γ := Set (PrimeSpectrum R)) {p : PrimeSpectrum R | Disjoint (↑M : Set R) (↑p.asIdeal : Set R)} x
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S))) x
have h₁ : comap (algebraMap R S) { asIdeal := Ideal.map (F := R →+* S) (algebraMap R S) x.asIdeal, isPrime := sorry } = x
Tactic: use ⟨x.asIdeal.map (algebraMap R S), IsLocalization.isPrime_of_isPrime_disjoint M S _ x.2 h⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
x : PrimeSpectrum R
h : Membership.mem (γ := Set (PrimeSpectrum R)) {p : PrimeSpectrum R | Disjoint (↑M : Set R) (↑p.asIdeal : Set R)} x
⊢ comap (algebraMap R S) { asIdeal := Ideal.map (F := R →+* S) (algebraMap R S) x.asIdeal, isPrime := ⋯ } = x
have h₁ : asIdeal (comap (algebraMap R S) { asIdeal := Ideal.map (F := R →+* S) (algebraMap R S) x.asIdeal, isPrime := sorry }) =
  x.asIdeal
Tactic: ext1
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
⊢ IsInducing (X := PrimeSpectrum S) (Y := PrimeSpectrum R) (comap (algebraMap R S))
have refine : ∀ (Z : Set (PrimeSpectrum S)),
  IsClosed Z ↔ IsClosed[TopologicalSpace.induced (comap (algebraMap R S)) zariskiTopology] Z
Tactic: refine ⟨TopologicalSpace.ext_isClosed fun Z ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
Z : Set (PrimeSpectrum S)
⊢ IsClosed Z ↔ IsClosed[TopologicalSpace.induced (comap (algebraMap R S)) zariskiTopology] Z
have simp_rw : (∃ (s : Set S), zeroLocus s = Z) ↔ ∃ (a : Set R), zeroLocus ((⇑(algebraMap R S) : (a : R) → S) '' a) = Z
Tactic: simp_rw [isClosed_induced_iff, isClosed_iff_zeroLocus, @eq_comm _ _ (zeroLocus _),
    exists_exists_eq_and, preimage_comap_zeroLocus]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
Z : Set (PrimeSpectrum S)
⊢ (∃ (s : Set S), zeroLocus s = Z) ↔ ∃ (a : Set R), zeroLocus ((⇑(algebraMap R S) : (a : R) → S) '' a) = Z
have mp : (∃ (s : Set S), zeroLocus s = Z) → ∃ (a : Set R), zeroLocus ((⇑(algebraMap R S) : (a : R) → S) '' a) = Z
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
Z : Set (PrimeSpectrum S)
mp : (∃ (s : Set S), zeroLocus s = Z) → ∃ (a : Set R), zeroLocus ((⇑(algebraMap R S) : (a : R) → S) '' a) = Z
⊢ (∃ (s : Set S), zeroLocus s = Z) ↔ ∃ (a : Set R), zeroLocus ((⇑(algebraMap R S) : (a : R) → S) '' a) = Z
have mpr : (∃ (a : Set R), zeroLocus ((⇑(algebraMap R S) : (a : R) → S) '' a) = Z) → ∃ (s : Set S), zeroLocus s = Z
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
s : Set S
⊢ ∃ (a : Set R), Eq (α := Set (PrimeSpectrum S)) (zeroLocus ((⇑(algebraMap R S) : (a : R) → S) '' a)) (zeroLocus s)
have mp : Eq (α := Set (PrimeSpectrum S))
  (zeroLocus
    ((⇑(algebraMap R S) : (a : R) → S) '' (↑(Ideal.comap (F := R →+* S) (algebraMap R S) (Ideal.span s)) : Set R)))
  (zeroLocus s)
Tactic: refine ⟨(Ideal.span s).comap (algebraMap R S), ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
s : Set S
⊢ Eq (α := Set (PrimeSpectrum S))
    (zeroLocus
      ((⇑(algebraMap R S) : (a : R) → S) '' (↑(Ideal.comap (F := R →+* S) (algebraMap R S) (Ideal.span s)) : Set R)))
    (zeroLocus s)
have mp : Eq (α := Set (PrimeSpectrum S))
  (zeroLocus
    (↑(Ideal.span
          ((⇑(algebraMap R S) : (a : R) → S) ''
            (↑(Ideal.comap (F := R →+* S) (algebraMap R S) (Ideal.span s)) : Set R))) :
      Set S))
  (zeroLocus s)
Tactic: rw [← zeroLocus_span, ← zeroLocus_span s, ← Ideal.map, IsLocalization.map_under M S]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
s : Set S
mp :
  Eq (α := Set (PrimeSpectrum S))
    (zeroLocus
      (↑(Ideal.span
            ((⇑(algebraMap R S) : (a : R) → S) ''
              (↑(Ideal.comap (F := R →+* S) (algebraMap R S) (Ideal.span s)) : Set R))) :
        Set S))
    (zeroLocus s)
⊢ Eq (α := Set (PrimeSpectrum S))
    (zeroLocus
      ((⇑(algebraMap R S) : (a : R) → S) '' (↑(Ideal.comap (F := R →+* S) (algebraMap R S) (Ideal.span s)) : Set R)))
    (zeroLocus s)
have mp₁ : Eq (α := Set (PrimeSpectrum S))
  (zeroLocus
    (↑(Ideal.span
          ((⇑(algebraMap R S) : (a : R) → S) ''
            (↑(Ideal.comap (F := R →+* S) (algebraMap R S) (Ideal.span s)) : Set R))) :
      Set S))
  (zeroLocus (↑(Ideal.span s) : Set S))
Tactic: rw [← zeroLocus_span, ← zeroLocus_span s, ← Ideal.map, IsLocalization.map_under M S]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
s : Set S
mp :
  Eq (α := Set (PrimeSpectrum S))
    (zeroLocus
      (↑(Ideal.span
            ((⇑(algebraMap R S) : (a : R) → S) ''
              (↑(Ideal.comap (F := R →+* S) (algebraMap R S) (Ideal.span s)) : Set R))) :
        Set S))
    (zeroLocus s)
mp₁ :
  Eq (α := Set (PrimeSpectrum S))
    (zeroLocus
      (↑(Ideal.span
            ((⇑(algebraMap R S) : (a : R) → S) ''
              (↑(Ideal.comap (F := R →+* S) (algebraMap R S) (Ideal.span s)) : Set R))) :
        Set S))
    (zeroLocus (↑(Ideal.span s) : Set S))
⊢ Eq (α := Set (PrimeSpectrum S))
    (zeroLocus
      ((⇑(algebraMap R S) : (a : R) → S) '' (↑(Ideal.comap (F := R →+* S) (algebraMap R S) (Ideal.span s)) : Set R)))
    (zeroLocus s)
have mp₂ : Eq (α := Set (PrimeSpectrum S))
  (zeroLocus
    (↑(Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.comap (F := R →+* S) (algebraMap R S) (Ideal.span s))) : Set S))
  (zeroLocus (↑(Ideal.span s) : Set S))
Tactic: rw [← zeroLocus_span, ← zeroLocus_span s, ← Ideal.map, IsLocalization.map_under M S]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
s : Set S
mp :
  Eq (α := Set (PrimeSpectrum S))
    (zeroLocus
      (↑(Ideal.span
            ((⇑(algebraMap R S) : (a : R) → S) ''
              (↑(Ideal.comap (F := R →+* S) (algebraMap R S) (Ideal.span s)) : Set R))) :
        Set S))
    (zeroLocus s)
mp₁ :
  Eq (α := Set (PrimeSpectrum S))
    (zeroLocus
      (↑(Ideal.span
            ((⇑(algebraMap R S) : (a : R) → S) ''
              (↑(Ideal.comap (F := R →+* S) (algebraMap R S) (Ideal.span s)) : Set R))) :
        Set S))
    (zeroLocus (↑(Ideal.span s) : Set S))
mp₂ :
  Eq (α := Set (PrimeSpectrum S))
    (zeroLocus
      (↑(Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.comap (F := R →+* S) (algebraMap R S) (Ideal.span s))) :
        Set S))
    (zeroLocus (↑(Ideal.span s) : Set S))
⊢ Eq (α := Set (PrimeSpectrum S))
    (zeroLocus
      ((⇑(algebraMap R S) : (a : R) → S) '' (↑(Ideal.comap (F := R →+* S) (algebraMap R S) (Ideal.span s)) : Set R)))
    (zeroLocus s)
have mp₃ : Eq (α := Set (PrimeSpectrum S)) (zeroLocus (↑(Ideal.span s) : Set S)) (zeroLocus (↑(Ideal.span s) : Set S))
Tactic: rw [← zeroLocus_span, ← zeroLocus_span s, ← Ideal.map, IsLocalization.map_under M S]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
hf : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ zariskiTopology = TopologicalSpace.induced (comap f) zariskiTopology
have simp : ∀ (s : Set (PrimeSpectrum S)),
  (∃ (s_1 : Set S), sᶜ = zeroLocus s_1) ↔
    ∃ (t : Set (PrimeSpectrum R)), (∃ (s : Set R), t = zeroLocus s) ∧ comap f ⁻¹' t = sᶜ
Tactic: simp only [TopologicalSpace.ext_iff, ← isClosed_compl_iff, isClosed_iff_zeroLocus,
      isClosed_induced_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
hf : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
s : Set (PrimeSpectrum S)
h : ∃ (s_1 : Set S), sᶜ = zeroLocus s_1
F : Set S
hF : sᶜ = zeroLocus F
⊢ comap f ⁻¹' zeroLocus ((⇑f : (a : R) → S) ⁻¹' F) = sᶜ
have rw : zeroLocus (Set.image.{u, v} (α := R) (⇑f : (a : R) → S) ((⇑f : (a : R) → S) ⁻¹' F)) = sᶜ
Tactic: rw [preimage_comap_zeroLocus, Function.Surjective.image_preimage hf, hF]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
hf : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
s : Set (PrimeSpectrum S)
h : ∃ (s_1 : Set S), sᶜ = zeroLocus s_1
F : Set S
hF : sᶜ = zeroLocus F
rw : zeroLocus (Set.image.{u, v} (α := R) (⇑f : (a : R) → S) ((⇑f : (a : R) → S) ⁻¹' F)) = sᶜ
⊢ comap f ⁻¹' zeroLocus ((⇑f : (a : R) → S) ⁻¹' F) = sᶜ
have rw₁ : zeroLocus F = sᶜ
Tactic: rw [preimage_comap_zeroLocus, Function.Surjective.image_preimage hf, hF]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
hf : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
s : Set (PrimeSpectrum S)
h : ∃ (s_1 : Set S), sᶜ = zeroLocus s_1
F : Set S
hF : sᶜ = zeroLocus F
rw : zeroLocus (Set.image.{u, v} (α := R) (⇑f : (a : R) → S) ((⇑f : (a : R) → S) ⁻¹' F)) = sᶜ
rw₁ : zeroLocus F = sᶜ
⊢ comap f ⁻¹' zeroLocus ((⇑f : (a : R) → S) ⁻¹' F) = sᶜ
have rw₂ : Eq (α := Set (PrimeSpectrum S)) (zeroLocus F) (zeroLocus F)
Tactic: rw [preimage_comap_zeroLocus, Function.Surjective.image_preimage hf, hF]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
hf : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ ∀ (s : Set (PrimeSpectrum S)),
    (∃ (s_1 : Set S), sᶜ = zeroLocus s_1) ↔
      ∃ (t : Set (PrimeSpectrum R)), (∃ (s : Set R), t = zeroLocus s) ∧ comap f ⁻¹' t = sᶜ
have refine : ∀ (s : Set (PrimeSpectrum S)),
  (∃ (t : Set (PrimeSpectrum R)), (∃ (s : Set R), t = zeroLocus s) ∧ comap f ⁻¹' t = sᶜ) →
    ∃ (s_1 : Set S), sᶜ = zeroLocus s_1
Tactic: refine fun s =>
      ⟨fun ⟨F, hF⟩ =>
        ⟨zeroLocus (f ⁻¹' F), ⟨f ⁻¹' F, rfl⟩, by
          rw [preimage_comap_zeroLocus, Function.Surjective.image_preimage hf, hF]⟩,
        ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hle : I ≤ nilradical R
⊢ Bijective.{u + 1, u + 1} (α := PrimeSpectrum (R ⧸ I)) (β := PrimeSpectrum R) (comap (Ideal.Quotient.mk I))
have refine : Surjective.{u + 1, u + 1} (α := PrimeSpectrum (R ⧸ I)) (β := PrimeSpectrum R) (comap (Ideal.Quotient.mk I))
Tactic: refine ⟨comap_injective_of_surjective _ Ideal.Quotient.mk_surjective, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ IsClosed (Set.range (comap f))
have rw : IsClosed (X := PrimeSpectrum R) (zeroLocus (↑(ker f) : Set R))
Tactic: rw [range_comap_of_surjective _ f hf]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
x : PrimeSpectrum R
⊢ Eq (α := PrimeSpectrum (R × S))
    ((Equiv.symm (primeSpectrumProd R S) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        (Sum.inl x) :
      PrimeSpectrum (R × S))
    (comap (RingHom.fst R S) x : PrimeSpectrum (R × S))
have asIdeal : ∀ (x_1 : R × S),
  Membership.mem (γ := Ideal (R × S))
      (asIdeal
        ((Equiv.symm (primeSpectrumProd R S) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
          (Sum.inl x)))
      x_1 ↔
    Membership.mem (γ := Ideal (R × S)) (asIdeal (comap (RingHom.fst R S) x)) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
x : PrimeSpectrum S
⊢ Eq (α := PrimeSpectrum (R × S))
    ((Equiv.symm (primeSpectrumProd R S) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        (Sum.inr x) :
      PrimeSpectrum (R × S))
    (comap (RingHom.snd R S) x : PrimeSpectrum (R × S))
have asIdeal : ∀ (x_1 : R × S),
  Membership.mem (γ := Ideal (R × S))
      (asIdeal
        ((Equiv.symm (primeSpectrumProd R S) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
          (Sum.inr x)))
      x_1 ↔
    Membership.mem (γ := Ideal (R × S)) (asIdeal (comap (RingHom.snd R S) x)) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
⊢ Eq (α := Set (PrimeSpectrum (R × S))) (Set.range (ι := PrimeSpectrum R) (comap (RingHom.fst R S)))
    (zeroLocus (↑(RingHom.ker (F := R × S →+* R) (RingHom.fst R S)) : Set (R × S)))
have refine_1 : ∀ (p : PrimeSpectrum (R × S)),
  Membership.mem (γ := Set (PrimeSpectrum (R × S))) (Set.range (ι := PrimeSpectrum R) (comap (RingHom.fst R S))) p →
    Membership.mem (γ := Set (PrimeSpectrum (R × S)))
      (zeroLocus (↑(RingHom.ker (F := R × S →+* R) (RingHom.fst R S)) : Set (R × S))) p
Tactic: refine Set.ext fun p ↦ ⟨?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
refine_1 :
  ∀ (p : PrimeSpectrum (R × S)),
    Membership.mem (γ := Set (PrimeSpectrum (R × S))) (Set.range (ι := PrimeSpectrum R) (comap (RingHom.fst R S))) p →
      Membership.mem (γ := Set (PrimeSpectrum (R × S)))
        (zeroLocus (↑(RingHom.ker (F := R × S →+* R) (RingHom.fst R S)) : Set (R × S))) p
⊢ Eq (α := Set (PrimeSpectrum (R × S))) (Set.range (ι := PrimeSpectrum R) (comap (RingHom.fst R S)))
    (zeroLocus (↑(RingHom.ker (F := R × S →+* R) (RingHom.fst R S)) : Set (R × S)))
have refine_2 : ∀ (p : PrimeSpectrum (R × S))
  (h :
    Membership.mem (γ := Set (PrimeSpectrum (R × S)))
      (zeroLocus (↑(RingHom.ker (F := R × S →+* R) (RingHom.fst R S)) : Set (R × S))) p),
  Membership.mem (γ := Set (PrimeSpectrum (R × S))) (Set.range (ι := PrimeSpectrum R) (comap (RingHom.fst R S))) p
Tactic: refine Set.ext fun p ↦ ⟨?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
p : PrimeSpectrum (R × S)
h :
  Membership.mem (γ := Set (PrimeSpectrum (R × S)))
    (zeroLocus (↑(RingHom.ker (F := R × S →+* R) (RingHom.fst R S)) : Set (R × S))) p
⊢ Membership.mem (γ := Set (PrimeSpectrum (R × S))) (Set.range (ι := PrimeSpectrum R) (comap (RingHom.fst R S))) p
have refine_2 : ∀ (p_1 : Ideal R) (hp : p_1.IsPrime) (eq : p.asIdeal = p_1.prod ⊤),
  Membership.mem (γ := Set (PrimeSpectrum (R × S))) (Set.range (ι := PrimeSpectrum R) (comap (RingHom.fst R S))) p
Tactic: obtain ⟨p, hp, eq⟩ | ⟨p, hp, eq⟩ := p.1.ideal_prod_prime.mp p.2
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
p : PrimeSpectrum (R × S)
h :
  Membership.mem (γ := Set (PrimeSpectrum (R × S)))
    (zeroLocus (↑(RingHom.ker (F := R × S →+* R) (RingHom.fst R S)) : Set (R × S))) p
refine_2 :
  ∀ (p_1 : Ideal R) (hp : p_1.IsPrime) (eq : p.asIdeal = p_1.prod ⊤),
    Membership.mem (γ := Set (PrimeSpectrum (R × S))) (Set.range (ι := PrimeSpectrum R) (comap (RingHom.fst R S))) p
⊢ Membership.mem (γ := Set (PrimeSpectrum (R × S))) (Set.range (ι := PrimeSpectrum R) (comap (RingHom.fst R S))) p
have refine_2₁ : ∀ (p_1 : Ideal S) (hp : p_1.IsPrime) (eq : p.asIdeal = Ideal.prod ⊤ p_1),
  Membership.mem (γ := Set (PrimeSpectrum (R × S))) (Set.range (ι := PrimeSpectrum R) (comap (RingHom.fst R S))) p
Tactic: obtain ⟨p, hp, eq⟩ | ⟨p, hp, eq⟩ := p.1.ideal_prod_prime.mp p.2
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
p_1 : PrimeSpectrum (R × S)
h :
  Membership.mem (γ := Set (PrimeSpectrum (R × S)))
    (zeroLocus (↑(RingHom.ker (F := R × S →+* R) (RingHom.fst R S)) : Set (R × S))) p_1
p : Ideal S
hp : p.IsPrime
eq : p_1.asIdeal = Ideal.prod ⊤ p
⊢ Membership.mem (γ := Set (PrimeSpectrum (R × S))) (Set.range (ι := PrimeSpectrum R) (comap (RingHom.fst R S))) p_1
have refine_2 : 1 ∈ p
Tactic: refine (hp.ne_top <| (Ideal.eq_top_iff_one _).mpr ?_).elim
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
⊢ Eq (α := Set (PrimeSpectrum (R × S))) (Set.range (ι := PrimeSpectrum S) (comap (RingHom.snd R S)))
    (zeroLocus (↑(RingHom.ker (F := R × S →+* S) (RingHom.snd R S)) : Set (R × S)))
have refine_1 : ∀ (p : PrimeSpectrum (R × S)),
  Membership.mem (γ := Set (PrimeSpectrum (R × S))) (Set.range (ι := PrimeSpectrum S) (comap (RingHom.snd R S))) p →
    Membership.mem (γ := Set (PrimeSpectrum (R × S)))
      (zeroLocus (↑(RingHom.ker (F := R × S →+* S) (RingHom.snd R S)) : Set (R × S))) p
Tactic: refine Set.ext fun p ↦ ⟨?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
refine_1 :
  ∀ (p : PrimeSpectrum (R × S)),
    Membership.mem (γ := Set (PrimeSpectrum (R × S))) (Set.range (ι := PrimeSpectrum S) (comap (RingHom.snd R S))) p →
      Membership.mem (γ := Set (PrimeSpectrum (R × S)))
        (zeroLocus (↑(RingHom.ker (F := R × S →+* S) (RingHom.snd R S)) : Set (R × S))) p
⊢ Eq (α := Set (PrimeSpectrum (R × S))) (Set.range (ι := PrimeSpectrum S) (comap (RingHom.snd R S)))
    (zeroLocus (↑(RingHom.ker (F := R × S →+* S) (RingHom.snd R S)) : Set (R × S)))
have refine_2 : ∀ (p : PrimeSpectrum (R × S))
  (h :
    Membership.mem (γ := Set (PrimeSpectrum (R × S)))
      (zeroLocus (↑(RingHom.ker (F := R × S →+* S) (RingHom.snd R S)) : Set (R × S))) p),
  Membership.mem (γ := Set (PrimeSpectrum (R × S))) (Set.range (ι := PrimeSpectrum S) (comap (RingHom.snd R S))) p
Tactic: refine Set.ext fun p ↦ ⟨?_, fun h ↦ ?_⟩