awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_4
inst : (i : ι) → CommRing (R i)
inst_1 : _root_.Finite ι
p : PrimeSpectrum ((i : ι) → R i)
intro : ∀ (val : Fintype ι), ∃ (i : ι) (q : PrimeSpectrum (R i)), comap (Pi.evalRingHom R i) q = p
intro₁ : ∀ (val : Fintype ι), ∃ (i : ι) (q : PrimeSpectrum (R i)), comap (Pi.evalRingHom R i) q = p
intro₂ :
  ∀ (val : Fintype ι),
    let e : (i i : ι) → R i := fun (i : ι) ↦ Function.update (β := R) 1 i 0;
    ∀ (H : Eq (α := (i : ι) → R i) (∏ i : ι, e i) 0),
      ∃ (i : ι) (q : PrimeSpectrum (R i)), comap (Pi.evalRingHom R i) q = p
intro₃ intro₄ :
  ∀ (val : Fintype ι),
    let e : (i i : ι) → R i := fun (i : ι) ↦ Function.update (β := R) 1 i 0;
    ∀ (H : Eq (α := (i : ι) → R i) (∏ i : ι, e i) 0) (i : ι) (hi : e i ∈ p.asIdeal),
      ∃ (i : ι) (q : PrimeSpectrum (R i)), comap (Pi.evalRingHom R i) q = p
intro₅ :
  ∀ (val : Fintype ι),
    let e : (i i : ι) → R i := fun (i : ι) ↦ Function.update (β := R) 1 i 0;
    ∀ (H : Eq (α := (i : ι) → R i) (∏ i : ι, e i) 0) (i : ι) (hi : e i ∈ p.asIdeal)
      (h₂ : ker (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) ≤ p.asIdeal),
      ∃ (i : ι) (q : PrimeSpectrum (R i)), comap (Pi.evalRingHom R i) q = p
intro₆ :
  ∀ (val : Fintype ι),
    let e : (i i : ι) → R i := fun (i : ι) ↦ Function.update (β := R) 1 i 0;
    ∀ (H : Eq (α := (i : ι) → R i) (∏ i : ι, e i) 0) (i : ι) (hi : e i ∈ p.asIdeal)
      (h₂ : ker (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) ≤ p.asIdeal)
      (this :
        Ideal.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i)
            (Ideal.map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) p.asIdeal) =
          p.asIdeal),
      ∃ (i : ι) (q : PrimeSpectrum (R i)), comap (Pi.evalRingHom R i) q = p
⊢ ∃ (i : ι) (q : PrimeSpectrum (R i)), comap (Pi.evalRingHom R i) q = p

Tactic:
classical
  cases nonempty_fintype ι
  let e (i) : Π i, R i := Function.update 1 i 0
  have H : ∏ i, e i = 0 := by
    ext j
    rw [Finset.prod_apply, Pi.zero_apply, Finset.prod_eq_zero (Finset.mem_univ j)]
    simp [e]
  obtain ⟨i, hi⟩ : ∃ i, e i ∈ p.asIdeal := by
    simpa [← H, Ideal.IsPrime.prod_mem_iff] using p.asIdeal.zero_mem
  let h₁ : Function.Surjective (Pi.evalRingHom R i) := RingHomSurjective.is_surjective
  have h₂ : RingHom.ker (Pi.evalRingHom R i) ≤ p.asIdeal := by
    intro x hx
    convert! p.asIdeal.mul_mem_left x hi
    ext j
    by_cases hj : i = j
    · subst hj; simpa [e]
    · simp [e, Function.update_of_ne (.symm hj)]
  have : (p.asIdeal.map (Pi.evalRingHom R i)).comap (Pi.evalRingHom R i) = p.asIdeal := by
    rwa [Ideal.comap_map_of_surjective _ h₁, sup_eq_left]
  exact ⟨i, ⟨_, Ideal.map_isPrime_of_surjective h₁ h₂⟩, PrimeSpectrum.ext this⟩

Premises used: nonempty_fintype, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_4
inst : (i : ι) → CommRing (R i)
inst_1 : _root_.Finite ι
⊢ Function.Bijective (α := (i : ι) × PrimeSpectrum (R i)) (sigmaToPi R)

Tactic:
⟨sigmaToPi_injective R, ?_⟩

Premises used: And.intro, Function.Bijective, PrimeSpectrum.sigmaToPi_injective
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_4
inst : (i : ι) → CommRing (R i)
inst_1 : _root_.Finite ι
refine : Function.Surjective (α := (i : ι) × PrimeSpectrum (R i)) (sigmaToPi R)
⊢ Function.Bijective (α := (i : ι) × PrimeSpectrum (R i)) (sigmaToPi R)

Tactic:
refine ⟨sigmaToPi_injective R, ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_4
inst : (i : ι) → CommRing (R i)
inst_1 : _root_.Finite ι
q : PrimeSpectrum ((i : ι) → R i)
obtain :
  ∀ (i : ι) (q : PrimeSpectrum (R i)),
    ∃ (a : (i : ι) × PrimeSpectrum (R i)), sigmaToPi R a = comap (Pi.evalRingHom R i) q
⊢ ∃ (a : (i : ι) × PrimeSpectrum (R i)), sigmaToPi R a = q

Tactic:
obtain ⟨i, q, rfl⟩ := exists_comap_evalRingHom_eq q

Premises used: PrimeSpectrum.exists_comap_evalRingHom_eq, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_4
inst : (i : ι) → CommRing (R i)
inst_1 : _root_.Finite ι
i : ι
q : PrimeSpectrum (R i)
⊢ ∃ (a : (i : ι) × PrimeSpectrum (R i)), sigmaToPi R a = comap (Pi.evalRingHom R i) q

Tactic:
⟨⟨i, q⟩, rfl⟩

Premises used: Exists.intro, Sigma.mk, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_4
inst : (i : ι) → CommRing (R i)
inst_1 : _root_.Finite ι
i : ι
q : PrimeSpectrum (R i)
⊢ ∃ (a : (i : ι) × PrimeSpectrum (R i)), sigmaToPi R a = comap (Pi.evalRingHom R i) q

Tactic:
exact ⟨⟨i, q⟩, rfl⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_4
inst : (i : ι) → CommRing (R i)
inst_1 : _root_.Finite ι
S : Type u_5
inst_2 : CommRing S
f : S →+* (i : ι) → R i
simp_rw :
  Eq.{u_5 + 1} (α := Set (PrimeSpectrum S))
    (⋃ (i : ι),
      Set.range.{u_5, u_4 + 1} (ι := PrimeSpectrum (R i))
        (Function.comp (β := PrimeSpectrum ((i : ι) → R i)) (comap f) (comap (Pi.evalRingHom R i))))
    (Set.range (ι := PrimeSpectrum ((i : ι) → R i)) (comap f))
⊢ Eq.{u_5 + 1} (α := Set (PrimeSpectrum S)) (⋃ (i : ι), Set.range (comap (comp (Pi.evalRingHom R i) f)))
    (Set.range (ι := PrimeSpectrum ((i : ι) → R i)) (comap f))

Tactic:
simp_rw [comap_comp]

Premises used: PrimeSpectrum.comap_comp
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_4
inst : (i : ι) → CommRing (R i)
inst_1 : _root_.Finite ι
S : Type u_5
inst_2 : CommRing S
f : S →+* (i : ι) → R i
a :
  Subset.{u_5} (α := Set (PrimeSpectrum S))
    (⋃ (i : ι),
      Set.range.{u_5, u_4 + 1} (ι := PrimeSpectrum (R i))
        (Function.comp (β := PrimeSpectrum ((i : ι) → R i)) (comap f) (comap (Pi.evalRingHom R i))))
    (Set.range (ι := PrimeSpectrum ((i : ι) → R i)) (comap f))
a₁ :
  Subset.{u_5} (α := Set (PrimeSpectrum S)) (Set.range (ι := PrimeSpectrum ((i : ι) → R i)) (comap f))
    (⋃ (i : ι),
      Set.range.{u_5, u_4 + 1} (ι := PrimeSpectrum (R i))
        (Function.comp (β := PrimeSpectrum ((i : ι) → R i)) (comap f) (comap (Pi.evalRingHom R i))))
⊢ Eq.{u_5 + 1} (α := Set (PrimeSpectrum S))
    (⋃ (i : ι),
      Set.range.{u_5, u_4 + 1} (ι := PrimeSpectrum (R i))
        (Function.comp (β := PrimeSpectrum ((i : ι) → R i)) (comap f) (comap (Pi.evalRingHom R i))))
    (Set.range (ι := PrimeSpectrum ((i : ι) → R i)) (comap f))

Tactic:
apply subset_antisymm

Premises used: subset_antisymm
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_4
inst : (i : ι) → CommRing (R i)
inst_1 : _root_.Finite ι
S : Type u_5
inst_2 : CommRing S
f : S →+* (i : ι) → R i
⊢ Subset.{u_5} (α := Set (PrimeSpectrum S))
    (⋃ (i : ι),
      Set.range.{u_5, u_4 + 1} (ι := PrimeSpectrum (R i))
        (Function.comp (β := PrimeSpectrum ((i : ι) → R i)) (comap f) (comap (Pi.evalRingHom R i))))
    (Set.range (ι := PrimeSpectrum ((i : ι) → R i)) (comap f))

Tactic:
Set.iUnion_subset fun _ ↦ Set.range_comp_subset_range _ _

Premises used: Set.range_comp_subset_range, Set.iUnion_subset, Pi.evalRingHom, PrimeSpectrum.comap
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_4
inst : (i : ι) → CommRing (R i)
inst_1 : _root_.Finite ι
S : Type u_5
inst_2 : CommRing S
f : S →+* (i : ι) → R i
⊢ Subset.{u_5} (α := Set (PrimeSpectrum S))
    (⋃ (i : ι),
      Set.range.{u_5, u_4 + 1} (ι := PrimeSpectrum (R i))
        (Function.comp (β := PrimeSpectrum ((i : ι) → R i)) (comap f) (comap (Pi.evalRingHom R i))))
    (Set.range (ι := PrimeSpectrum ((i : ι) → R i)) (comap f))

Tactic:
exact Set.iUnion_subset fun _ ↦ Set.range_comp_subset_range _ _

Premises used: Set.range_comp_subset_range, Set.iUnion_subset
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_4
inst : (i : ι) → CommRing (R i)
inst_1 : _root_.Finite ι
S : Type u_5
inst_2 : CommRing S
f : S →+* (i : ι) → R i
p : PrimeSpectrum ((i : ι) → R i)
a :
  ∀ (i : ι) (p : PrimeSpectrum (R i)),
    Membership.mem (γ := Set (PrimeSpectrum S))
      (⋃ (i : ι),
        Set.range.{u_5, u_4 + 1} (ι := PrimeSpectrum (R i))
          (Function.comp (β := PrimeSpectrum ((i : ι) → R i)) (comap f) (comap (Pi.evalRingHom R i))))
      (comap (S := (i : ι) → R i) f (comap (Pi.evalRingHom R i) p))
⊢ Membership.mem (γ := Set (PrimeSpectrum S))
    (⋃ (i : ι),
      Set.range.{u_5, u_4 + 1} (ι := PrimeSpectrum (R i))
        (Function.comp (β := PrimeSpectrum ((i : ι) → R i)) (comap f) (comap (Pi.evalRingHom R i))))
    (comap f p)

Tactic:
obtain ⟨i, p, rfl⟩ := exists_comap_evalRingHom_eq p

Premises used: PrimeSpectrum.exists_comap_evalRingHom_eq, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_4
inst : (i : ι) → CommRing (R i)
inst_1 : _root_.Finite ι
S : Type u_5
inst_2 : CommRing S
f : S →+* (i : ι) → R i
i : ι
p : PrimeSpectrum (R i)
⊢ Membership.mem (γ := Set (PrimeSpectrum S))
    (⋃ (i : ι),
      Set.range.{u_5, u_4 + 1} (ι := PrimeSpectrum (R i))
        (Function.comp (β := PrimeSpectrum ((i : ι) → R i)) (comap f) (comap (Pi.evalRingHom R i))))
    (comap (S := (i : ι) → R i) f (comap (Pi.evalRingHom R i) p))

Tactic:
Set.mem_iUnion_of_mem i ⟨p, rfl⟩

Premises used: Set.mem_iUnion_of_mem, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_4
inst : (i : ι) → CommRing (R i)
inst_1 : _root_.Finite ι
S : Type u_5
inst_2 : CommRing S
f : S →+* (i : ι) → R i
i : ι
p : PrimeSpectrum (R i)
⊢ Membership.mem (γ := Set (PrimeSpectrum S))
    (⋃ (i : ι),
      Set.range.{u_5, u_4 + 1} (ι := PrimeSpectrum (R i))
        (Function.comp (β := PrimeSpectrum ((i : ι) → R i)) (comap f) (comap (Pi.evalRingHom R i))))
    (comap (S := (i : ι) → R i) f (comap (Pi.evalRingHom R i) p))

Tactic:
exact Set.mem_iUnion_of_mem i ⟨p, rfl⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
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)
I : Ideal S
simp :
  ∀ (x : PrimeSpectrum R), (∃ (x_1 : PrimeSpectrum S), I ≤ x_1.asIdeal ∧ comap f x_1 = x) ↔ Ideal.comap f I ≤ x.asIdeal
⊢ comap f '' zeroLocus (↑I : Set S) = zeroLocus (↑(Ideal.comap f I) : Set R)

Tactic:
simp only [Set.ext_iff, Set.mem_image, mem_zeroLocus, SetLike.coe_subset_coe]

Premises used: Set.mem_image, PrimeSpectrum.mem_zeroLocus, SetLike.coe_subset_coe, Set.ext_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
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)
I : Ideal S
⊢ ∀ (x : PrimeSpectrum R), (∃ (x_1 : PrimeSpectrum S), I ≤ x_1.asIdeal ∧ comap f x_1 = x) ↔ Ideal.comap f I ≤ x.asIdeal

Tactic:
fun p => ⟨?_, fun h_I_p => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
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)
I : Ideal S
refine_1 :
  ∀ (p : PrimeSpectrum R), (∃ (x : PrimeSpectrum S), I ≤ x.asIdeal ∧ comap f x = p) → Ideal.comap f I ≤ p.asIdeal
refine_2 :
  ∀ (p : PrimeSpectrum R) (h_I_p : Ideal.comap f I ≤ p.asIdeal), ∃ (x : PrimeSpectrum S), I ≤ x.asIdeal ∧ comap f x = p
⊢ ∀ (x : PrimeSpectrum R), (∃ (x_1 : PrimeSpectrum S), I ≤ x_1.asIdeal ∧ comap f x_1 = x) ↔ Ideal.comap f I ≤ x.asIdeal

Tactic:
refine fun p => ⟨?_, fun h_I_p => ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
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)
I : Ideal S
p : PrimeSpectrum S
hp : I ≤ p.asIdeal
a : R
ha : Membership.mem (γ := Submodule R R) (Ideal.comap f I) a
⊢ a ∈ (comap f p).asIdeal

Tactic:
hp ha

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
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)
I : Ideal S
p : PrimeSpectrum S
hp : I ≤ p.asIdeal
a : R
ha : Membership.mem (γ := Submodule R R) (Ideal.comap f I) a
⊢ a ∈ (comap f p).asIdeal

Tactic:
exact hp ha
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
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)
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
⊢ ker f ≤ p.asIdeal

Tactic:
have hp : ker f ≤ p.asIdeal := (Ideal.comap_mono bot_le).trans h_I_p
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
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)
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
⊢ ∃ (x : PrimeSpectrum S), I ≤ x.asIdeal ∧ comap f x = p

Tactic:
⟨⟨p.asIdeal.map f, Ideal.map_isPrime_of_surjective hf hp⟩, fun x hx => ?_, ?_⟩

Premises used: PrimeSpectrum.mk, Ideal.map, And.intro, Exists.intro, Ideal.map_isPrime_of_surjective, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
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)
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
refine_2 :
  ∀ (x : S) (hx : x ∈ I),
    Membership.mem (γ := Submodule S S) (asIdeal { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ }) x
refine_2₁ : comap f { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ : PrimeSpectrum S } = p
⊢ ∃ (x : PrimeSpectrum S), I ≤ x.asIdeal ∧ comap f x = p

Tactic:
refine ⟨⟨p.asIdeal.map f, Ideal.map_isPrime_of_surjective hf hp⟩, fun x hx => ?_, ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
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)
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : S
hx : x ∈ I
refine_2 :
  ∀ (x' : R) (hx : Membership.mem (α := S) I ((f : (a : R) → S) x' : S)),
    Membership.mem.{v, v} (α := S) (γ := Submodule S S) (asIdeal { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ })
      ((f : (a : R) → S) x' : S)
⊢ Membership.mem (γ := Submodule S S) (asIdeal { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ }) x

Tactic:
obtain ⟨x', rfl⟩ := hf x

Premises used: rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
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)
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x' : R
hx : Membership.mem (α := S) I ((f : (a : R) → S) x' : S)
⊢ Membership.mem.{v, v} (α := S) (γ := Submodule S S) (asIdeal { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ })
    ((f : (a : R) → S) x' : S)

Tactic:
Ideal.mem_map_of_mem f (h_I_p hx)

Premises used: Ideal.mem_map_of_mem, Set.Mem
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
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)
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x' : R
hx : Membership.mem (α := S) I ((f : (a : R) → S) x' : S)
⊢ Membership.mem.{v, v} (α := S) (γ := Submodule S S) (asIdeal { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ })
    ((f : (a : R) → S) x' : S)

Tactic:
exact Ideal.mem_map_of_mem f (h_I_p hx)

Premises used: Ideal.mem_map_of_mem
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
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)
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
refine_2 :
  ∀ (x : R), x ∈ (comap f { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ : PrimeSpectrum S }).asIdeal ↔ x ∈ p.asIdeal
⊢ comap f { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ : PrimeSpectrum S } = p

Tactic:
ext x
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
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)
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : R
refine_2 :
  (∃ x_1 ∈ p.asIdeal, Eq.{v + 1} (α := S) ((f : (a : R) → S) x_1 : S) ((f : (a : R) → S) x : S)) ↔ x ∈ p.asIdeal
⊢ x ∈ (comap f { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ : PrimeSpectrum S }).asIdeal ↔ x ∈ p.asIdeal

Tactic:
rw [comap_asIdeal, Ideal.mem_comap, Ideal.mem_map_iff_of_surjective f hf]

Premises used: Ideal.mem_map_iff_of_surjective, PrimeSpectrum.comap_asIdeal, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
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)
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : R
⊢ (∃ x_1 ∈ p.asIdeal, Eq.{v + 1} (α := S) ((f : (a : R) → S) x_1 : S) ((f : (a : R) → S) x : S)) ↔ x ∈ p.asIdeal

Tactic:
⟨?_, fun hx => ⟨x, hx, rfl⟩⟩

Premises used: And.intro, Iff.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
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)
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : R
refine_2 :
  (∃ x_1 ∈ p.asIdeal, Eq.{v + 1} (α := S) ((f : (a : R) → S) x_1 : S) ((f : (a : R) → S) x : S)) → x ∈ p.asIdeal
⊢ (∃ x_1 ∈ p.asIdeal, Eq.{v + 1} (α := S) ((f : (a : R) → S) x_1 : S) ((f : (a : R) → S) x : S)) ↔ x ∈ p.asIdeal

Tactic:
refine ⟨?_, fun hx => ⟨x, hx, rfl⟩⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
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)
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x x' : R
hx' : x' ∈ p.asIdeal
heq : Eq.{v + 1} (α := S) ((f : (a : R) → S) x' : S) ((f : (a : R) → S) x : S)
refine_2 : x' - (x' - x) ∈ p.asIdeal
⊢ x ∈ p.asIdeal

Tactic:
rw [← sub_sub_cancel x' x]

Premises used: sub_sub_cancel
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
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)
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x x' : R
hx' : x' ∈ p.asIdeal
heq : Eq.{v + 1} (α := S) ((f : (a : R) → S) x' : S) ((f : (a : R) → S) x : S)
⊢ x' - (x' - x) ∈ p.asIdeal

Tactic:
p.asIdeal.sub_mem hx' (hp ?_)

Premises used: Set.Mem, Ideal.sub_mem, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
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)
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x x' : R
hx' : x' ∈ p.asIdeal
heq : Eq.{v + 1} (α := S) ((f : (a : R) → S) x' : S) ((f : (a : R) → S) x : S)
refine_2 : Membership.mem (γ := Submodule R R) (ker f) (x' - x)
⊢ x' - (x' - x) ∈ p.asIdeal

Tactic:
refine p.asIdeal.sub_mem hx' (hp ?_)

Premises used: Ideal.sub_mem, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
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)
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x x' : R
hx' : x' ∈ p.asIdeal
heq : Eq.{v + 1} (α := S) ((f : (a : R) → S) x' : S) ((f : (a : R) → S) x : S)
refine_2 : Eq.{v + 1} (α := S) ((f : (a : R) → S) (x' - x) : S) (0 : S)
refine_2₁ : HSub.hSub (α := S) (β := S) ((f : (a : R) → S) x' : S) ((f : (a : R) → S) x : S) = 0
refine_2₂ refine_2₃ refine_2₄ refine_2₅ : Eq.{v + 1} (α := S) ((f : (a : R) → S) x' : S) ((f : (a : R) → S) x : S)
⊢ Membership.mem (γ := Submodule R R) (ker f) (x' - x)

Tactic:
rwa [mem_ker, map_sub, sub_eq_zero]

Premises used: map_sub, sub_eq_zero, RingHom.mem_ker
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
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 : comap f '' Set.univ = zeroLocus (↑(ker f) : Set R)
⊢ Set.range (comap f) = zeroLocus (↑(ker f) : Set R)

Tactic:
rw [← Set.image_univ]

Premises used: Set.image_univ
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
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)
⊢ comap f '' zeroLocus (↑⊥ : Set S) = zeroLocus (↑(Ideal.comap f ⊥) : Set R)

Tactic:
image_comap_zeroLocus_eq_zeroLocus_comap _ _ hf _

Premises used: image_comap_zeroLocus_eq_zeroLocus_comap
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
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)
h : Eq (α := Set (PrimeSpectrum S)) Set.univ (zeroLocus (↑⊥ : Set S))
⊢ comap f '' Set.univ = zeroLocus (↑(ker f) : Set R)

Tactic:
convert! image_comap_zeroLocus_eq_zeroLocus_comap _ _ hf _

Premises used: image_comap_zeroLocus_eq_zeroLocus_comap
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
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)
h h₁ : Eq.{v + 1} (α := Set (PrimeSpectrum S)) Set.univ Set.univ
⊢ Eq (α := Set (PrimeSpectrum S)) Set.univ (zeroLocus (↑⊥ : Set S))

Tactic:
rw [zeroLocus_bot]

Premises used: PrimeSpectrum.zeroLocus_bot
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
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)
I : Ideal R
hI : ker f = I
p : Ideal S
isPrime : p.IsPrime
simp : map f (PrimeSpectrum.comap f { asIdeal := p, isPrime := isPrime : PrimeSpectrum S }).asIdeal = p
⊢ (fun (x : (↑(zeroLocus (↑I : Set R)) : Type u)) ↦
        (match (motive := (↑(zeroLocus (↑I : Set R)) : Type u) → PrimeSpectrum S) x with
          | ⟨{ asIdeal := p, isPrime := isPrime }, hp⟩ => { asIdeal := map f p, isPrime := ⋯ } :
          PrimeSpectrum S))
      ((fun (p : PrimeSpectrum S) ↦
          (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
              Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) x) (PrimeSpectrum.comap f p) ⋯ :
            { x : PrimeSpectrum R // Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) x }))
        { asIdeal := p, isPrime := isPrime }) =
    { asIdeal := p, isPrime := isPrime : PrimeSpectrum S }

Tactic:
simp only [PrimeSpectrum.mk.injEq]

Premises used: PrimeSpectrum.mk.injEq
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
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)
I : Ideal R
hI : ker f = I
p : Ideal S
isPrime : p.IsPrime
⊢ map f (PrimeSpectrum.comap f { asIdeal := p, isPrime := isPrime : PrimeSpectrum S }).asIdeal = p

Tactic:
p.map_comap_of_surjective f hf

Premises used: Ideal.comap, Ideal.map_comap_of_surjective
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
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)
I : Ideal R
hI : ker f = I
p : Ideal S
isPrime : p.IsPrime
⊢ map f (PrimeSpectrum.comap f { asIdeal := p, isPrime := isPrime : PrimeSpectrum S }).asIdeal = p

Tactic:
exact p.map_comap_of_surjective f hf

Premises used: Ideal.map_comap_of_surjective