awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
refine :
  ∀ (e f : R),
    f * e = 0 ∧ f + e = 1 ∧ s = (↑(basicOpen f) : Set (PrimeSpectrum R)) ↔ e * f = 0 ∧ e + f = 1 ∧ s = zeroLocus {e}
⊢ (∃ (b : R) (a : R), a * b = 0 ∧ a + b = 1 ∧ s = (↑(basicOpen a) : Set (PrimeSpectrum R))) ↔
    ∃ (e : R) (f : R), e * f = 0 ∧ e + f = 1 ∧ s = zeroLocus {e}

Tactic:
refine exists₂_congr fun e f ↦ ?_

Premises used: exists₂_congr
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
e f : R
rw : e * f = 0 ∧ e + f = 1 → (s = (↑(basicOpen f) : Set (PrimeSpectrum R)) ↔ s = zeroLocus {e})
⊢ f * e = 0 ∧ f + e = 1 ∧ s = (↑(basicOpen f) : Set (PrimeSpectrum R)) ↔ e * f = 0 ∧ e + f = 1 ∧ s = zeroLocus {e}

Tactic:
rw [mul_comm, add_comm, ← and_assoc, ← and_assoc, and_congr_right]

Premises used: and_congr_right, add_comm, and_assoc, mul_comm
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
e f : R
mul : e * f = 0
add : e + f = 1
rw rw₁ : s = (↑(basicOpen f) : Set (PrimeSpectrum R)) ↔ s = (↑(basicOpen f) : Set (PrimeSpectrum R))
⊢ s = (↑(basicOpen f) : Set (PrimeSpectrum R)) ↔ s = zeroLocus {e}

Tactic:
rw [zeroLocus_eq_basicOpen_of_mul_add e f mul add]

Premises used: PrimeSpectrum.zeroLocus_eq_basicOpen_of_mul_add
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
⊢ Function.Bijective (β := Clopens (PrimeSpectrum R)) fun (e : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }) ↦
    { carrier := (↑(basicOpen (↑e : R × R).1) : Set (PrimeSpectrum R)), isClopen' := ⋯ }

Tactic:
⟨fun ⟨x, hx⟩ ⟨y, hy⟩ eq ↦ mul_eq_zero_add_eq_one_ext_left ?_, fun s ↦ ?_⟩

Premises used: Subtype.mk, _private.0.PrimeSpectrum.mulZeroAddOneEquivClopens.match_2, _private.0.PrimeSpectrum.mulZeroAddOneEquivClopens.match_1, And.intro, Function.Bijective, mul_eq_zero_add_eq_one_ext_left, Eq
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
refine_1 :
  ∀ (x x : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }) (x : R × R) (hx : x.1 * x.2 = 0 ∧ x.1 + x.2 = 1) (y : R × R)
    (hy : y.1 * y.2 = 0 ∧ y.1 + y.2 = 1)
    (eq :
      Eq.{u + 1} (α := Clopens (PrimeSpectrum R))
        ((fun (e : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }) ↦
            { carrier := (↑(basicOpen (↑e : R × R).1) : Set (PrimeSpectrum R)), isClopen' := ⋯ :
              Clopens (PrimeSpectrum R) })
          (Subtype.mk (p := fun (e : R × R) ↦ e.1 * e.2 = 0 ∧ e.1 + e.2 = 1) x hx))
        ((fun (e : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }) ↦
            { carrier := (↑(basicOpen (↑e : R × R).1) : Set (PrimeSpectrum R)), isClopen' := ⋯ :
              Clopens (PrimeSpectrum R) })
          (Subtype.mk (p := fun (e : R × R) ↦ e.1 * e.2 = 0 ∧ e.1 + e.2 = 1) y hy))),
    (↑(Subtype.mk (p := fun (e : R × R) ↦ e.1 * e.2 = 0 ∧ e.1 + e.2 = 1) x hx) : R × R).1 =
      (↑(Subtype.mk (p := fun (e : R × R) ↦ e.1 * e.2 = 0 ∧ e.1 + e.2 = 1) y hy) : R × R).1
refine_2 :
  ∀ (s : Clopens (PrimeSpectrum R)),
    ∃ (a : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }),
      (fun (e : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }) ↦
            { carrier := (↑(basicOpen (↑e : R × R).1) : Set (PrimeSpectrum R)), isClopen' := ⋯ :
              Clopens (PrimeSpectrum R) })
          a =
        s
⊢ Function.Bijective (β := Clopens (PrimeSpectrum R)) fun (e : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }) ↦
    { carrier := (↑(basicOpen (↑e : R × R).1) : Set (PrimeSpectrum R)), isClopen' := ⋯ }

Tactic:
refine ⟨fun ⟨x, hx⟩ ⟨y, hy⟩ eq ↦ mul_eq_zero_add_eq_one_ext_left ?_, fun s ↦ ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
x_1 x_2 : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }
x : R × R
hx : x.1 * x.2 = 0 ∧ x.1 + x.2 = 1
y : R × R
hy : y.1 * y.2 = 0 ∧ y.1 + y.2 = 1
eq :
  Eq.{u + 1} (α := Clopens (PrimeSpectrum R))
    ((fun (e : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }) ↦
        { carrier := (↑(basicOpen (↑e : R × R).1) : Set (PrimeSpectrum R)), isClopen' := ⋯ :
          Clopens (PrimeSpectrum R) })
      (Subtype.mk (p := fun (e : R × R) ↦ e.1 * e.2 = 0 ∧ e.1 + e.2 = 1) x hx))
    ((fun (e : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }) ↦
        { carrier := (↑(basicOpen (↑e : R × R).1) : Set (PrimeSpectrum R)), isClopen' := ⋯ :
          Clopens (PrimeSpectrum R) })
      (Subtype.mk (p := fun (e : R × R) ↦ e.1 * e.2 = 0 ∧ e.1 + e.2 = 1) y hy))
⊢ (↑(Subtype.mk (p := fun (e : R × R) ↦ e.1 * e.2 = 0 ∧ e.1 + e.2 = 1) x hx) : R × R).1 =
    (↑(Subtype.mk (p := fun (e : R × R) ↦ e.1 * e.2 = 0 ∧ e.1 + e.2 = 1) y hy) : R × R).1

Tactic:
basicOpen_injOn_isIdempotentElem (IsIdempotentElem.of_mul_add hx.1 hx.2).1
          (IsIdempotentElem.of_mul_add hy.1 hy.2).1 <| SetLike.ext' (congr_arg (·.1) eq)

Premises used: IsIdempotentElem.of_mul_add, PrimeSpectrum.basicOpen_injOn_isIdempotentElem, SetLike.ext', And.right, And.left
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
x_1 x_2 : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }
x : R × R
hx : x.1 * x.2 = 0 ∧ x.1 + x.2 = 1
y : R × R
hy : y.1 * y.2 = 0 ∧ y.1 + y.2 = 1
eq :
  Eq.{u + 1} (α := Clopens (PrimeSpectrum R))
    ((fun (e : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }) ↦
        { carrier := (↑(basicOpen (↑e : R × R).1) : Set (PrimeSpectrum R)), isClopen' := ⋯ :
          Clopens (PrimeSpectrum R) })
      (Subtype.mk (p := fun (e : R × R) ↦ e.1 * e.2 = 0 ∧ e.1 + e.2 = 1) x hx))
    ((fun (e : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }) ↦
        { carrier := (↑(basicOpen (↑e : R × R).1) : Set (PrimeSpectrum R)), isClopen' := ⋯ :
          Clopens (PrimeSpectrum R) })
      (Subtype.mk (p := fun (e : R × R) ↦ e.1 * e.2 = 0 ∧ e.1 + e.2 = 1) y hy))
⊢ (↑(Subtype.mk (p := fun (e : R × R) ↦ e.1 * e.2 = 0 ∧ e.1 + e.2 = 1) x hx) : R × R).1 =
    (↑(Subtype.mk (p := fun (e : R × R) ↦ e.1 * e.2 = 0 ∧ e.1 + e.2 = 1) y hy) : R × R).1

Tactic:
exact basicOpen_injOn_isIdempotentElem (IsIdempotentElem.of_mul_add hx.1 hx.2).1
          (IsIdempotentElem.of_mul_add hy.1 hy.2).1 <| SetLike.ext' (congr_arg (·.1) eq)

Premises used: IsIdempotentElem.of_mul_add, PrimeSpectrum.basicOpen_injOn_isIdempotentElem, SetLike.ext', And.right, And.left
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
s : Clopens (PrimeSpectrum R)
refine_2 :
  ∀ (e f : R) (mul : e * f = 0) (add : e + f = 1) (eq : s.carrier = (↑(basicOpen e) : Set (PrimeSpectrum R))),
    ∃ (a : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }),
      (fun (e : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }) ↦
            { carrier := (↑(basicOpen (↑e : R × R).1) : Set (PrimeSpectrum R)), isClopen' := ⋯ :
              Clopens (PrimeSpectrum R) })
          a =
        s
⊢ ∃ (a : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }),
    (fun (e : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }) ↦
          { carrier := (↑(basicOpen (↑e : R × R).1) : Set (PrimeSpectrum R)), isClopen' := ⋯ :
            Clopens (PrimeSpectrum R) })
        a =
      s

Tactic:
have ⟨e, f, mul, add, eq⟩ := isClopen_iff_mul_add.mp s.2
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
s : Clopens (PrimeSpectrum R)
e f : R
mul : e * f = 0
add : e + f = 1
eq : s.carrier = (↑(basicOpen e) : Set (PrimeSpectrum R))
⊢ ∃ (a : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }),
    (fun (e : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }) ↦
          { carrier := (↑(basicOpen (↑e : R × R).1) : Set (PrimeSpectrum R)), isClopen' := ⋯ :
            Clopens (PrimeSpectrum R) })
        a =
      s

Tactic:
⟨⟨(e, f), mul, add⟩, SetLike.ext' eq.symm⟩

Premises used: Prod.mk, SetLike.ext', Subtype.mk, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
s : Clopens (PrimeSpectrum R)
e f : R
mul : e * f = 0
add : e + f = 1
eq : s.carrier = (↑(basicOpen e) : Set (PrimeSpectrum R))
⊢ ∃ (a : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }),
    (fun (e : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }) ↦
          { carrier := (↑(basicOpen (↑e : R × R).1) : Set (PrimeSpectrum R)), isClopen' := ⋯ :
            Clopens (PrimeSpectrum R) })
        a =
      s

Tactic:
exact ⟨⟨(e, f), mul, add⟩, SetLike.ext' eq.symm⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
a b : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }
rw :
  Eq (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen ((↑a : R × R).1 * (↑b : R × R).1))
      (basicOpen (↑a : R × R).1) ↔
    a ≤ b
⊢ LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen (↑a : R × R).1) (basicOpen (↑b : R × R).1) ↔ a ≤ b

Tactic:
rw [← inf_eq_left, ← basicOpen_mul]

Premises used: PrimeSpectrum.basicOpen_mul, inf_eq_left
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
a b : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }
refine :
  ∀
    (h :
      Eq (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen ((↑a : R × R).1 * (↑b : R × R).1))
        (basicOpen (↑a : R × R).1)),
    a ≤ b
⊢ Eq (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen ((↑a : R × R).1 * (↑b : R × R).1))
      (basicOpen (↑a : R × R).1) ↔
    a ≤ b

Tactic:
refine ⟨fun h ↦ ?_, (by rw [·])⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
a b : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }
h :
  Eq (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen ((↑a : R × R).1 * (↑b : R × R).1))
    (basicOpen (↑a : R × R).1)
rw : a ⊓ b = a
⊢ a ≤ b

Tactic:
rw [← inf_eq_left]

Premises used: inf_eq_left
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
a b : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }
h :
  Eq (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen ((↑a : R × R).1 * (↑b : R × R).1))
    (basicOpen (↑a : R × R).1)
⊢ IsIdempotentElem (↑a : R × R).1

Tactic:
have := (IsIdempotentElem.of_mul_add a.2.1 a.2.2).1
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
a b : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }
h :
  Eq (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen ((↑a : R × R).1 * (↑b : R × R).1))
    (basicOpen (↑a : R × R).1)
this : IsIdempotentElem (↑a : R × R).1
⊢ a ⊓ b = a

Tactic:
mul_eq_zero_add_eq_one_ext_left (basicOpen_injOn_isIdempotentElem
      (this.mul (IsIdempotentElem.of_mul_add b.2.1 b.2.2).1) this h)

Premises used: IsIdempotentElem.of_mul_add, PrimeSpectrum.basicOpen_injOn_isIdempotentElem, IsIdempotentElem.mul, And.right, And.left, mul_eq_zero_add_eq_one_ext_left, Subtype.property
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
a b : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }
h :
  Eq (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen ((↑a : R × R).1 * (↑b : R × R).1))
    (basicOpen (↑a : R × R).1)
this : IsIdempotentElem (↑a : R × R).1
⊢ a ⊓ b = a

Tactic:
exact mul_eq_zero_add_eq_one_ext_left (basicOpen_injOn_isIdempotentElem
      (this.mul (IsIdempotentElem.of_mul_add b.2.1 b.2.2).1) this h)

Premises used: mul_eq_zero_add_eq_one_ext_left
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set R
hs : s.Finite
⊢ Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑(hs.toFinset (s := s)) : Set R))ᶜ (zeroLocus s)ᶜ

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
hI : I.FG
obtain : ∀ (s : Finset R), IsRetrocompact (X := PrimeSpectrum R) (zeroLocus (↑(Ideal.span (↑s : Set R)) : Set R))ᶜ
⊢ IsRetrocompact (X := PrimeSpectrum R) (zeroLocus (↑I : Set R))ᶜ

Tactic:
obtain ⟨s, rfl⟩ := hI

Premises used: rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Finset R
rw : IsRetrocompact (X := PrimeSpectrum R) (zeroLocus (↑s : Set R))ᶜ
⊢ IsRetrocompact (X := PrimeSpectrum R) (zeroLocus (↑(Ideal.span (↑s : Set R)) : Set R))ᶜ

Tactic:
rw [zeroLocus_span]

Premises used: PrimeSpectrum.zeroLocus_span
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Finset R
⊢ IsRetrocompact (X := PrimeSpectrum R) (zeroLocus (↑s : Set R))ᶜ

Tactic:
isRetrocompact_zeroLocus_compl s.finite_toSet

Premises used: PrimeSpectrum.isRetrocompact_zeroLocus_compl, Finset.finite_toSet
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Finset R
⊢ IsRetrocompact (X := PrimeSpectrum R) (zeroLocus (↑s : Set R))ᶜ

Tactic:
exact isRetrocompact_zeroLocus_compl s.finite_toSet

Premises used: PrimeSpectrum.isRetrocompact_zeroLocus_compl, Finset.finite_toSet
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
f : R
⊢ IsRetrocompact (↑(basicOpen f) : Set (PrimeSpectrum R))

Tactic:
simpa using isRetrocompact_zeroLocus_compl (Set.finite_singleton f)

Premises used: PrimeSpectrum.isRetrocompact_zeroLocus_compl, Set.finite_singleton
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
f : R
⊢ IsConstructible (↑(basicOpen f) : Set (PrimeSpectrum R))

Tactic:
isRetrocompact_basicOpen.isConstructible (basicOpen f).2

Premises used: PrimeSpectrum.basicOpen, TopologicalSpace.Opens.is_open', IsRetrocompact.isConstructible, PrimeSpectrum.isRetrocompact_basicOpen
-- 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
⊢ IsClosedMap (comap f)

Tactic:
fun s hs ↦ isClosed_image_of_stableUnderSpecialization _ _ hs ?_

Premises used: IsClosedMap, PrimeSpectrum.isClosed_image_of_stableUnderSpecialization
-- 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
refine : ∀ (s : Set (PrimeSpectrum S)) (hs : IsClosed s), StableUnderSpecialization (comap f '' s)
⊢ IsClosedMap (comap f)

Tactic:
refine fun s hs ↦ isClosed_image_of_stableUnderSpecialization _ _ hs ?_

Premises used: PrimeSpectrum.isClosed_image_of_stableUnderSpecialization
-- 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
s : Set (PrimeSpectrum S)
hs : IsClosed s
y : PrimeSpectrum R
x : PrimeSpectrum S
hx : x ∈ s
e : comap f x ⤳ y
⊢ 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
s : Set (PrimeSpectrum S)
hs : IsClosed s
y : PrimeSpectrum R
x : PrimeSpectrum S
hx : x ∈ s
e : comap f x ⤳ y
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.IsIntegral R S
obtain :
  ∀ (q : Ideal S) (hq₁ : q ≥ x.asIdeal) (hq₂ : q.IsPrime)
    (hq₃ : Ideal.comap (F := R →+* S) (algebraMap R S) q = y.asIdeal), y ∈ comap f '' s
⊢ y ∈ comap f '' s

Tactic:
obtain ⟨q, hq₁, hq₂, hq₃⟩ := Ideal.exists_ideal_over_prime_of_isIntegral y.asIdeal x.asIdeal
    ((le_iff_specializes _ _).mpr e)

Premises used: Iff.mpr, PrimeSpectrum.le_iff_specializes, Ideal.exists_ideal_over_prime_of_isIntegral, PrimeSpectrum.asIdeal
-- 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
s : Set (PrimeSpectrum S)
hs : IsClosed s
y : PrimeSpectrum R
x : PrimeSpectrum S
hx : x ∈ s
e : comap f x ⤳ y
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.IsIntegral R S
q : Ideal S
hq₁ : q ≥ x.asIdeal
hq₂ : q.IsPrime
hq₃ : Ideal.comap (F := R →+* S) (algebraMap R S) q = y.asIdeal
⊢ y ∈ comap f '' s

Tactic:
⟨⟨q, hq₂⟩, ((le_iff_specializes _ ⟨q, hq₂⟩).mp hq₁).mem_closed hs hx,
    PrimeSpectrum.ext hq₃⟩

Premises used: PrimeSpectrum.mk, PrimeSpectrum.ext, Set.Mem, setOf, PrimeSpectrum.le_iff_specializes, And.intro, Exists.intro, Iff.mp, Set.image, Specializes.mem_closed
-- 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
s : Set (PrimeSpectrum S)
hs : IsClosed s
y : PrimeSpectrum R
x : PrimeSpectrum S
hx : x ∈ s
e : comap f x ⤳ y
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.IsIntegral R S
q : Ideal S
hq₁ : q ≥ x.asIdeal
hq₂ : q.IsPrime
hq₃ : Ideal.comap (F := R →+* S) (algebraMap R S) q = y.asIdeal
⊢ y ∈ comap f '' s

Tactic:
refine ⟨⟨q, hq₂⟩, ((le_iff_specializes _ ⟨q, hq₂⟩).mp hq₁).mem_closed hs hx,
    PrimeSpectrum.ext hq₃⟩
-- 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
x : PrimeSpectrum S
hx : IsClosed (X := PrimeSpectrum S) {x}
⊢ IsClosed (X := PrimeSpectrum R) {comap f x}

Tactic:
simpa using isClosedMap_comap_of_isIntegral f hf _ hx

Premises used: PrimeSpectrum.isClosedMap_comap_of_isIntegral
-- 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
I : Ideal S
a : closure (comap f '' zeroLocus (↑I : Set S)) ⊆ zeroLocus (↑(Ideal.comap f I) : Set R)
a₁ : zeroLocus (↑(Ideal.comap f I) : Set R) ⊆ closure (comap f '' zeroLocus (↑I : Set S))
⊢ closure (comap f '' zeroLocus (↑I : Set S)) = zeroLocus (↑(Ideal.comap f I) : Set R)

Tactic:
apply subset_antisymm

Premises used: subset_antisymm
-- 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
I : Ideal S
a :
  Subset (α := Set (PrimeSpectrum S)) (zeroLocus (↑I : Set S))
    (zeroLocus ((⇑f : (a : R) → S) '' (↑(Ideal.comap f I) : Set R)))
⊢ closure (comap f '' zeroLocus (↑I : Set S)) ⊆ zeroLocus (↑(Ideal.comap f I) : Set R)

Tactic:
rw [(isClosed_zeroLocus _).closure_subset_iff, Set.image_subset_iff, preimage_comap_zeroLocus]

Premises used: PrimeSpectrum.isClosed_zeroLocus, PrimeSpectrum.preimage_comap_zeroLocus, IsClosed.closure_subset_iff, Set.image_subset_iff
-- 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
I : Ideal S
⊢ Subset (α := Set (PrimeSpectrum S)) (zeroLocus (↑I : Set S))
    (zeroLocus ((⇑f : (a : R) → S) '' (↑(Ideal.comap f I) : Set R)))

Tactic:
zeroLocus_anti_mono (Set.image_preimage_subset _ _)

Premises used: PrimeSpectrum.zeroLocus_anti_mono, Set.image_preimage_subset
-- 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
I : Ideal S
⊢ Subset (α := Set (PrimeSpectrum S)) (zeroLocus (↑I : Set S))
    (zeroLocus ((⇑f : (a : R) → S) '' (↑(Ideal.comap f I) : Set R)))

Tactic:
exact zeroLocus_anti_mono (Set.image_preimage_subset _ _)

Premises used: PrimeSpectrum.zeroLocus_anti_mono, Set.image_preimage_subset
-- 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
I : Ideal S
x : PrimeSpectrum R
hx : Ideal.comap f I ≤ x.asIdeal
a :
  ∀ (q : Ideal R) (hq₁ : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (Ideal.comap f I)) q)
    (hq₂ : q ≤ x.asIdeal), x ∈ closure (comap f '' zeroLocus (↑I : Set S))
⊢ x ∈ closure (comap f '' zeroLocus (↑I : Set S))

Tactic:
obtain ⟨q, hq₁, hq₂⟩ := Ideal.exists_minimalPrimes_le hx

Premises used: Ideal.exists_minimalPrimes_le
-- 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
I : Ideal S
x : PrimeSpectrum R
hx : Ideal.comap f I ≤ x.asIdeal
q : Ideal R
hq₁ : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (Ideal.comap f I)) q
hq₂ : q ≤ x.asIdeal
a :
  ∀ (p' : Ideal S) (hp' : p'.IsPrime) (hp'' : I ≤ p')
    (hq₁ : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (Ideal.comap f I)) (Ideal.comap f p'))
    (hq₂ : Ideal.comap f p' ≤ x.asIdeal), x ∈ closure (comap f '' zeroLocus (↑I : Set S))
⊢ x ∈ closure (comap f '' zeroLocus (↑I : Set S))

Tactic:
obtain ⟨p', hp', hp'', rfl⟩ := Ideal.exists_comap_eq_of_mem_minimalPrimes f _ hq₁

Premises used: Ideal.exists_comap_eq_of_mem_minimalPrimes, 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
I : Ideal S
x : PrimeSpectrum R
hx : Ideal.comap f I ≤ x.asIdeal
p' : Ideal S
hp' : p'.IsPrime
hp'' : I ≤ p'
hq₁ : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (Ideal.comap f I)) (Ideal.comap f p')
hq₂ : Ideal.comap f p' ≤ x.asIdeal
p'' : PrimeSpectrum S := { asIdeal := p', isPrime := hp' }
⊢ comap f { asIdeal := p', isPrime := hp' : PrimeSpectrum S } ∈ comap f '' zeroLocus (↑I : Set S)

Tactic:
⟨_, hp'', rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, 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
I : Ideal S
x : PrimeSpectrum R
hx : Ideal.comap f I ≤ x.asIdeal
p' : Ideal S
hp' : p'.IsPrime
hp'' : I ≤ p'
hq₁ : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (Ideal.comap f I)) (Ideal.comap f p')
hq₂ : Ideal.comap f p' ≤ x.asIdeal
p'' : PrimeSpectrum S := { asIdeal := p', isPrime := hp' }
⊢ comap f { asIdeal := p', isPrime := hp' : PrimeSpectrum S } ∈ comap f '' zeroLocus (↑I : Set S)

Tactic:
exact ⟨_, hp'', 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
I : Ideal S
x : PrimeSpectrum R
hx : Ideal.comap f I ≤ x.asIdeal
p' : Ideal S
hp' : p'.IsPrime
hp'' : I ≤ p'
hq₁ : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (Ideal.comap f I)) (Ideal.comap f p')
hq₂ : Ideal.comap f p' ≤ x.asIdeal
p'' : PrimeSpectrum S := { asIdeal := p', isPrime := hp' }
⊢ x ∈ closure (comap f '' zeroLocus (↑I : Set S))

Tactic:
apply isClosed_closure.stableUnderSpecialization ((le_iff_specializes
      (comap f ⟨p', hp'⟩) x).mp hq₂) (subset_closure (by exact ⟨_, hp'', rfl⟩))

Premises used: PrimeSpectrum.mk, subset_closure, PrimeSpectrum.le_iff_specializes, IsClosed.stableUnderSpecialization, Iff.mp, PrimeSpectrum.comap, isClosed_closure
-- 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
h : IsClosedMap (comap (mapRingHom f))
algInst : Algebra R S := f.toAlgebra
this : Algebra.IsIntegral R S
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : ∀ (x : S), IsIntegral R x), f.IsIntegral
⊢ f.IsIntegral

Tactic:
rwa [Algebra.isIntegral_def] at this

Premises used: Algebra.isIntegral_def
-- 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
h : IsClosedMap (comap (mapRingHom f))
algInst : Algebra R S := f.toAlgebra
suffices : Algebra.IsIntegral R S
⊢ f.IsIntegral

Tactic:
suffices Algebra.IsIntegral R S by rwa [Algebra.isIntegral_def] at this
-- 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
h : IsClosedMap (comap (mapRingHom f))
algInst : Algebra R S := f.toAlgebra
⊢ Nontrivial R

Tactic:
nontriviality R
-- 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
h : IsClosedMap (comap (mapRingHom f))
algInst : Algebra R S := f.toAlgebra
h_1 : Nontrivial R
⊢ Nontrivial S

Tactic:
nontriviality S