awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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
⊢ ∀ (m : R) (_ : Membership.mem (γ := Submonoid R) (Submonoid.powers f) m), m ∉ Ideal.span {r}

Tactic:
simp_rw [← Ideal.mem_span_singleton] at hr

Premises used: Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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}
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
⊢ 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)
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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)
⊢ 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)
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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 }
⊢ { asIdeal := q, isPrime := prime : PrimeSpectrum R } = p

Tactic:
rw [h, Set.mem_singleton_iff] at this

Premises used: Set.mem_singleton_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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
rw : r ∉ { asIdeal := q, isPrime := prime : PrimeSpectrum R }.asIdeal.primeCompl
⊢ r ∉ p.asIdeal.primeCompl

Tactic:
rw [← this]
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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 ∉ { asIdeal := q, isPrime := prime : PrimeSpectrum R }.asIdeal.primeCompl

Tactic:
not_not.mpr (q.span_singleton_le_iff_mem.mp le)

Premises used: Iff.mpr, Classical.not_not, Set.Mem, setOf, Ideal.span_singleton_le_iff_mem, Iff.mp, Not
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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 ∉ { asIdeal := q, isPrime := prime : PrimeSpectrum R }.asIdeal.primeCompl

Tactic:
exact not_not.mpr (q.span_singleton_le_iff_mem.mp le)

Premises used: Iff.mpr, Classical.not_not, Ideal.span_singleton_le_iff_mem, Iff.mp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
inst : CommRing R
c : R
this : Algebra R[X] (Away c)[X] := RingHom.toAlgebra (mapRingHom (algebraMap R (Away c)))
⊢ IsLocalization (Submonoid.map (F := R →+* R[X]) C (Submonoid.powers c)) (Away c)[X]

Tactic:
have := Polynomial.isLocalization (.powers c) (Away c)
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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]
⊢ 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

Premises used: Submonoid.map_powers
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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]
⊢ 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
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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])
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])
⊢ 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})))))

Tactic:
rw [range_comap_of_surjective _ _ surj, localization_away_comap_range _ (C c)]

Premises used: Polynomial.C, range_comap_of_surjective, DFunLike.coe, PrimeSpectrum.localization_away_comap_range
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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])
⊢ (↑(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:
simp [Polynomial.ker_mapRingHom, Ideal.map_span]

Premises used: Polynomial.ker_mapRingHom, Ideal.map_span
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
i j : R
⊢ IsCompact ((↑(basicOpen i) : Set (PrimeSpectrum R)) ∩ (↑(basicOpen j) : Set (PrimeSpectrum R)))

Tactic:
simpa [← TopologicalSpace.Opens.coe_inf, ← basicOpen_mul, -basicOpen_eq_zeroLocus_compl]
      using isCompact_basicOpen _

Premises used: PrimeSpectrum.basicOpen_mul, PrimeSpectrum.basicOpen_eq_zeroLocus_compl, PrimeSpectrum.isCompact_basicOpen, TopologicalSpace.Opens.coe_inf
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
inst_1 : DecidableEq ι
i : ι
f : R i
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)))
⊢ comap (Pi.evalRingHom R i) '' (↑(basicOpen f) : Set (PrimeSpectrum (R i))) =
    (↑(basicOpen (Pi.single (M := R) i f)) : Set (PrimeSpectrum ((i : ι) → R i)))

Tactic:
ext p
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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)))

Tactic:
⟨?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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)))
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
⊢ 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 ⟨?_, ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
inst_1 : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum (R i)
hp : p ∈ (↑(basicOpen f) : Set (PrimeSpectrum (R i)))
⊢ comap (Pi.evalRingHom R i) p ∈ (↑(basicOpen (Pi.single (M := R) i f)) : Set (PrimeSpectrum ((i : ι) → R i)))

Tactic:
simpa
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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)))
rw : RingHom.ker (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) ≤ p.asIdeal
⊢ Membership.mem (γ := Set (PrimeSpectrum ((i : ι) → R i)))
    (Set.range (ι := PrimeSpectrum (R i)) (comap (Pi.evalRingHom R i))) p

Tactic:
rw [range_comap_of_surjective _ _ (RingHom.surjective _), mem_zeroLocus,
        SetLike.coe_subset_coe]

Premises used: range_comap_of_surjective, PrimeSpectrum.mem_zeroLocus, SetLike.coe_subset_coe, RingHom.surjective
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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 i = 0

Tactic:
rw [RingHom.mem_ker, Pi.evalRingHom_apply] at hx

Premises used: Pi.evalRingHom_apply, RingHom.mem_ker
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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
h : ∀ (j : ι), (Pi.single (M := R) i f * x) j = 0 j
⊢ Pi.single (M := R) i f * x = 0

Tactic:
ext j
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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
neg : ∀ (h : ¬i = j), (Pi.single (M := R) i f * x) j = 0 j
⊢ (Pi.single (M := R) i f * x) j = 0 j

Tactic:
by_cases h : i = j
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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
pos : (Pi.single (M := R) i f * x) i = 0 i
⊢ (Pi.single (M := R) i f * x) j = 0 j

Tactic:
subst h
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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) i = 0 i

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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

Tactic:
have : Pi.single i f * x = 0 := by
        ext j
        by_cases h : i = j
        · subst h
          simp [hx]
        · simp [h]
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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
inr : ∀ (h : x ∈ p.asIdeal), x ∈ p.asIdeal
⊢ x ∈ p.asIdeal

Tactic:
obtain (h | h) := Ideal.IsPrime.mem_or_mem_of_mul_eq_zero p.isPrime this

Premises used: PrimeSpectrum.isPrime, Ideal.IsPrime.mem_or_mem_of_mul_eq_zero
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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
h : Pi.single (M := R) i f ∈ p.asIdeal
⊢ x ∈ p.asIdeal

Tactic:
tauto
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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
h : x ∈ p.asIdeal
⊢ x ∈ p.asIdeal

Tactic:
tauto
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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

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
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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
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)
⊢ Membership.mem (γ := Set (PrimeSpectrum ((i : ι) → R i)))
    (comap (Pi.evalRingHom R i) '' (↑(basicOpen f) : Set (PrimeSpectrum (R i)))) p

Tactic:
obtain ⟨q, rfl⟩ := this

Premises used: rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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)))
⊢ q ∈ (↑(basicOpen f) : Set (PrimeSpectrum (R i)))

Tactic:
simpa using hp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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)))
asIdeal :
  ∀ (x : (i : ι) → R i),
    Membership.mem (γ := Ideal ((i : ι) → R i)) (PrimeSpectrum.asIdeal (comap (Pi.evalRingHom R i) q)) x ↔
      Membership.mem (γ := Ideal ((i : ι) → R i)) (PrimeSpectrum.asIdeal (comap (Pi.evalRingHom R i) q)) x
⊢ Eq (α := PrimeSpectrum ((i : ι) → R i)) (comap (Pi.evalRingHom R i) q) (comap (Pi.evalRingHom R i) q)

Tactic:
ext
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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)))
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:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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)))
⊢ 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:
exact ⟨q, by simpa using hp, by ext; simp⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
inst_1 : DecidableEq ι
i : ι
f : R i
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)))
⊢ 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)))

Tactic:
simp only [Set.image_image, sigmaToPi_apply]

Premises used: Set.image_image, PrimeSpectrum.sigmaToPi_apply
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
inst_1 : DecidableEq ι
i : ι
f : R i
⊢ (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:
PrimeSpectrum.comap_evalRingHom_basicOpen _ _

Premises used: PrimeSpectrum.comap_evalRingHom_basicOpen
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
inst_1 : DecidableEq ι
i : ι
f : R i
⊢ (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:
exact PrimeSpectrum.comap_evalRingHom_basicOpen _ _

Premises used: PrimeSpectrum.comap_evalRingHom_basicOpen
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
⊢ IsOpenEmbedding (X := (i : ι) × PrimeSpectrum (R i)) (sigmaToPi R)

Tactic:
.of_continuous_injective_isOpenMap ?_ ?_ ?_

Premises used: Topology.IsOpenEmbedding.of_continuous_injective_isOpenMap
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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)
refine_3 : IsOpenMap (X := (i : ι) × PrimeSpectrum (R i)) (sigmaToPi R)
⊢ IsOpenEmbedding (X := (i : ι) × PrimeSpectrum (R i)) (sigmaToPi R)

Tactic:
refine .of_continuous_injective_isOpenMap ?_ ?_ ?_
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
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)
⊢ Continuous (X := (i : ι) × PrimeSpectrum (R i)) (sigmaToPi R)

Tactic:
rw [continuous_sigma_iff]

Premises used: continuous_sigma_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
i : ι
⊢ Continuous (Y := PrimeSpectrum ((i : ι) → R i)) fun (a : PrimeSpectrum (R i)) ↦
    sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i a)

Tactic:
continuous_comap (Pi.evalRingHom R i)

Premises used: PrimeSpectrum.continuous_comap, PrimeSpectrum.sigmaToPi, Pi.evalRingHom