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
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
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
⊢ 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)))

Tactic:
refine Set.ext fun p ↦ ⟨?_, fun h ↦ ?_⟩

Premises used: Set.ext, Iff.intro
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
I : PrimeSpectrum R
⊢ Membership.mem (γ := Set (PrimeSpectrum (R × S)))
    (zeroLocus (↑(RingHom.ker (F := R × S →+* R) (RingHom.fst R S)) : Set (R × S))) (comap (RingHom.fst R S) I)

Tactic:
Ideal.comap_mono bot_le

Premises used: PrimeSpectrum.zeroLocus, Set.Mem, setOf, Ideal.comap_mono, Set.Subset, bot_le
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
I : PrimeSpectrum R
⊢ Membership.mem (γ := Set (PrimeSpectrum (R × S)))
    (zeroLocus (↑(RingHom.ker (F := R × S →+* R) (RingHom.fst R S)) : Set (R × S))) (comap (RingHom.fst R S) I)

Tactic:
exact Ideal.comap_mono bot_le

Premises used: Ideal.comap_mono, bot_le
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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
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
⊢ 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

Premises used: Ideal.ideal_prod_prime, PrimeSpectrum.isPrime, Iff.mp, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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 R
hp : p.IsPrime
eq : p_1.asIdeal = p.prod ⊤
⊢ asIdeal (comap (RingHom.fst R S) { asIdeal := p, isPrime := hp : PrimeSpectrum R }) = p_1.asIdeal

Tactic:
simpa [Ideal.prod] using eq.symm

Premises used: Ideal.prod, Eq.symm
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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 R
hp : p.IsPrime
eq : p_1.asIdeal = p.prod ⊤
⊢ Membership.mem (γ := Set (PrimeSpectrum (R × S))) (Set.range (ι := PrimeSpectrum R) (comap (RingHom.fst R S))) p_1

Tactic:
exact ⟨⟨p, hp⟩, PrimeSpectrum.ext <| by simpa [Ideal.prod] using eq.symm⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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

Tactic:
(hp.ne_top <| (Ideal.eq_top_iff_one _).mpr ?_).elim

Premises used: Iff.mpr, False.elim, Ideal.eq_top_iff_one, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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
refine_2 : 1 ∈ p
⊢ Membership.mem (γ := Set (PrimeSpectrum (R × S))) (Set.range (ι := PrimeSpectrum R) (comap (RingHom.fst R S))) p_1

Tactic:
refine (hp.ne_top <| (Ideal.eq_top_iff_one _).mpr ?_).elim

Premises used: Iff.mpr, False.elim, Ideal.eq_top_iff_one, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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 (γ := Ideal (R × S)) (RingHom.ker (F := R × S →+* R) (RingHom.fst R S)) (0, 1)

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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
⊢ 1 ∈ p

Tactic:
simpa [eq] using h (show (0, 1) ∈ RingHom.ker (RingHom.fst R S) by simp)
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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)))

Tactic:
Set.ext fun p ↦ ⟨?_, fun h ↦ ?_⟩

Premises used: Set.ext, Iff.intro
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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
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
⊢ 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)))

Tactic:
refine Set.ext fun p ↦ ⟨?_, fun h ↦ ?_⟩

Premises used: Set.ext, Iff.intro
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
I : PrimeSpectrum S
⊢ Membership.mem (γ := Set (PrimeSpectrum (R × S)))
    (zeroLocus (↑(RingHom.ker (F := R × S →+* S) (RingHom.snd R S)) : Set (R × S))) (comap (RingHom.snd R S) I)

Tactic:
Ideal.comap_mono bot_le

Premises used: PrimeSpectrum.zeroLocus, Set.Mem, setOf, Ideal.comap_mono, Set.Subset, bot_le
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
I : PrimeSpectrum S
⊢ Membership.mem (γ := Set (PrimeSpectrum (R × S)))
    (zeroLocus (↑(RingHom.ker (F := R × S →+* S) (RingHom.snd R S)) : Set (R × S))) (comap (RingHom.snd R S) I)

Tactic:
exact Ideal.comap_mono bot_le

Premises used: Ideal.comap_mono, bot_le
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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 →+* S) (RingHom.snd 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 S) (comap (RingHom.snd R S))) p
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 S) (comap (RingHom.snd R S))) p
⊢ Membership.mem (γ := Set (PrimeSpectrum (R × S))) (Set.range (ι := PrimeSpectrum S) (comap (RingHom.snd R S))) p

Tactic:
obtain ⟨p, hp, eq⟩ | ⟨p, hp, eq⟩ := p.1.ideal_prod_prime.mp p.2

Premises used: Ideal.ideal_prod_prime, PrimeSpectrum.isPrime, Iff.mp, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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 →+* S) (RingHom.snd R S)) : Set (R × S))) p_1
p : Ideal R
hp : p.IsPrime
eq : p_1.asIdeal = p.prod ⊤
⊢ Membership.mem (γ := Set (PrimeSpectrum (R × S))) (Set.range (ι := PrimeSpectrum S) (comap (RingHom.snd R S))) p_1

Tactic:
(hp.ne_top <| (Ideal.eq_top_iff_one _).mpr ?_).elim

Premises used: Iff.mpr, False.elim, Ideal.eq_top_iff_one, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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 →+* S) (RingHom.snd R S)) : Set (R × S))) p_1
p : Ideal R
hp : p.IsPrime
eq : p_1.asIdeal = p.prod ⊤
refine_2 : 1 ∈ p
⊢ Membership.mem (γ := Set (PrimeSpectrum (R × S))) (Set.range (ι := PrimeSpectrum S) (comap (RingHom.snd R S))) p_1

Tactic:
refine (hp.ne_top <| (Ideal.eq_top_iff_one _).mpr ?_).elim

Premises used: Iff.mpr, False.elim, Ideal.eq_top_iff_one, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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 →+* S) (RingHom.snd R S)) : Set (R × S))) p_1
p : Ideal R
hp : p.IsPrime
eq : p_1.asIdeal = p.prod ⊤
⊢ Membership.mem (γ := Ideal (R × S)) (RingHom.ker (F := R × S →+* S) (RingHom.snd R S)) (1, 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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 →+* S) (RingHom.snd R S)) : Set (R × S))) p_1
p : Ideal R
hp : p.IsPrime
eq : p_1.asIdeal = p.prod ⊤
⊢ 1 ∈ p

Tactic:
simpa [eq] using h (show (1, 0) ∈ RingHom.ker (RingHom.snd R S) by simp)
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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 →+* S) (RingHom.snd R S)) : Set (R × S))) p_1
p : Ideal S
hp : p.IsPrime
eq : p_1.asIdeal = Ideal.prod ⊤ p
⊢ asIdeal (comap (RingHom.snd R S) { asIdeal := p, isPrime := hp : PrimeSpectrum S }) = p_1.asIdeal

Tactic:
simpa [Ideal.prod] using eq.symm

Premises used: Ideal.prod, Eq.symm
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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 →+* S) (RingHom.snd 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 S) (comap (RingHom.snd R S))) p_1

Tactic:
exact ⟨⟨p, hp⟩, PrimeSpectrum.ext <| by simpa [Ideal.prod] using eq.symm⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
simp_rw :
  IsClosed (X := PrimeSpectrum (R × S)) (zeroLocus (↑(RingHom.ker (F := R × S →+* R) (RingHom.fst R S)) : Set (R × S)))
⊢ IsClosed (X := PrimeSpectrum (R × S)) (Set.range (ι := PrimeSpectrum R) (comap (RingHom.fst R S)))

Tactic:
simp_rw [range_comap_fst, isClosed_zeroLocus]

Premises used: PrimeSpectrum.isClosed_zeroLocus, PrimeSpectrum.range_comap_fst
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
simp_rw :
  IsClosed (X := PrimeSpectrum (R × S)) (zeroLocus (↑(RingHom.ker (F := R × S →+* S) (RingHom.snd R S)) : Set (R × S)))
⊢ IsClosed (X := PrimeSpectrum (R × S)) (Set.range (ι := PrimeSpectrum S) (comap (RingHom.snd R S)))

Tactic:
simp_rw [range_comap_snd, isClosed_zeroLocus]

Premises used: PrimeSpectrum.isClosed_zeroLocus, PrimeSpectrum.range_comap_snd
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
refine :
  IsInducing (X := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)) (Y := PrimeSpectrum (R × S))
    (⇑(Equiv.symm (primeSpectrumProd R S)) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
⊢ PrimeSpectrum (R × S) ≃ₜ Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)

Tactic:
refine ((primeSpectrumProd R S).symm.toHomeomorphOfIsInducing ?_).symm

Premises used: PrimeSpectrum.primeSpectrumProd, Homeomorph.symm, Equiv.toHomeomorphOfIsInducing, Equiv.symm
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
⊢ IsInducing (X := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)) (Y := PrimeSpectrum (R × S))
    (⇑(Equiv.symm (primeSpectrumProd R S)) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))

Tactic:
(IsClosedEmbedding.of_continuous_injective_isClosedMap ?_
    (Equiv.injective _) ?_).isInducing

Premises used: Topology.IsClosedEmbedding.isInducing, Topology.IsClosedEmbedding.of_continuous_injective_isClosedMap, Equiv.injective
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
refine_1 :
  Continuous (X := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)) (Y := PrimeSpectrum (R × S))
    (⇑(Equiv.symm (primeSpectrumProd R S)) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
refine_2 :
  IsClosedMap (X := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)) (Y := PrimeSpectrum (R × S))
    (⇑(Equiv.symm (primeSpectrumProd R S)) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
⊢ IsInducing (X := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)) (Y := PrimeSpectrum (R × S))
    (⇑(Equiv.symm (primeSpectrumProd R S)) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))

Tactic:
refine (IsClosedEmbedding.of_continuous_injective_isClosedMap ?_
    (Equiv.injective _) ?_).isInducing

Premises used: Topology.IsClosedEmbedding.isInducing, Topology.IsClosedEmbedding.of_continuous_injective_isClosedMap, Equiv.injective
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
refine_1 :
  Continuous (X := PrimeSpectrum R) (Y := PrimeSpectrum (R × S))
      (Function.comp (β := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S))
        (⇑(Equiv.symm (primeSpectrumProd R S)) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        Sum.inl) ∧
    Continuous (X := PrimeSpectrum S) (Y := PrimeSpectrum (R × S))
      (Function.comp (β := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S))
        (⇑(Equiv.symm (primeSpectrumProd R S)) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        Sum.inr)
⊢ Continuous (X := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)) (Y := PrimeSpectrum (R × S))
    (⇑(Equiv.symm (primeSpectrumProd R S)) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))

Tactic:
rw [continuous_sum_dom]

Premises used: continuous_sum_dom
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
refine_1 :
  (Continuous (Y := PrimeSpectrum (R × S)) fun (x : PrimeSpectrum R) ↦ comap (RingHom.fst R S) x) ∧
    Continuous (Y := PrimeSpectrum (R × S)) fun (x : PrimeSpectrum S) ↦ comap (RingHom.snd R S) x
⊢ Continuous (X := PrimeSpectrum R) (Y := PrimeSpectrum (R × S))
      (Function.comp (β := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S))
        (⇑(Equiv.symm (primeSpectrumProd R S)) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        Sum.inl) ∧
    Continuous (X := PrimeSpectrum S) (Y := PrimeSpectrum (R × S))
      (Function.comp (β := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S))
        (⇑(Equiv.symm (primeSpectrumProd R S)) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
        Sum.inr)

Tactic:
simp only [Function.comp_def, primeSpectrumProd_symm_inl, primeSpectrumProd_symm_inr]

Premises used: PrimeSpectrum.primeSpectrumProd_symm_inl, PrimeSpectrum.primeSpectrumProd_symm_inr, Function.comp_def
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
⊢ (Continuous (Y := PrimeSpectrum (R × S)) fun (x : PrimeSpectrum R) ↦ comap (RingHom.fst R S) x) ∧
    Continuous (Y := PrimeSpectrum (R × S)) fun (x : PrimeSpectrum S) ↦ comap (RingHom.snd R S) x

Tactic:
⟨continuous_comap _, continuous_comap _⟩

Premises used: PrimeSpectrum.continuous_comap, And.intro
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
⊢ (Continuous (Y := PrimeSpectrum (R × S)) fun (x : PrimeSpectrum R) ↦ comap (RingHom.fst R S) x) ∧
    Continuous (Y := PrimeSpectrum (R × S)) fun (x : PrimeSpectrum S) ↦ comap (RingHom.snd R S) x

Tactic:
exact ⟨continuous_comap _, continuous_comap _⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
refine_2 :
  (IsClosedMap (Y := PrimeSpectrum (R × S)) fun (a : PrimeSpectrum R) ↦ comap (RingHom.fst R S) a) ∧
    IsClosedMap (Y := PrimeSpectrum (R × S)) fun (b : PrimeSpectrum S) ↦ comap (RingHom.snd R S) b
⊢ IsClosedMap (X := Sum.{u, v} (PrimeSpectrum R) (PrimeSpectrum S)) (Y := PrimeSpectrum (R × S))
    (⇑(Equiv.symm (primeSpectrumProd R S)) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))

Tactic:
simp_rw [isClosedMap_sum, primeSpectrumProd_symm_inl, primeSpectrumProd_symm_inr]

Premises used: PrimeSpectrum.primeSpectrumProd_symm_inl, PrimeSpectrum.primeSpectrumProd_symm_inr, isClosedMap_sum
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
⊢ (IsClosedMap (Y := PrimeSpectrum (R × S)) fun (a : PrimeSpectrum R) ↦ comap (RingHom.fst R S) a) ∧
    IsClosedMap (Y := PrimeSpectrum (R × S)) fun (b : PrimeSpectrum S) ↦ comap (RingHom.snd R S) b

Tactic:
⟨isClosedEmbedding_comap_fst.isClosedMap, isClosedEmbedding_comap_snd.isClosedMap⟩

Premises used: PrimeSpectrum.isClosedEmbedding_comap_snd, Topology.IsClosedEmbedding.isClosedMap, PrimeSpectrum.isClosedEmbedding_comap_fst, And.intro
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
⊢ (IsClosedMap (Y := PrimeSpectrum (R × S)) fun (a : PrimeSpectrum R) ↦ comap (RingHom.fst R S) a) ∧
    IsClosedMap (Y := PrimeSpectrum (R × S)) fun (b : PrimeSpectrum S) ↦ comap (RingHom.snd R S) b

Tactic:
exact ⟨isClosedEmbedding_comap_fst.isClosedMap, isClosedEmbedding_comap_snd.isClosedMap⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
f : R
x : PrimeSpectrum R
⊢ Membership.mem (γ := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen f) x ↔ f ∉ x.asIdeal

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Not
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
a : R
⊢ IsOpen (↑(basicOpen a) : Set (PrimeSpectrum R))

Tactic:
(basicOpen a).isOpen

Premises used: PrimeSpectrum.basicOpen, TopologicalSpace.Opens.isOpen
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
r : R
x : PrimeSpectrum R
⊢ x ∈ (↑(basicOpen r) : Set (PrimeSpectrum R)) ↔ Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus {r})ᶜ x

Tactic:
simp only [SetLike.mem_coe, mem_basicOpen, Set.mem_compl_iff, mem_zeroLocus,
    Set.singleton_subset_iff]

Premises used: Set.singleton_subset_iff, PrimeSpectrum.mem_zeroLocus, SetLike.mem_coe, PrimeSpectrum.mem_basicOpen, Set.mem_compl_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
⊢ (↑(basicOpen 1) : Set (PrimeSpectrum R)) = (↑⊤ : Set (PrimeSpectrum R))

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
⊢ (↑(basicOpen 0) : Set (PrimeSpectrum R)) = (↑⊥ : Set (PrimeSpectrum R))

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
f g : R
rw :
  (↑(basicOpen f) : Set (PrimeSpectrum R)) ⊆ (↑(basicOpen g) : Set (PrimeSpectrum R)) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {g})) f
rw₁ :
  (zeroLocus {f})ᶜ ⊆ (↑(basicOpen g) : Set (PrimeSpectrum R)) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {g})) f
rw₂ :
  Subset (α := Set (PrimeSpectrum R)) (zeroLocus {f})ᶜ (zeroLocus {g})ᶜ ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {g})) f
rw₃ :
  Subset (α := Set (PrimeSpectrum R)) (zeroLocus {g}) (zeroLocus {f}) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {g})) f
rw₄ rw₅ :
  Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {g})) f ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {g})) f
⊢ LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen f) (basicOpen g) ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {g})) f

Tactic:
rw [← SetLike.coe_subset_coe, basicOpen_eq_zeroLocus_compl, basicOpen_eq_zeroLocus_compl,
    Set.compl_subset_compl, zeroLocus_subset_zeroLocus_singleton_iff]

Premises used: PrimeSpectrum.zeroLocus_subset_zeroLocus_singleton_iff, Set.compl_subset_compl, SetLike.coe_subset_coe, PrimeSpectrum.basicOpen_eq_zeroLocus_compl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
f g : R
inst_2 : Algebra R S
inst_3 : IsLocalization.Away f S
simp_rw :
  Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {g})) f ↔
    IsUnit.{v} (M := S) ((algebraMap R S : (a : R) → S) g : S)
simp_rw₁ :
  (∃ (n : ℕ), Membership.mem (γ := Ideal R) (Ideal.span {g}) (f ^ n)) ↔
    IsUnit.{v} (M := S) ((algebraMap R S : (a : R) → S) g : S)
simp_rw₂ : (∃ (n : ℕ), g ∣ f ^ n) ↔ IsUnit.{v} (M := S) ((algebraMap R S : (a : R) → S) g : S)
⊢ LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen f) (basicOpen g) ↔
    IsUnit.{v} (M := S) ((algebraMap R S : (a : R) → S) g : S)

Tactic:
simp_rw [basicOpen_le_basicOpen_iff, Ideal.mem_radical_iff, Ideal.mem_span_singleton,
    IsLocalization.Away.algebraMap_isUnit_iff f]

Premises used: IsLocalization.Away.algebraMap_isUnit_iff, PrimeSpectrum.basicOpen_le_basicOpen_iff, Ideal.mem_radical_iff, Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
f g : R
⊢ (↑(basicOpen (f * g)) : Set (PrimeSpectrum R)) = (↑(basicOpen f ⊓ basicOpen g) : Set (PrimeSpectrum R))

Tactic:
simp [zeroLocus_singleton_mul]

Premises used: PrimeSpectrum.zeroLocus_singleton_mul