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
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)
⊢ 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
-- 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
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.asIdeal = q.asIdeal

Tactic:
rw [IsLocalization.map_under M S, IsLocalization.map_under M S] at h

Premises used: IsLocalization.map_under
-- 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
M : Submonoid R
inst_3 : IsLocalization M S
p q : PrimeSpectrum S
h asIdeal : p.asIdeal = q.asIdeal
⊢ p = q

Tactic:
ext1
-- 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
M : Submonoid R
inst_3 : IsLocalization M S
p q : PrimeSpectrum S
h : p.asIdeal = q.asIdeal
⊢ p.asIdeal = q.asIdeal

Tactic:
h
-- 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
M : Submonoid R
inst_3 : IsLocalization M S
p q : PrimeSpectrum S
h : p.asIdeal = q.asIdeal
⊢ p.asIdeal = q.asIdeal

Tactic:
exact h
-- 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
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)}

Tactic:
Set.ext fun x ↦ ⟨?_, 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
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
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
⊢ Eq (α := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S)))
    {p : PrimeSpectrum R | Disjoint (↑M : Set R) (↑p.asIdeal : Set R)}

Tactic:
refine Set.ext fun x ↦ ⟨?_, 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
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
p : PrimeSpectrum S
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) {p : PrimeSpectrum R | Disjoint (↑M : Set R) (↑p.asIdeal : Set R)}
    (comap (algebraMap R S) p)

Tactic:
((IsLocalization.isPrime_iff_isPrime_disjoint ..).mp p.2).2

Premises used: PrimeSpectrum.isPrime, Set.Mem, setOf, Disjoint, IsLocalization.isPrime_iff_isPrime_disjoint, And.right, Iff.mp
-- 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
M : Submonoid R
inst_3 : IsLocalization M S
p : PrimeSpectrum S
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) {p : PrimeSpectrum R | Disjoint (↑M : Set R) (↑p.asIdeal : Set R)}
    (comap (algebraMap R S) p)

Tactic:
exact ((IsLocalization.isPrime_iff_isPrime_disjoint ..).mp p.2).2

Premises used: PrimeSpectrum.isPrime, IsLocalization.isPrime_iff_isPrime_disjoint, And.right, Iff.mp
-- 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
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
h₁ : comap (algebraMap R S) { asIdeal := Ideal.map (F := R →+* S) (algebraMap R S) x.asIdeal, isPrime := ⋯ } = x
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S))) x

Tactic:
use ⟨x.asIdeal.map (algebraMap R S), IsLocalization.isPrime_of_isPrime_disjoint M S _ x.2 h⟩
-- 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
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
h₁ :
  asIdeal (comap (algebraMap R S) { asIdeal := Ideal.map (F := R →+* S) (algebraMap R S) x.asIdeal, isPrime := ⋯ }) =
    x.asIdeal
⊢ comap (algebraMap R S) { asIdeal := Ideal.map (F := R →+* S) (algebraMap R S) x.asIdeal, isPrime := ⋯ } = x

Tactic:
ext1
-- 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
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
⊢ asIdeal (comap (algebraMap R S) { asIdeal := Ideal.map (F := R →+* S) (algebraMap R S) x.asIdeal, isPrime := ⋯ }) =
    x.asIdeal

Tactic:
IsLocalization.under_map_of_isPrime_disjoint M S x.2 h

Premises used: PrimeSpectrum.isPrime, Ideal.comap, IsLocalization.under_map_of_isPrime_disjoint
-- 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
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
⊢ asIdeal (comap (algebraMap R S) { asIdeal := Ideal.map (F := R →+* S) (algebraMap R S) x.asIdeal, isPrime := ⋯ }) =
    x.asIdeal

Tactic:
exact IsLocalization.under_map_of_isPrime_disjoint M S x.2 h

Premises used: PrimeSpectrum.isPrime, IsLocalization.under_map_of_isPrime_disjoint
-- 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
M : Submonoid R
inst_3 : IsLocalization M S
⊢ IsInducing (X := PrimeSpectrum S) (Y := PrimeSpectrum R) (comap (algebraMap R S))

Tactic:
⟨TopologicalSpace.ext_isClosed fun Z ↦ ?_⟩

Premises used: Topology.IsInducing.mk, TopologicalSpace.ext_isClosed
-- 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
M : Submonoid R
inst_3 : IsLocalization M S
refine :
  ∀ (Z : Set (PrimeSpectrum S)),
    IsClosed Z ↔ IsClosed[TopologicalSpace.induced (comap (algebraMap R S)) zariskiTopology] Z
⊢ IsInducing (X := PrimeSpectrum S) (Y := PrimeSpectrum R) (comap (algebraMap R S))

Tactic:
refine ⟨TopologicalSpace.ext_isClosed fun Z ↦ ?_⟩
-- 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
M : Submonoid R
inst_3 : IsLocalization M S
Z : Set (PrimeSpectrum S)
simp_rw : (∃ (s : Set S), zeroLocus s = Z) ↔ ∃ (a : Set R), zeroLocus ((⇑(algebraMap R S) : (a : R) → S) '' a) = Z
⊢ IsClosed Z ↔ IsClosed[TopologicalSpace.induced (comap (algebraMap R S)) zariskiTopology] Z

Tactic:
simp_rw [isClosed_induced_iff, isClosed_iff_zeroLocus, @eq_comm _ _ (zeroLocus _),
    exists_exists_eq_and, preimage_comap_zeroLocus]

Premises used: PrimeSpectrum.isClosed_iff_zeroLocus, PrimeSpectrum.preimage_comap_zeroLocus, eq_comm, isClosed_induced_iff, exists_exists_eq_and
-- 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
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
mpr : (∃ (a : Set R), zeroLocus ((⇑(algebraMap R S) : (a : R) → S) '' a) = Z) → ∃ (s : Set S), zeroLocus s = Z
⊢ (∃ (s : Set S), zeroLocus s = Z) ↔ ∃ (a : Set R), zeroLocus ((⇑(algebraMap R S) : (a : R) → S) '' a) = Z

Tactic:
constructor
-- 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
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)

Tactic:
⟨(Ideal.span s).comap (algebraMap R S), ?_⟩

Premises used: Algebra.algebraMap, SetLike.coe, Ideal.comap, Exists.intro, Ideal.span
-- 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
M : Submonoid R
inst_3 : IsLocalization M S
s : Set S
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)
⊢ ∃ (a : Set R), Eq (α := Set (PrimeSpectrum S)) (zeroLocus ((⇑(algebraMap R S) : (a : R) → S) '' a)) (zeroLocus s)

Tactic:
refine ⟨(Ideal.span s).comap (algebraMap R S), ?_⟩
-- 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
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))
mp₃ mp₄ : Eq (α := Set (PrimeSpectrum S)) (zeroLocus (↑(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)

Tactic:
rw [← zeroLocus_span, ← zeroLocus_span s, ← Ideal.map, IsLocalization.map_under M S]

Premises used: PrimeSpectrum.zeroLocus_span, Ideal.map, IsLocalization.map_under
-- 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
M : Submonoid R
inst_3 : IsLocalization M S
s : Set R
⊢ ∃ (s_1 : Set S), Eq (α := Set (PrimeSpectrum S)) (zeroLocus s_1) (zeroLocus ((⇑(algebraMap R S) : (a : R) → S) '' s))

Tactic:
⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- 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
M : Submonoid R
inst_3 : IsLocalization M S
s : Set R
⊢ ∃ (s_1 : Set S), Eq (α := Set (PrimeSpectrum S)) (zeroLocus s_1) (zeroLocus ((⇑(algebraMap R S) : (a : R) → S) '' s))

Tactic:
exact ⟨_, rfl⟩
-- 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
M : Submonoid R
inst_3 : IsLocalization M S
⊢ IsEmbedding (X := PrimeSpectrum S) (Y := PrimeSpectrum R) (comap (algebraMap R S))

Tactic:
⟨localization_comap_isInducing S M, localization_comap_injective S M⟩

Premises used: PrimeSpectrum.localization_comap_isInducing, PrimeSpectrum.localization_comap_injective, Topology.IsEmbedding.mk
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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)
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ᶜ
⊢ zariskiTopology = TopologicalSpace.induced (comap f) zariskiTopology

Tactic:
simp only [TopologicalSpace.ext_iff, ← isClosed_compl_iff, isClosed_iff_zeroLocus,
      isClosed_induced_iff]

Premises used: PrimeSpectrum.isClosed_iff_zeroLocus, TopologicalSpace.ext_iff, isClosed_induced_iff, isClosed_compl_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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ᶜ
rw₂ rw₃ : Eq (α := Set (PrimeSpectrum S)) (zeroLocus F) (zeroLocus F)
⊢ comap f ⁻¹' zeroLocus ((⇑f : (a : R) → S) ⁻¹' F) = sᶜ

Tactic:
rw [preimage_comap_zeroLocus, Function.Surjective.image_preimage hf, hF]

Premises used: PrimeSpectrum.preimage_comap_zeroLocus, Function.Surjective.image_preimage
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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)
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
⊢ ∀ (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:
refine fun s =>
      ⟨fun ⟨F, hF⟩ =>
        ⟨zeroLocus (f ⁻¹' F), ⟨f ⁻¹' F, rfl⟩, by
          rw [preimage_comap_zeroLocus, Function.Surjective.image_preimage hf, hF]⟩,
        ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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)
F : Set R
hF : comap f ⁻¹' zeroLocus F = sᶜ
⊢ ∃ (s_1 : Set S), sᶜ = zeroLocus s_1

Tactic:
⟨f '' F, hF.symm.trans (preimage_comap_zeroLocus f F)⟩

Premises used: PrimeSpectrum.preimage_comap_zeroLocus, Exists.intro, Set.image, Eq.symm, DFunLike.coe, Eq.trans
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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)
F : Set R
hF : comap f ⁻¹' zeroLocus F = sᶜ
⊢ ∃ (s_1 : Set S), sᶜ = zeroLocus s_1

Tactic:
exact ⟨f '' F, hF.symm.trans (preimage_comap_zeroLocus f F)⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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)
⊢ IsEmbedding (comap f)

Tactic:
(isEmbedding_iff _).2 ⟨comap_isInducing_of_surjective _ _ hf, comap_injective_of_surjective f hf⟩

Premises used: Iff.mpr, Topology.isEmbedding_iff, And.intro, PrimeSpectrum.comap_injective_of_surjective, PrimeSpectrum.comap_isInducing_of_surjective
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
e : R ≃+* S
x : PrimeSpectrum R
⊢ comap (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e.symm : S →+* R) (↑e : R →+* S)) x = x

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
e : R ≃+* S
x : PrimeSpectrum S
⊢ comap (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e : R →+* S) (↑e.symm : S →+* R)) x = x

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
hf : Function.Bijective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ IsHomeomorph (comap f)

Tactic:
(homeomorphOfRingEquiv (.ofBijective f hf)).symm.isHomeomorph

Premises used: RingEquiv.ofBijective, MonoidHomClass.toMonoidHom, Homeomorph.isHomeomorph, RingHomClass.toRingHom, Homeomorph.symm, PrimeSpectrum.homeomorphOfRingEquiv, PrimeSpectrum.comap
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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)
x : PrimeSpectrum S
hx : IsClosed (X := PrimeSpectrum S) {x}
⊢ IsClosed (X := PrimeSpectrum R) {comap f x}

Tactic:
haveI : x.asIdeal.IsMaximal := (isClosed_singleton_iff_isMaximal x).1 hx
  (isClosed_singleton_iff_isMaximal _).2 (Ideal.comap_isMaximal_of_surjective f hf)

Premises used: Iff.mpr, Ideal.comap_isMaximal_of_surjective, PrimeSpectrum.isClosed_singleton_iff_isMaximal, PrimeSpectrum.comap
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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))

Tactic:
⟨comap_injective_of_surjective _ Ideal.Quotient.mk_surjective, ?_⟩

Premises used: Ideal.Quotient.mk_surjective, And.intro, PrimeSpectrum.comap_injective_of_surjective, Function.Bijective
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hle : I ≤ nilradical R
refine : Surjective.{u + 1, u + 1} (α := PrimeSpectrum (R ⧸ I)) (β := PrimeSpectrum R) (comap (Ideal.Quotient.mk I))
⊢ Bijective.{u + 1, u + 1} (α := PrimeSpectrum (R ⧸ I)) (β := PrimeSpectrum R) (comap (Ideal.Quotient.mk I))

Tactic:
refine ⟨comap_injective_of_surjective _ Ideal.Quotient.mk_surjective, ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hle : I ≤ nilradical R
⊢ Surjective.{u + 1, u + 1} (α := PrimeSpectrum (R ⧸ I)) (β := PrimeSpectrum R) (comap (Ideal.Quotient.mk I))

Tactic:
simpa [← Set.range_eq_univ, range_comap_of_surjective _ _ Ideal.Quotient.mk_surjective,
    zeroLocus_eq_univ_iff]

Premises used: Set.range_eq_univ, PrimeSpectrum.zeroLocus_eq_univ_iff, range_comap_of_surjective, Ideal.Quotient.mk_surjective
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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)
rw : IsClosed (X := PrimeSpectrum R) (zeroLocus (↑(ker f) : Set R))
⊢ IsClosed (Set.range (comap f))

Tactic:
rw [range_comap_of_surjective _ f hf]

Premises used: range_comap_of_surjective
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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 (X := PrimeSpectrum R) (zeroLocus (↑(ker f) : Set R))

Tactic:
isClosed_zeroLocus _

Premises used: PrimeSpectrum.isClosed_zeroLocus
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
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 (X := PrimeSpectrum R) (zeroLocus (↑(ker f) : Set R))

Tactic:
exact isClosed_zeroLocus _

Premises used: PrimeSpectrum.isClosed_zeroLocus
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
x : PrimeSpectrum R
asIdeal :
  ∀ (x_1 : R × S),
    Membership.mem (γ := Ideal (R × S))
        (PrimeSpectrum.asIdeal
          ((Equiv.symm (primeSpectrumProd R S) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
            (Sum.inl x)))
        x_1 ↔
      Membership.mem (γ := Ideal (R × S)) (PrimeSpectrum.asIdeal (comap (RingHom.fst R S) x)) x_1
⊢ 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))

Tactic:
ext
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
x : PrimeSpectrum R
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:
simp [Ideal.prod]

Premises used: Ideal.prod
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
x : PrimeSpectrum S
asIdeal :
  ∀ (x_1 : R × S),
    Membership.mem (γ := Ideal (R × S))
        (PrimeSpectrum.asIdeal
          ((Equiv.symm (primeSpectrumProd R S) : (a : PrimeSpectrum R ⊕ PrimeSpectrum S) → PrimeSpectrum (R × S))
            (Sum.inr x)))
        x_1 ↔
      Membership.mem (γ := Ideal (R × S)) (PrimeSpectrum.asIdeal (comap (RingHom.snd R S) x)) x_1
⊢ 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))

Tactic:
ext
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
x : PrimeSpectrum S
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:
simp [Ideal.prod]

Premises used: Ideal.prod
-- 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 R) (comap (RingHom.fst R S)))
    (zeroLocus (↑(RingHom.ker (F := R × S →+* R) (RingHom.fst R S)) : Set (R × S)))

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

Premises used: Set.ext, Iff.intro