awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
inst_4 : FaithfulSMul R S
p : Ideal R
hp : p.IsPrime
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
obtain :
  ∀ Q ≥ ⊥,
    ∀ (hQ : Q.IsPrime) (hp : Ideal.IsPrime (Ideal.comap (F := R →+* S) (algebraMap R S) Q)),
      ∃ (a : PrimeSpectrum S),
        comap (algebraMap R S) a =
          { asIdeal := Ideal.comap (F := R →+* S) (algebraMap R S) Q, isPrime := hp : PrimeSpectrum R }
⊢ ∃ (a : PrimeSpectrum S), comap (algebraMap R S) a = { asIdeal := p, isPrime := hp : PrimeSpectrum R }

Tactic:
obtain ⟨Q, _, hQ, rfl⟩ := Ideal.exists_ideal_over_prime_of_isIntegral p (⊥ : Ideal S)
    (by simp [Ideal.comap_bot_of_injective (algebraMap R S) hinj])

Premises used: Bot.bot, Ideal.exists_ideal_over_prime_of_isIntegral, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
inst_4 : FaithfulSMul R S
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
Q : Ideal S
left : Q ≥ ⊥
hQ : Q.IsPrime
hp : Ideal.IsPrime (Ideal.comap (F := R →+* S) (algebraMap R S) Q)
⊢ ∃ (a : PrimeSpectrum S),
    comap (algebraMap R S) a =
      { asIdeal := Ideal.comap (F := R →+* S) (algebraMap R S) Q, isPrime := hp : PrimeSpectrum R }

Tactic:
⟨⟨Q, hQ⟩, rfl⟩

Premises used: PrimeSpectrum.mk, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
inst_4 : FaithfulSMul R S
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
Q : Ideal S
left : Q ≥ ⊥
hQ : Q.IsPrime
hp : Ideal.IsPrime (Ideal.comap (F := R →+* S) (algebraMap R S) Q)
⊢ ∃ (a : PrimeSpectrum S),
    comap (algebraMap R S) a =
      { asIdeal := Ideal.comap (F := R →+* S) (algebraMap R S) Q, isPrime := hp : PrimeSpectrum R }

Tactic:
exact ⟨⟨Q, hQ⟩, rfl⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.IsIntegral
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ let algInst := f.toAlgebra;
  Algebra.IsIntegral R S

Tactic:
algebraize [f]
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.IsIntegral
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.IsIntegral R S
⊢ FaithfulSMul R S

Tactic:
have : FaithfulSMul R S := (faithfulSMul_iff_algebraMap_injective R S).mpr hinj
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.IsIntegral
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.IsIntegral R S
this : FaithfulSMul R S
⊢ Function.Surjective (comap f)

Tactic:
Algebra.IsIntegral.comap_surjective _ _

Premises used: Algebra.IsIntegral.comap_surjective
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.IsIntegral
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.IsIntegral R S
this : FaithfulSMul R S
⊢ Function.Surjective (comap f)

Tactic:
exact Algebra.IsIntegral.comap_surjective _ _

Premises used: Algebra.IsIntegral.comap_surjective
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
I : Ideal R
e : (↑{p : Ideal R | p.IsPrime ∧ I ≤ p} : Type u) ≃o (↑(zeroLocus (↑I : Set R)) : Type u) :=
  RelIso.mk (r := fun (x1 x2 : (↑{p : Ideal R | p.IsPrime ∧ I ≤ p} : Type u)) ↦ x1 ≤ x2) (s :=
    fun (x1 x2 : (↑(zeroLocus (↑I : Set R)) : Type u)) ↦ x1 ≤ x2)
    {
      toFun := fun (x : (↑{p : Ideal R | p.IsPrime ∧ I ≤ p} : Type u)) ↦
        Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
          Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) x)
          { asIdeal := (↑x : Ideal R), isPrime := ⋯ } ⋯,
      invFun := fun (x : (↑(zeroLocus (↑I : Set R)) : Type u)) ↦
        Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p.IsPrime ∧ I ≤ p} x)
          (↑x : PrimeSpectrum R).asIdeal ⋯,
      left_inv := ⋯, right_inv := ⋯ }
    ⋯
rw :
  (↑I.minimalPrimes : Type u) ≃o
    (↑{s : Set (↑(zeroLocus (↑I : Set R)) : Type u) |
            Maximal (fun (x : Set (↑(zeroLocus (↑I : Set R)) : Type u)) ↦ IsClosed x ∧ IsIrreducible x) s} :
        Type u)ᵒᵈ
⊢ (↑I.minimalPrimes : Type u) ≃o (↑(irreducibleComponents (↑(zeroLocus (↑I : Set R)) : Type u)) : Type u)ᵒᵈ

Tactic:
rw [irreducibleComponents_eq_maximals_closed]

Premises used: irreducibleComponents_eq_maximals_closed
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
I : Ideal R
e : (↑{p : Ideal R | p.IsPrime ∧ I ≤ p} : Type u) ≃o (↑(zeroLocus (↑I : Set R)) : Type u) :=
  RelIso.mk (r := fun (x1 x2 : (↑{p : Ideal R | p.IsPrime ∧ I ≤ p} : Type u)) ↦ x1 ≤ x2) (s :=
    fun (x1 x2 : (↑(zeroLocus (↑I : Set R)) : Type u)) ↦ x1 ≤ x2)
    {
      toFun := fun (x : (↑{p : Ideal R | p.IsPrime ∧ I ≤ p} : Type u)) ↦
        Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
          Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) x)
          { asIdeal := (↑x : Ideal R), isPrime := ⋯ } ⋯,
      invFun := fun (x : (↑(zeroLocus (↑I : Set R)) : Type u)) ↦
        Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p.IsPrime ∧ I ≤ p} x)
          (↑x : PrimeSpectrum R).asIdeal ⋯,
      left_inv := ⋯, right_inv := ⋯ }
    ⋯
⊢ (↑I.minimalPrimes : Type u) ≃o
    (↑{s : Set (↑(zeroLocus (↑I : Set R)) : Type u) |
            Maximal (fun (x : Set (↑(zeroLocus (↑I : Set R)) : Type u)) ↦ IsClosed x ∧ IsIrreducible x) s} :
        Type u)ᵒᵈ

Tactic:
exact OrderIso.setOfMinimalIsoSetOfMaximal
    (e.trans ((PrimeSpectrum.zeroLocusEquivIrreducibleCloseds (I : Set R)).trans
    (TopologicalSpace.IrreducibleCloseds.orderIsoSubtype' (zeroLocus (I : Set R))).dual))

Premises used: PrimeSpectrum.zeroLocusEquivIrreducibleCloseds, PrimeSpectrum.zeroLocus, OrderIso.setOfMinimalIsoSetOfMaximal, Set.Elem, OrderIso.dual, SetLike.coe, TopologicalSpace.IrreducibleCloseds.orderIsoSubtype', OrderIso.trans
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
e : (↑{p : Ideal R | p.IsPrime ∧ ⊥ ≤ p} : Type u) ≃o PrimeSpectrum R :=
  RelIso.mk (r := fun (x1 x2 : (↑{p : Ideal R | p.IsPrime ∧ ⊥ ≤ p} : Type u)) ↦ x1 ≤ x2) (s :=
    fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2)
    { toFun := fun (x : (↑{p : Ideal R | p.IsPrime ∧ ⊥ ≤ p} : Type u)) ↦ { asIdeal := (↑x : Ideal R), isPrime := ⋯ },
      invFun := fun (x : PrimeSpectrum R) ↦
        Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p.IsPrime ∧ ⊥ ≤ p} x)
          x.asIdeal ⋯,
      left_inv := ⋯, right_inv := ⋯ }
    ⋯
rw :
  (↑(minimalPrimes R) : Type u) ≃o
    (↑{s : Set (PrimeSpectrum R) | Maximal (fun (x : Set (PrimeSpectrum R)) ↦ IsClosed x ∧ IsIrreducible x) s} :
        Type u)ᵒᵈ
⊢ (↑(minimalPrimes R) : Type u) ≃o (↑(irreducibleComponents (PrimeSpectrum R)) : Type u)ᵒᵈ

Tactic:
rw [irreducibleComponents_eq_maximals_closed]

Premises used: irreducibleComponents_eq_maximals_closed
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
e : (↑{p : Ideal R | p.IsPrime ∧ ⊥ ≤ p} : Type u) ≃o PrimeSpectrum R :=
  RelIso.mk (r := fun (x1 x2 : (↑{p : Ideal R | p.IsPrime ∧ ⊥ ≤ p} : Type u)) ↦ x1 ≤ x2) (s :=
    fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2)
    { toFun := fun (x : (↑{p : Ideal R | p.IsPrime ∧ ⊥ ≤ p} : Type u)) ↦ { asIdeal := (↑x : Ideal R), isPrime := ⋯ },
      invFun := fun (x : PrimeSpectrum R) ↦
        Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p.IsPrime ∧ ⊥ ≤ p} x)
          x.asIdeal ⋯,
      left_inv := ⋯, right_inv := ⋯ }
    ⋯
⊢ (↑(minimalPrimes R) : Type u) ≃o
    (↑{s : Set (PrimeSpectrum R) | Maximal (fun (x : Set (PrimeSpectrum R)) ↦ IsClosed x ∧ IsIrreducible x) s} :
        Type u)ᵒᵈ

Tactic:
exact OrderIso.setOfMinimalIsoSetOfMaximal
    (e.trans ((PrimeSpectrum.pointsEquivIrreducibleCloseds R).trans
    (TopologicalSpace.IrreducibleCloseds.orderIsoSubtype' (PrimeSpectrum R)).dual))

Premises used: PrimeSpectrum.pointsEquivIrreducibleCloseds, OrderIso.setOfMinimalIsoSetOfMaximal, OrderIso.dual, TopologicalSpace.IrreducibleCloseds.orderIsoSubtype', PrimeSpectrum, OrderIso.trans
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
rw :
  Eq.{u + 1} (α := Set (Ideal R))
    {x : Ideal R |
      Minimal
        (fun (x : Ideal R) ↦ ∃ (x₀ : Set (PrimeSpectrum R)), (IsClosed x₀ ∧ IsIrreducible x₀) ∧ vanishingIdeal x₀ = x)
        x}
    {x : Ideal R |
      Minimal
        (Membership.mem (γ := Set (Ideal R))
          (vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsClosed s ∧ IsIrreducible s}))
        x}
⊢ Eq (α := Set (Ideal R)) (vanishingIdeal '' irreducibleComponents (PrimeSpectrum R)) (minimalPrimes R)

Tactic:
rw [irreducibleComponents_eq_maximals_closed, minimalPrimes_eq_minimals,
    image_antitone_setOf_maximal (fun s t hs _ ↦ (vanishingIdeal_anti_mono_iff hs.1).symm),
    ← funext (@Set.mem_setOf_eq _ · Ideal.IsPrime), ← vanishingIdeal_isClosed_isIrreducible]

Premises used: PrimeSpectrum.vanishingIdeal_isClosed_isIrreducible, minimalPrimes_eq_minimals, PrimeSpectrum.vanishingIdeal_anti_mono_iff, Set.mem_setOf_eq, funext, image_antitone_setOf_maximal, irreducibleComponents_eq_maximals_closed, Iff.symm
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq.{u + 1} (α := Set (Ideal R))
    {x : Ideal R |
      Minimal
        (fun (x : Ideal R) ↦ ∃ (x₀ : Set (PrimeSpectrum R)), (IsClosed x₀ ∧ IsIrreducible x₀) ∧ vanishingIdeal x₀ = x)
        x}
    {x : Ideal R |
      Minimal
        (Membership.mem (γ := Set (Ideal R))
          (vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsClosed s ∧ IsIrreducible s}))
        x}

Tactic:
rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
rw :
  Set.EqOn (α := Set (PrimeSpectrum R)) ((zeroLocus ∘ SetLike.coe) ∘ vanishingIdeal) id
    (irreducibleComponents (PrimeSpectrum R))
⊢ Eq (α := Set (Set (PrimeSpectrum R))) (Set.image (α := Ideal R) (zeroLocus ∘ SetLike.coe) (minimalPrimes R))
    (irreducibleComponents (PrimeSpectrum R))

Tactic:
rw [← vanishingIdeal_irreducibleComponents, ← Set.image_comp, Set.EqOn.image_eq_self]

Premises used: PrimeSpectrum.vanishingIdeal_irreducibleComponents, Set.image_comp, Set.EqOn.image_eq_self
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
hs : Membership.mem (γ := Set (Set (PrimeSpectrum R))) (irreducibleComponents (PrimeSpectrum R)) s
⊢ ((zeroLocus ∘ SetLike.coe) ∘ vanishingIdeal) s = id s

Tactic:
simpa [zeroLocus_vanishingIdeal_eq_closure, closure_eq_iff_isClosed]
    using isClosed_of_mem_irreducibleComponents s hs

Premises used: isClosed_of_mem_irreducibleComponents, closure_eq_iff_isClosed, PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
mp :
  Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) (vanishingIdeal s) →
    Membership.mem (γ := Set (Set (PrimeSpectrum R))) (irreducibleComponents (PrimeSpectrum R)) (closure s)
mpr :
  Membership.mem (γ := Set (Set (PrimeSpectrum R))) (irreducibleComponents (PrimeSpectrum R)) (closure s) →
    Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) (vanishingIdeal s)
⊢ Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) (vanishingIdeal s) ↔
    Membership.mem (γ := Set (Set (PrimeSpectrum R))) (irreducibleComponents (PrimeSpectrum R)) (closure s)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
mp :
  Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) (vanishingIdeal s) →
    Membership.mem (γ := Set (Set (PrimeSpectrum R)))
      (Set.image (α := Ideal R) (zeroLocus ∘ SetLike.coe) (minimalPrimes R)) (zeroLocus (↑(vanishingIdeal s) : Set R))
⊢ Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) (vanishingIdeal s) →
    Membership.mem (γ := Set (Set (PrimeSpectrum R))) (irreducibleComponents (PrimeSpectrum R)) (closure s)

Tactic:
rw [← zeroLocus_minimalPrimes, ← zeroLocus_vanishingIdeal_eq_closure]

Premises used: PrimeSpectrum.zeroLocus_minimalPrimes, PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) (vanishingIdeal s) →
    Membership.mem (γ := Set (Set (PrimeSpectrum R)))
      (Set.image (α := Ideal R) (zeroLocus ∘ SetLike.coe) (minimalPrimes R)) (zeroLocus (↑(vanishingIdeal s) : Set R))

Tactic:
Set.mem_image_of_mem _

Premises used: PrimeSpectrum.zeroLocus, Set.Mem, setOf, Set.mem_image_of_mem
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) (vanishingIdeal s) →
    Membership.mem (γ := Set (Set (PrimeSpectrum R)))
      (Set.image (α := Ideal R) (zeroLocus ∘ SetLike.coe) (minimalPrimes R)) (zeroLocus (↑(vanishingIdeal s) : Set R))

Tactic:
exact Set.mem_image_of_mem _

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
mpr :
  Membership.mem (γ := Set (Set (PrimeSpectrum R))) (irreducibleComponents (PrimeSpectrum R)) (closure s) →
    Membership.mem (γ := Set (Ideal R)) (vanishingIdeal '' irreducibleComponents (PrimeSpectrum R))
      (vanishingIdeal (closure s))
⊢ Membership.mem (γ := Set (Set (PrimeSpectrum R))) (irreducibleComponents (PrimeSpectrum R)) (closure s) →
    Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) (vanishingIdeal s)

Tactic:
rw [← vanishingIdeal_irreducibleComponents, ← vanishingIdeal_closure]

Premises used: PrimeSpectrum.vanishingIdeal_irreducibleComponents, PrimeSpectrum.vanishingIdeal_closure
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ Membership.mem (γ := Set (Set (PrimeSpectrum R))) (irreducibleComponents (PrimeSpectrum R)) (closure s) →
    Membership.mem (γ := Set (Ideal R)) (vanishingIdeal '' irreducibleComponents (PrimeSpectrum R))
      (vanishingIdeal (closure s))

Tactic:
Set.mem_image_of_mem _

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ Membership.mem (γ := Set (Set (PrimeSpectrum R))) (irreducibleComponents (PrimeSpectrum R)) (closure s) →
    Membership.mem (γ := Set (Ideal R)) (vanishingIdeal '' irreducibleComponents (PrimeSpectrum R))
      (vanishingIdeal (closure s))

Tactic:
exact Set.mem_image_of_mem _

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
rw :
  Membership.mem (γ := Set (Set (PrimeSpectrum R))) (irreducibleComponents (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) ↔
    Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) (vanishingIdeal (zeroLocus (↑I : Set R)))
⊢ Membership.mem (γ := Set (Set (PrimeSpectrum R))) (irreducibleComponents (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) ↔
    Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) I.radical

Tactic:
rw [← vanishingIdeal_zeroLocus_eq_radical]

Premises used: PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
rw :
  Membership.mem (γ := Set (Set (PrimeSpectrum R))) (irreducibleComponents (PrimeSpectrum R))
    (closure (zeroLocus (↑I : Set R)))
| Membership.mem (γ := Set (Set (PrimeSpectrum R))) (irreducibleComponents (PrimeSpectrum R)) (zeroLocus (↑I : Set R))

Tactic:
rw [← (isClosed_zeroLocus _).closure_eq]

Premises used: PrimeSpectrum.isClosed_zeroLocus, IsClosed.closure_eq
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
conv_lhs :
  Membership.mem (γ := Set (Set (PrimeSpectrum R))) (irreducibleComponents (PrimeSpectrum R))
      (closure (zeroLocus (↑I : Set R))) ↔
    Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) (vanishingIdeal (zeroLocus (↑I : Set R)))
⊢ Membership.mem (γ := Set (Set (PrimeSpectrum R))) (irreducibleComponents (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) ↔
    Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) (vanishingIdeal (zeroLocus (↑I : Set R)))

Tactic:
conv_lhs => rw [← (isClosed_zeroLocus _).closure_eq]

Premises used: PrimeSpectrum.isClosed_zeroLocus, IsClosed.closure_eq
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
⊢ Membership.mem (γ := Set (Set (PrimeSpectrum R))) (irreducibleComponents (PrimeSpectrum R))
      (closure (zeroLocus (↑I : Set R))) ↔
    Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) (vanishingIdeal (zeroLocus (↑I : Set R)))

Tactic:
vanishingIdeal_mem_minimalPrimes.symm

Premises used: Iff.symm, PrimeSpectrum.vanishingIdeal_mem_minimalPrimes
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
⊢ Membership.mem (γ := Set (Set (PrimeSpectrum R))) (irreducibleComponents (PrimeSpectrum R))
      (closure (zeroLocus (↑I : Set R))) ↔
    Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) (vanishingIdeal (zeroLocus (↑I : Set R)))

Tactic:
exact vanishingIdeal_mem_minimalPrimes.symm

Premises used: Iff.symm, PrimeSpectrum.vanishingIdeal_mem_minimalPrimes
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsLocalRing R
⊢ Eq (α := Ideal R) (PrimeSpectrum.asIdeal ⊤) (maximalIdeal R)

Tactic:
rfl

Premises used: IsLocalRing.maximalIdeal, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsLocalRing R
S : Type v
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
⊢ IsLocalHom (R := R) (S := S) f ↔ Eq (α := Ideal R) (Ideal.comap f (maximalIdeal S)) (maximalIdeal R)

Tactic:
have := (local_hom_TFAE f).out 0 4
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsLocalRing R
S : Type v
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
this : IsLocalHom (R := R) (S := S) f ↔ Eq (α := Ideal R) (Ideal.comap f (maximalIdeal S)) (maximalIdeal R)
rw :
  Eq (α := Ideal R) (Ideal.comap f (maximalIdeal S)) (maximalIdeal R) ↔
    (PrimeSpectrum.comap f (closedPoint S)).asIdeal = PrimeSpectrum.asIdeal (closedPoint R)
⊢ IsLocalHom (R := R) (S := S) f ↔ PrimeSpectrum.comap f (closedPoint S) = closedPoint R

Tactic:
rw [this, PrimeSpectrum.ext_iff]

Premises used: PrimeSpectrum.ext_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsLocalRing R
S : Type v
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
this : IsLocalHom (R := R) (S := S) f ↔ Eq (α := Ideal R) (Ideal.comap f (maximalIdeal S)) (maximalIdeal R)
⊢ Eq (α := Ideal R) (Ideal.comap f (maximalIdeal S)) (maximalIdeal R) ↔
    (PrimeSpectrum.comap f (closedPoint S)).asIdeal = PrimeSpectrum.asIdeal (closedPoint R)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsLocalRing R
S : Type v
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
inst_4 : IsLocalHom (R := R) (S := S) f
⊢ PrimeSpectrum.comap f (closedPoint S) = closedPoint R

Tactic:
(isLocalHom_iff_comap_closedPoint f).mp inferInstance

Premises used: inferInstance, IsLocalRing.isLocalHom_iff_comap_closedPoint, Iff.mp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsLocalRing R
x : PrimeSpectrum R
⊢ x ⤳ closedPoint R

Tactic:
(PrimeSpectrum.le_iff_specializes _ _).mp (IsLocalRing.le_maximalIdeal x.2.1)

Premises used: PrimeSpectrum.le_iff_specializes, IsLocalRing.le_maximalIdeal, Iff.mp, Ideal.IsPrime.ne_top'
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsLocalRing R
U : TopologicalSpace.Opens (PrimeSpectrum R)
mp : closedPoint R ∈ U → U = ⊤
mpr : U = ⊤ → closedPoint R ∈ U
⊢ closedPoint R ∈ U ↔ U = ⊤

Tactic:
constructor
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsLocalRing R
U : TopologicalSpace.Opens (PrimeSpectrum R)
mp : closedPoint R ∈ U → ⊤ ≤ U
⊢ closedPoint R ∈ U → U = ⊤

Tactic:
rw [eq_top_iff]

Premises used: eq_top_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsLocalRing R
U : TopologicalSpace.Opens (PrimeSpectrum R)
⊢ closedPoint R ∈ U → ⊤ ≤ U

Tactic:
fun h x _ => (specializes_closedPoint x).mem_open U.2 h

Premises used: Specializes.mem_open, IsLocalRing.specializes_closedPoint, TopologicalSpace.Opens.is_open'
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsLocalRing R
U : TopologicalSpace.Opens (PrimeSpectrum R)
⊢ closedPoint R ∈ U → ⊤ ≤ U

Tactic:
exact fun h x _ => (specializes_closedPoint x).mem_open U.2 h

Premises used: Specializes.mem_open, IsLocalRing.specializes_closedPoint, TopologicalSpace.Opens.is_open'
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsLocalRing R
⊢ Membership.mem (γ := TopologicalSpace.Opens (PrimeSpectrum R)) ⊤ (closedPoint R)

Tactic:
TopologicalSpace.Opens.mem_top _

Premises used: TopologicalSpace.Opens.mem_top
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsLocalRing R
⊢ Membership.mem (γ := TopologicalSpace.Opens (PrimeSpectrum R)) ⊤ (closedPoint R)

Tactic:
exact TopologicalSpace.Opens.mem_top _

Premises used: TopologicalSpace.Opens.mem_top
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsLocalRing R
U : TopologicalSpace.Opens (PrimeSpectrum R)
⊢ closedPoint R ∈ U ↔ U = ⊤

Tactic:
⟨(eq_top_iff.mpr fun x _ ↦ (specializes_closedPoint x).mem_open U.2 ·), (· ▸ trivial)⟩

Premises used: Iff.mpr, trivial, eq_top_iff, Specializes.mem_open, Eq.rec, IsLocalRing.specializes_closedPoint, Iff.intro, TopologicalSpace.Opens.is_open', Eq.symm
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
T : Type u
inst : CommRing T
inst_1 : IsLocalRing T
x : PrimeSpectrum (ResidueField T)
rw : Eq (α := PrimeSpectrum T) (PrimeSpectrum.comap (S := ResidueField T) (residue T) ⊥) (closedPoint T)
⊢ PrimeSpectrum.comap (residue T) x = closedPoint T

Tactic:
rw [Subsingleton.elim x ⊥]

Premises used: Bot.bot, Subsingleton.elim
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
T : Type u
inst : CommRing T
inst_1 : IsLocalRing T
x : PrimeSpectrum (ResidueField T)
asIdeal :
  Eq (α := Ideal T) (PrimeSpectrum.asIdeal (PrimeSpectrum.comap (S := ResidueField T) (residue T) ⊥))
    (PrimeSpectrum.asIdeal (closedPoint T))
⊢ Eq (α := PrimeSpectrum T) (PrimeSpectrum.comap (S := ResidueField T) (residue T) ⊥) (closedPoint T)

Tactic:
ext1