awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
ι : Type u_3
R : ι → Type u_4
inst : (i : ι) → CommRing (R i)
inst_1 : _root_.Finite ι
p : PrimeSpectrum ((i : ι) → R i)
val : Fintype ι
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₁ : Function.Surjective (α := (i : ι) → R i) (β := R i) (⇑(Pi.evalRingHom R i) : (a : (i : ι) → R i) → R i) := ⋯
x : (i : ι) → R i
hx :
  Membership.mem (γ := Submodule ((i : ι) → R i) ((i : ι) → R i))
    (ker (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i)) x
j : ι
pos : ∀ (hj : i = j), x j = (x * e i) j
⊢ x j = (x * e i) j
have neg : ∀ (hj : ¬i = j), x j = (x * e i) j
Tactic: by_cases hj : i = j
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
ι : Type u_3
R : ι → Type u_4
inst : (i : ι) → CommRing (R i)
inst_1 : _root_.Finite ι
p : PrimeSpectrum ((i : ι) → R i)
val : Fintype ι
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₁ : Function.Surjective (α := (i : ι) → R i) (β := R i) (⇑(Pi.evalRingHom R i) : (a : (i : ι) → R i) → R i) := ⋯
x : (i : ι) → R i
hx :
  Membership.mem (γ := Submodule ((i : ι) → R i) ((i : ι) → R i))
    (ker (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i)) x
j : ι
hj : i = j
⊢ x j = (x * e i) j
have pos : x i = (x * e i) i
Tactic: subst hj
Cleared hypotheses: j, hj
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (hypothesis)
Goal:
ι : Type u_3
R : ι → Type u_4
inst : (i : ι) → CommRing (R i)
inst_1 : _root_.Finite ι
p : PrimeSpectrum ((i : ι) → R i)
val : Fintype ι
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₁ : Function.Surjective (α := (i : ι) → R i) (β := R i) (⇑(Pi.evalRingHom R i) : (a : (i : ι) → R i) → R i) := ⋯
⊢ ∃ (i : ι) (q : PrimeSpectrum (R i)), comap (Pi.evalRingHom R i) q = p
have h₂ : ker (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) ≤ p.asIdeal
Tactic: 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)]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
ι : Type u_3
R : ι → Type u_4
inst : (i : ι) → CommRing (R i)
inst_1 : _root_.Finite ι
p : PrimeSpectrum ((i : ι) → R i)
val : Fintype ι
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₁ : Function.Surjective (α := (i : ι) → R i) (β := R i) (⇑(Pi.evalRingHom R i) : (a : (i : ι) → R i) → R i) := ⋯
h₂ : ker (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) ≤ p.asIdeal
⊢ 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
have rwa : p.asIdeal ⊔ Ideal.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) ⊥ = p.asIdeal
Tactic: rwa [Ideal.comap_map_of_surjective _ h₁, sup_eq_left]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
ι : Type u_3
R : ι → Type u_4
inst : (i : ι) → CommRing (R i)
inst_1 : _root_.Finite ι
p : PrimeSpectrum ((i : ι) → R i)
val : Fintype ι
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₁ : Function.Surjective (α := (i : ι) → R i) (β := R i) (⇑(Pi.evalRingHom R i) : (a : (i : ι) → R i) → R i) := ⋯
h₂ : ker (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) ≤ p.asIdeal
rwa : p.asIdeal ⊔ Ideal.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) ⊥ = p.asIdeal
⊢ 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
have rwa₁ : Ideal.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) ⊥ ≤ p.asIdeal
Tactic: rwa [Ideal.comap_map_of_surjective _ h₁, sup_eq_left]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (hypothesis)
Goal:
ι : Type u_3
R : ι → Type u_4
inst : (i : ι) → CommRing (R i)
inst_1 : _root_.Finite ι
p : PrimeSpectrum ((i : ι) → R i)
val : Fintype ι
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₁ : Function.Surjective (α := (i : ι) → R i) (β := R i) (⇑(Pi.evalRingHom R i) : (a : (i : ι) → R i) → R i) := ⋯
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
have 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
Tactic: 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]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
ι : Type u_3
R : ι → Type u_4
inst : (i : ι) → CommRing (R i)
inst_1 : _root_.Finite ι
p : PrimeSpectrum ((i : ι) → R i)
⊢ ∃ (i : ι) (q : PrimeSpectrum (R i)), comap (Pi.evalRingHom R i) q = p
have intro : ∀ (val : Fintype ι), ∃ (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⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
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
⊢ ∃ (i : ι) (q : PrimeSpectrum (R i)), comap (Pi.evalRingHom R i) q = p
have 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
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⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
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
⊢ ∃ (i : ι) (q : PrimeSpectrum (R i)), comap (Pi.evalRingHom R i) q = p
have 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
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⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
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
⊢ ∃ (i : ι) (q : PrimeSpectrum (R i)), comap (Pi.evalRingHom R i) q = p
have 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
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⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
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
⊢ ∃ (i : ι) (q : PrimeSpectrum (R i)), comap (Pi.evalRingHom R i) q = p
have 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
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⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
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)
have refine : Function.Surjective (α := (i : ι) × PrimeSpectrum (R i)) (sigmaToPi R)
Tactic: refine ⟨sigmaToPi_injective R, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
ι : Type u_3
R : ι → Type u_4
inst : (i : ι) → CommRing (R i)
inst_1 : _root_.Finite ι
q : PrimeSpectrum ((i : ι) → R i)
⊢ ∃ (a : (i : ι) × PrimeSpectrum (R i)), sigmaToPi R a = q
have obtain : ∀ (i : ι) (q : PrimeSpectrum (R i)), ∃ (a : (i : ι) × PrimeSpectrum (R i)), sigmaToPi R a = comap (Pi.evalRingHom R i) q
Tactic: obtain ⟨i, q, rfl⟩ := exists_comap_evalRingHom_eq q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
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
⊢ 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))
have 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))
Tactic: simp_rw [comap_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
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
⊢ 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))
have 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))
Tactic: apply subset_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
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))
⊢ 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))
have 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))))
Tactic: apply subset_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
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)
⊢ 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)
have 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))
Tactic: obtain ⟨i, p, rfl⟩ := exists_comap_evalRingHom_eq p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
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
⊢ comap f '' zeroLocus (↑I : Set S) = zeroLocus (↑(Ideal.comap f I) : Set R)
have simp : ∀ (x : PrimeSpectrum R), (∃ (x_1 : PrimeSpectrum S), I ≤ x_1.asIdeal ∧ comap f x_1 = x) ↔ Ideal.comap f I ≤ x.asIdeal
Tactic: simp only [Set.ext_iff, Set.mem_image, mem_zeroLocus, SetLike.coe_subset_coe]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
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
have refine_1 : ∀ (p : PrimeSpectrum R), (∃ (x : PrimeSpectrum S), I ≤ x.asIdeal ∧ comap f x = p) → Ideal.comap f I ≤ p.asIdeal
Tactic: refine fun p => ⟨?_, fun h_I_p => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
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
⊢ ∀ (x : PrimeSpectrum R), (∃ (x_1 : PrimeSpectrum S), I ≤ x_1.asIdeal ∧ comap f x_1 = x) ↔ Ideal.comap f I ≤ x.asIdeal
have refine_2 : ∀ (p : PrimeSpectrum R) (h_I_p : Ideal.comap f I ≤ p.asIdeal), ∃ (x : PrimeSpectrum S), I ≤ x.asIdeal ∧ comap f x = p
Tactic: refine fun p => ⟨?_, fun h_I_p => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (hypothesis)
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
⊢ ∃ (x : PrimeSpectrum S), I ≤ x.asIdeal ∧ comap f x = p
have hp : ker f ≤ p.asIdeal
Tactic: have hp : ker f ≤ p.asIdeal := (Ideal.comap_mono bot_le).trans h_I_p
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
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
have refine_2 : ∀ (x : S) (hx : x ∈ I),
  Membership.mem (γ := Submodule S S) (asIdeal { asIdeal := Ideal.map f p.asIdeal, isPrime := sorry }) x
Tactic: refine ⟨⟨p.asIdeal.map f, Ideal.map_isPrime_of_surjective hf hp⟩, fun x hx => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
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
⊢ ∃ (x : PrimeSpectrum S), I ≤ x.asIdeal ∧ comap f x = p
have refine_2₁ : comap f { asIdeal := Ideal.map f p.asIdeal, isPrime := sorry : PrimeSpectrum S } = p
Tactic: refine ⟨⟨p.asIdeal.map f, Ideal.map_isPrime_of_surjective hf hp⟩, fun x hx => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
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
⊢ Membership.mem (γ := Submodule S S) (asIdeal { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ }) x
have 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 := sorry })
    ((f : (a : R) → S) x' : S)
Tactic: obtain ⟨x', rfl⟩ := hf x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
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
⊢ comap f { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ : PrimeSpectrum S } = p
have refine_2 : ∀ (x : R), x ∈ (comap f { asIdeal := Ideal.map f p.asIdeal, isPrime := sorry : PrimeSpectrum S }).asIdeal ↔ x ∈ p.asIdeal
Tactic: ext x