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
S : Type v
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
⊢ IsOpen (X := PrimeSpectrum R) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S)))
have rw : IsOpen (↑(basicOpen r) : Set (PrimeSpectrum R))
Tactic: rw [localization_away_comap_range S r]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
f : R
⊢ IsCompact (↑(basicOpen f) : Set (PrimeSpectrum R))
have rw : IsCompact (X := PrimeSpectrum R)
  (Set.range (ι := PrimeSpectrum (Localization (Submonoid.powers f)))
    (comap (algebraMap R (Localization (Submonoid.powers f)))))
Tactic: rw [← localization_away_comap_range (Localization (Submonoid.powers f))]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_1
f : ι → R
⊢ Eq.{u + 1} (α := Opens (PrimeSpectrum R)) (⨆ (i : ι), basicOpen (f i)) ⊤ ↔
    Eq (α := Ideal R) (Ideal.span (Set.range f)) ⊤
have rw : ⋃ (i : ι), (↑(basicOpen (f i)) : Set (PrimeSpectrum R)) = (↑⊤ : Set (PrimeSpectrum R)) ↔
  Eq (α := Ideal R) (Ideal.span (Set.range f)) ⊤
Tactic: rw [SetLike.ext'_iff, Opens.coe_iSup]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_1
f : ι → R
⊢ ⋃ (i : ι), (↑(basicOpen (f i)) : Set (PrimeSpectrum R)) = (↑⊤ : Set (PrimeSpectrum R)) ↔
    Eq (α := Ideal R) (Ideal.span (Set.range f)) ⊤
have simp : Eq.{u + 1} (α := Set (PrimeSpectrum R)) (zeroLocus (⋃ (i : ι), {f i}))ᶜ Set.univ ↔
  Eq (α := Ideal R) (Ideal.span (Set.range f)) ⊤
Tactic: simp only [PrimeSpectrum.basicOpen_eq_zeroLocus_compl, Opens.coe_top, ← Set.compl_iInter,
    ← PrimeSpectrum.zeroLocus_iUnion]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_1
f : ι → R
⊢ Eq.{u + 1} (α := Set (PrimeSpectrum R)) (zeroLocus (⋃ (i : ι), {f i}))ᶜ Set.univ ↔
    Eq (α := Ideal R) (Ideal.span (Set.range f)) ⊤
have rw : Eq.{u + 1} (α := Set (PrimeSpectrum R)) (zeroLocus (⋃ (i : ι), {f i})) Set.univᶜ ↔
  Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑(Ideal.span (Set.range f)) : Set R)) ∅
Tactic: rw [← PrimeSpectrum.zeroLocus_empty_iff_eq_top, compl_involutive.eq_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
s : Set R
| Eq (α := Ideal R) (Ideal.span s) ⊤
have rw : Eq.{u + 1} (α := TopologicalSpace.Opens (PrimeSpectrum R)) (⨆ (i : { x : R // x ∈ s }), basicOpen (↑i : R)) ⊤
Tactic: rw [← Subtype.range_val (s := s), ← iSup_basicOpen_eq_top_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
s : Set R
⊢ Eq.{u + 1} (α := TopologicalSpace.Opens (PrimeSpectrum R)) (⨆ i ∈ s, basicOpen i) ⊤ ↔
    Eq (α := Ideal R) (Ideal.span s) ⊤
have conv_rhs : Eq.{u + 1} (α := TopologicalSpace.Opens (PrimeSpectrum R)) (⨆ i ∈ s, basicOpen i) ⊤ ↔
  Eq.{u + 1} (α := TopologicalSpace.Opens (PrimeSpectrum R)) (⨆ (i : { x : R // x ∈ s }), basicOpen (↑i : R)) ⊤
Tactic: conv_rhs => rw [← Subtype.range_val (s := s), ← iSup_basicOpen_eq_top_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
inst_2 : Algebra R S
f : R
p : PrimeSpectrum R
h : Eq (α := Set (PrimeSpectrum R)) (TopologicalSpace.Opens.carrier (basicOpen f)) {p}
⊢ IsLocalization.AtPrime (Localization.Away f) p.asIdeal
have refine : ∀ (r : R) (hr : r ∈ p.asIdeal.primeCompl), ∃ (m : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) m ∧ r ∣ m
Tactic: refine .of_le_of_exists_dvd (.powers f) _
      (Submonoid.powers_le.mpr <| by apply h ▸ Set.mem_singleton p) fun r hr ↦ ?_
-- 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
f : R
p : PrimeSpectrum R
h : Eq (α := Set (PrimeSpectrum R)) (TopologicalSpace.Opens.carrier (basicOpen f)) {p}
r : R
hr : r ∈ p.asIdeal.primeCompl
⊢ ∃ (m : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) m ∧ r ∣ m
have contrapose! : ∀ (hr : ∀ (m : R) (_ : Membership.mem (γ := Submonoid R) (Submonoid.powers f) m), ¬r ∣ m), r ∉ p.asIdeal.primeCompl
Tactic: contrapose! hr
Cleared hypotheses: hr
-- 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
f : R
p : PrimeSpectrum R
h : Eq (α := Set (PrimeSpectrum R)) (TopologicalSpace.Opens.carrier (basicOpen f)) {p}
r : R
hr : ∀ (m : R) (_ : Membership.mem (γ := Submonoid R) (Submonoid.powers f) m), ¬r ∣ m
⊢ r ∉ p.asIdeal.primeCompl
have hr₁ : ∀ (m : R) (_ : Membership.mem (γ := Submonoid R) (Submonoid.powers f) m), m ∉ Ideal.span {r}
Tactic: simp_rw [← Ideal.mem_span_singleton] at hr
Cleared hypotheses: hr
-- 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
f : R
p : PrimeSpectrum R
h : Eq (α := Set (PrimeSpectrum R)) (TopologicalSpace.Opens.carrier (basicOpen f)) {p}
r : R
hr : ∀ (m : R) (_ : Membership.mem (γ := Submonoid R) (Submonoid.powers f) m), m ∉ Ideal.span {r}
⊢ r ∉ p.asIdeal.primeCompl
have have : ∀ (q : Ideal R) (prime : q.IsPrime) (le : Ideal.span {r} ≤ q)
  (disj : Disjoint (↑q : Set R) (↑(Submonoid.powers f) : Set R)), r ∉ p.asIdeal.primeCompl
Tactic: have ⟨q, prime, le, disj⟩ := Ideal.exists_le_prime_disjoint (Ideal.span {r})
      (.powers f) (Set.disjoint_right.mpr hr)
-- 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
f : R
p : PrimeSpectrum R
h : Eq (α := Set (PrimeSpectrum R)) (TopologicalSpace.Opens.carrier (basicOpen f)) {p}
r : R
hr : ∀ (m : R) (_ : Membership.mem (γ := Submonoid R) (Submonoid.powers f) m), m ∉ Ideal.span {r}
q : Ideal R
prime : q.IsPrime
le : Ideal.span {r} ≤ q
disj : Disjoint (↑q : Set R) (↑(Submonoid.powers f) : Set R)
⊢ r ∉ p.asIdeal.primeCompl
have this : Membership.mem (γ := Set (PrimeSpectrum R)) (TopologicalSpace.Opens.carrier (basicOpen f))
  { asIdeal := q, isPrime := prime : PrimeSpectrum R }
Tactic: have : ⟨q, prime⟩ ∈ (basicOpen f).1 := Set.disjoint_right.mp disj (Submonoid.mem_powers f)
-- 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
f : R
p : PrimeSpectrum R
h : Eq (α := Set (PrimeSpectrum R)) (TopologicalSpace.Opens.carrier (basicOpen f)) {p}
r : R
hr : ∀ (m : R) (_ : Membership.mem (γ := Submonoid R) (Submonoid.powers f) m), m ∉ Ideal.span {r}
q : Ideal R
prime : q.IsPrime
le : Ideal.span {r} ≤ q
disj : Disjoint (↑q : Set R) (↑(Submonoid.powers f) : Set R)
this :
  Membership.mem (γ := Set (PrimeSpectrum R)) (TopologicalSpace.Opens.carrier (basicOpen f))
    { asIdeal := q, isPrime := prime : PrimeSpectrum R }
⊢ r ∉ p.asIdeal.primeCompl
have this₁ : { asIdeal := q, isPrime := prime : PrimeSpectrum R } = p
Tactic: rw [h, Set.mem_singleton_iff] at this
Cleared hypotheses: this
-- 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
f : R
p : PrimeSpectrum R
h : Eq (α := Set (PrimeSpectrum R)) (TopologicalSpace.Opens.carrier (basicOpen f)) {p}
r : R
hr : ∀ (m : R) (_ : Membership.mem (γ := Submonoid R) (Submonoid.powers f) m), m ∉ Ideal.span {r}
q : Ideal R
prime : q.IsPrime
le : Ideal.span {r} ≤ q
disj : Disjoint (↑q : Set R) (↑(Submonoid.powers f) : Set R)
this : { asIdeal := q, isPrime := prime : PrimeSpectrum R } = p
⊢ r ∉ p.asIdeal.primeCompl
have rw : r ∉ { asIdeal := q, isPrime := prime : PrimeSpectrum R }.asIdeal.primeCompl
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
c : R
this : Algebra R[X] (Away c)[X] := RingHom.toAlgebra (mapRingHom (algebraMap R (Away c)))
⊢ Eq.{u_1 + 1} (α := Set (PrimeSpectrum R[X]))
    (range (ι := PrimeSpectrum (Away c)[X]) (comap (algebraMap R[X] (Away c)[X])))ᶜ
    (range (ι := PrimeSpectrum (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))[X])
      (comap (mapRingHom (Ideal.Quotient.mk (Ideal.span {c})))))
have this₁ : IsLocalization (Submonoid.map (F := R →+* R[X]) C (Submonoid.powers c)) (Away c)[X]
Tactic: have := Polynomial.isLocalization (.powers c) (Away c)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
c : R
this_1 : Algebra R[X] (Away c)[X] := RingHom.toAlgebra (mapRingHom (algebraMap R (Away c)))
this : IsLocalization (Submonoid.map (F := R →+* R[X]) C (Submonoid.powers c)) (Away c)[X]
⊢ Eq.{u_1 + 1} (α := Set (PrimeSpectrum R[X]))
    (range (ι := PrimeSpectrum (Away c)[X]) (comap (algebraMap R[X] (Away c)[X])))ᶜ
    (range (ι := PrimeSpectrum (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))[X])
      (comap (mapRingHom (Ideal.Quotient.mk (Ideal.span {c})))))
have this₁ : IsLocalization (R := R[X]) (Submonoid.powers ((C : (a : R) → R[X]) c) : Submonoid R[X]) (Away c)[X]
Tactic: rw [Submonoid.map_powers] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
c : R
this_1 : Algebra R[X] (Away c)[X] := RingHom.toAlgebra (mapRingHom (algebraMap R (Away c)))
this : IsLocalization (R := R[X]) (Submonoid.powers ((C : (a : R) → R[X]) c) : Submonoid R[X]) (Away c)[X]
⊢ Eq.{u_1 + 1} (α := Set (PrimeSpectrum R[X]))
    (range (ι := PrimeSpectrum (Away c)[X]) (comap (algebraMap R[X] (Away c)[X])))ᶜ
    (range (ι := PrimeSpectrum (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))[X])
      (comap (mapRingHom (Ideal.Quotient.mk (Ideal.span {c})))))
have surj : Function.Surjective (α := R[X]) (β := (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))[X])
  (⇑(mapRingHom (Ideal.Quotient.mk (Ideal.span {c}))) : (a : R[X]) → (R ⧸ Ideal.span {c})[X])
Tactic: have surj : Function.Surjective (mapRingHom (Ideal.Quotient.mk (.span {c}))) :=
    Polynomial.map_surjective _ Ideal.Quotient.mk_surjective
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
this_1 : Algebra R[X] (Away c)[X] := RingHom.toAlgebra (mapRingHom (algebraMap R (Away c)))
this : IsLocalization (R := R[X]) (Submonoid.powers ((C : (a : R) → R[X]) c) : Submonoid R[X]) (Away c)[X]
surj :
  Function.Surjective (α := R[X]) (β := (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))[X])
    (⇑(mapRingHom (Ideal.Quotient.mk (Ideal.span {c}))) : (a : R[X]) → (R ⧸ Ideal.span {c})[X])
⊢ Eq.{u_1 + 1} (α := Set (PrimeSpectrum R[X]))
    (range (ι := PrimeSpectrum (Away c)[X]) (comap (algebraMap R[X] (Away c)[X])))ᶜ
    (range (ι := PrimeSpectrum (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))[X])
      (comap (mapRingHom (Ideal.Quotient.mk (Ideal.span {c})))))
have rw : (↑(basicOpen ((C : (a : R) → R[X]) c) : TopologicalSpace.Opens (PrimeSpectrum R[X])) : Set (PrimeSpectrum R[X]))ᶜ =
  zeroLocus
    (↑(RingHom.ker (F := R[X] →+* (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))[X])
          (mapRingHom (Ideal.Quotient.mk (Ideal.span {c})))) :
      Set R[X])
Tactic: rw [range_comap_of_surjective _ _ surj, localization_away_comap_range _ (C c)]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
inst_1 : DecidableEq ι
i : ι
f : R i
⊢ comap (Pi.evalRingHom R i) '' (↑(basicOpen f) : Set (PrimeSpectrum (R i))) =
    (↑(basicOpen (Pi.single (M := R) i f)) : Set (PrimeSpectrum ((i : ι) → R i)))
have h : ∀ (p : PrimeSpectrum ((i : ι) → R i)),
  Membership.mem (γ := Set (PrimeSpectrum ((i : ι) → R i)))
      (comap (Pi.evalRingHom R i) '' (↑(basicOpen f) : Set (PrimeSpectrum (R i)))) p ↔
    p ∈ (↑(basicOpen (Pi.single (M := R) i f)) : Set (PrimeSpectrum ((i : ι) → R i)))
Tactic: ext p
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
inst_1 : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
⊢ Membership.mem (γ := Set (PrimeSpectrum ((i : ι) → R i)))
      (comap (Pi.evalRingHom R i) '' (↑(basicOpen f) : Set (PrimeSpectrum (R i)))) p ↔
    p ∈ (↑(basicOpen (Pi.single (M := R) i f)) : Set (PrimeSpectrum ((i : ι) → R i)))
have h : Membership.mem (γ := Set (PrimeSpectrum ((i : ι) → R i)))
    (comap (Pi.evalRingHom R i) '' (↑(basicOpen f) : Set (PrimeSpectrum (R i)))) p →
  p ∈ (↑(basicOpen (Pi.single (M := R) i f)) : Set (PrimeSpectrum ((i : ι) → R i)))
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
inst_1 : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
h :
  Membership.mem (γ := Set (PrimeSpectrum ((i : ι) → R i)))
      (comap (Pi.evalRingHom R i) '' (↑(basicOpen f) : Set (PrimeSpectrum (R i)))) p →
    p ∈ (↑(basicOpen (Pi.single (M := R) i f)) : Set (PrimeSpectrum ((i : ι) → R i)))
⊢ Membership.mem (γ := Set (PrimeSpectrum ((i : ι) → R i)))
      (comap (Pi.evalRingHom R i) '' (↑(basicOpen f) : Set (PrimeSpectrum (R i)))) p ↔
    p ∈ (↑(basicOpen (Pi.single (M := R) i f)) : Set (PrimeSpectrum ((i : ι) → R i)))
have h₁ : p ∈ (↑(basicOpen (Pi.single (M := R) i f)) : Set (PrimeSpectrum ((i : ι) → R i))) →
  Membership.mem (γ := Set (PrimeSpectrum ((i : ι) → R i)))
    (comap (Pi.evalRingHom R i) '' (↑(basicOpen f) : Set (PrimeSpectrum (R i)))) p
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
inst_1 : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
hp : p ∈ (↑(basicOpen (Pi.single (M := R) i f)) : Set (PrimeSpectrum ((i : ι) → R i)))
⊢ Membership.mem (γ := Set (PrimeSpectrum ((i : ι) → R i)))
    (Set.range (ι := PrimeSpectrum (R i)) (comap (Pi.evalRingHom R i))) p
have rw : RingHom.ker (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) ≤ p.asIdeal
Tactic: rw [range_comap_of_surjective _ _ (RingHom.surjective _), mem_zeroLocus,
        SetLike.coe_subset_coe]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (hypothesis)
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
inst_1 : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
hp : p ∈ (↑(basicOpen (Pi.single (M := R) i f)) : Set (PrimeSpectrum ((i : ι) → R i)))
x : (i : ι) → R i
hx :
  Membership.mem (γ := Submodule ((i : ι) → R i) ((i : ι) → R i))
    (RingHom.ker (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i : ((i : ι) → R i) →+* R i)) x
⊢ x ∈ p.asIdeal
have hx₁ : x i = 0
Tactic: rw [RingHom.mem_ker, Pi.evalRingHom_apply] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
inst_1 : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
hp : p ∈ (↑(basicOpen (Pi.single (M := R) i f)) : Set (PrimeSpectrum ((i : ι) → R i)))
x : (i : ι) → R i
hx : x i = 0
⊢ Pi.single (M := R) i f * x = 0
have h : ∀ (j : ι), (Pi.single (M := R) i f * x) j = 0 j
Tactic: ext j
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
inst_1 : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
hp : p ∈ (↑(basicOpen (Pi.single (M := R) i f)) : Set (PrimeSpectrum ((i : ι) → R i)))
x : (i : ι) → R i
hx : x i = 0
j : ι
⊢ (Pi.single (M := R) i f * x) j = 0 j
have pos : ∀ (h : i = j), (Pi.single (M := R) i f * x) j = 0 j
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
inst_1 : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
hp : p ∈ (↑(basicOpen (Pi.single (M := R) i f)) : Set (PrimeSpectrum ((i : ι) → R i)))
x : (i : ι) → R i
hx : x i = 0
j : ι
pos : ∀ (h : i = j), (Pi.single (M := R) i f * x) j = 0 j
⊢ (Pi.single (M := R) i f * x) j = 0 j
have neg : ∀ (h : ¬i = j), (Pi.single (M := R) i f * x) j = 0 j
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
inst_1 : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
hp : p ∈ (↑(basicOpen (Pi.single (M := R) i f)) : Set (PrimeSpectrum ((i : ι) → R i)))
x : (i : ι) → R i
hx : x i = 0
j : ι
h : i = j
⊢ (Pi.single (M := R) i f * x) j = 0 j
have pos : (Pi.single (M := R) i f * x) i = 0 i
Tactic: subst h
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (hypothesis)
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
inst_1 : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
hp : p ∈ (↑(basicOpen (Pi.single (M := R) i f)) : Set (PrimeSpectrum ((i : ι) → R i)))
x : (i : ι) → R i
hx : x i = 0
⊢ x ∈ p.asIdeal
have this : Pi.single (M := R) i f * x = 0
Tactic: have : Pi.single i f * x = 0 := by
        ext j
        by_cases h : i = j
        · subst h
          simp [hx]
        · simp [h]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
inst_1 : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
hp : p ∈ (↑(basicOpen (Pi.single (M := R) i f)) : Set (PrimeSpectrum ((i : ι) → R i)))
x : (i : ι) → R i
hx : x i = 0
this : Pi.single (M := R) i f * x = 0
⊢ x ∈ p.asIdeal
have inl : ∀ (h : Pi.single (M := R) i f ∈ p.asIdeal), x ∈ p.asIdeal
Tactic: obtain (h | h) := Ideal.IsPrime.mem_or_mem_of_mul_eq_zero p.isPrime this
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
inst_1 : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
hp : p ∈ (↑(basicOpen (Pi.single (M := R) i f)) : Set (PrimeSpectrum ((i : ι) → R i)))
x : (i : ι) → R i
hx : x i = 0
this : Pi.single (M := R) i f * x = 0
inl : ∀ (h : Pi.single (M := R) i f ∈ p.asIdeal), x ∈ p.asIdeal
⊢ x ∈ p.asIdeal
have inr : ∀ (h : x ∈ p.asIdeal), x ∈ p.asIdeal
Tactic: obtain (h | h) := Ideal.IsPrime.mem_or_mem_of_mul_eq_zero p.isPrime this
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (hypothesis)
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
inst_1 : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
hp : p ∈ (↑(basicOpen (Pi.single (M := R) i f)) : Set (PrimeSpectrum ((i : ι) → R i)))
⊢ Membership.mem (γ := Set (PrimeSpectrum ((i : ι) → R i)))
    (comap (Pi.evalRingHom R i) '' (↑(basicOpen f) : Set (PrimeSpectrum (R i)))) p
have this : Membership.mem (γ := Set (PrimeSpectrum ((i : ι) → R i)))
  (Set.range (ι := PrimeSpectrum (R i)) (comap (Pi.evalRingHom R i))) p
Tactic: have : p ∈ Set.range (PrimeSpectrum.comap (Pi.evalRingHom R i)) := by
      rw [range_comap_of_surjective _ _ (RingHom.surjective _), mem_zeroLocus,
        SetLike.coe_subset_coe]
      intro x hx
      rw [RingHom.mem_ker, Pi.evalRingHom_apply] at hx
      have : Pi.single i f * x = 0 := by
        ext j
        by_cases h : i = j
        · subst h
          simp [hx]
        · simp [h]
      obtain (h | h) := Ideal.IsPrime.mem_or_mem_of_mul_eq_zero p.isPrime this <;> tauto
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
inst_1 : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
hp : p ∈ (↑(basicOpen (Pi.single (M := R) i f)) : Set (PrimeSpectrum ((i : ι) → R i)))
this :
  Membership.mem (γ := Set (PrimeSpectrum ((i : ι) → R i)))
    (Set.range (ι := PrimeSpectrum (R i)) (comap (Pi.evalRingHom R i))) p
⊢ Membership.mem (γ := Set (PrimeSpectrum ((i : ι) → R i)))
    (comap (Pi.evalRingHom R i) '' (↑(basicOpen f) : Set (PrimeSpectrum (R i)))) p
have h : ∀ (q : PrimeSpectrum (R i))
  (hp : comap (Pi.evalRingHom R i) q ∈ (↑(basicOpen (Pi.single (M := R) i f)) : Set (PrimeSpectrum ((i : ι) → R i)))),
  Membership.mem (γ := Set (PrimeSpectrum ((i : ι) → R i)))
    (comap (Pi.evalRingHom R i) '' (↑(basicOpen f) : Set (PrimeSpectrum (R i)))) (comap (Pi.evalRingHom R i) q)
Tactic: obtain ⟨q, rfl⟩ := this
Cleared hypotheses: p, hp, this
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
inst_1 : DecidableEq ι
i : ι
f : R i
q : PrimeSpectrum (R i)
hp : comap (Pi.evalRingHom R i) q ∈ (↑(basicOpen (Pi.single (M := R) i f)) : Set (PrimeSpectrum ((i : ι) → R i)))
⊢ Eq (α := PrimeSpectrum ((i : ι) → R i)) (comap (Pi.evalRingHom R i) q) (comap (Pi.evalRingHom R i) q)
have asIdeal : ∀ (x : (i : ι) → R i),
  Membership.mem (γ := Ideal ((i : ι) → R i)) (asIdeal (comap (Pi.evalRingHom R i) q)) x ↔
    Membership.mem (γ := Ideal ((i : ι) → R i)) (asIdeal (comap (Pi.evalRingHom R i) q)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
inst_1 : DecidableEq ι
i : ι
f : R i
⊢ sigmaToPi R '' Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i '' (↑(basicOpen f) : Set (PrimeSpectrum (R i))) =
    (↑(basicOpen (Pi.single (M := R) i f)) : Set (PrimeSpectrum ((i : ι) → R i)))
have simp : (fun (a : PrimeSpectrum (R i)) ↦ comap (Pi.evalRingHom R i) a) '' (↑(basicOpen f) : Set (PrimeSpectrum (R i))) =
  (↑(basicOpen (Pi.single (M := R) i f)) : Set (PrimeSpectrum ((i : ι) → R i)))
Tactic: simp only [Set.image_image, sigmaToPi_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
⊢ IsOpenEmbedding (X := (i : ι) × PrimeSpectrum (R i)) (sigmaToPi R)
have refine_1 : Continuous (X := (i : ι) × PrimeSpectrum (R i)) (sigmaToPi R)
Tactic: refine .of_continuous_injective_isOpenMap ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
refine_1 : Continuous (X := (i : ι) × PrimeSpectrum (R i)) (sigmaToPi R)
⊢ IsOpenEmbedding (X := (i : ι) × PrimeSpectrum (R i)) (sigmaToPi R)
have refine_2 : Function.Injective (α := (i : ι) × PrimeSpectrum (R i)) (sigmaToPi R)
Tactic: refine .of_continuous_injective_isOpenMap ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
refine_1 : Continuous (X := (i : ι) × PrimeSpectrum (R i)) (sigmaToPi R)
refine_2 : Function.Injective (α := (i : ι) × PrimeSpectrum (R i)) (sigmaToPi R)
⊢ IsOpenEmbedding (X := (i : ι) × PrimeSpectrum (R i)) (sigmaToPi R)
have refine_3 : IsOpenMap (X := (i : ι) × PrimeSpectrum (R i)) (sigmaToPi R)
Tactic: refine .of_continuous_injective_isOpenMap ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
⊢ Continuous (X := (i : ι) × PrimeSpectrum (R i)) (sigmaToPi R)
have refine_1 : ∀ (i : ι),
  Continuous (Y := PrimeSpectrum ((i : ι) → R i)) fun (a : PrimeSpectrum (R i)) ↦
    sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i a)
Tactic: rw [continuous_sigma_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
⊢ IsOpenMap (X := (i : ι) × PrimeSpectrum (R i)) (sigmaToPi R)
have refine_3 : ∀ (i : ι),
  IsOpenMap (Y := PrimeSpectrum ((i : ι) → R i)) fun (a : PrimeSpectrum (R i)) ↦
    sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i a)
Tactic: rw [isOpenMap_sigma]