awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
inst_1 : Infinite ι
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
J : Ideal ((i : ι) → R i) :=
  let __spread.0 : AddSubmonoid ((i : ι) → R i) :=
    AddMonoidHom.mrange (F := (Π₀ (i : ι), R i) →+ (i : ι) → R i) (DFinsupp.coeFnAddMonoidHom (β := R));
  { toAddSubmonoid := __spread.0, smul_mem' := ⋯ }
x : Π₀ (i : ι), R i
hx :
  Eq (α := (i : ι) → R i)
    ((DFinsupp.coeFnAddMonoidHom (β := R) : (a : Π₀ (i : ι), R i) → (i : ι) → R i) x : (i : ι) → R i)
    (1 : (i : ι) → R i)
i : ι
hi : i ∉ x.support (β := R)
⊢ False

Tactic:
simpa [DFinsupp.coeFnAddMonoidHom, DFinsupp.notMem_support_iff.mp hi] using congr_fun hx i

Premises used: DFinsupp.notMem_support_iff, DFinsupp.coeFnAddMonoidHom, Iff.mp, congr_fun
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
inst_1 : Infinite ι
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
J : Ideal ((i : ι) → R i) :=
  let __spread.0 : AddSubmonoid ((i : ι) → R i) :=
    AddMonoidHom.mrange (F := (Π₀ (i : ι), R i) →+ (i : ι) → R i) (DFinsupp.coeFnAddMonoidHom (β := R));
  { toAddSubmonoid := __spread.0, smul_mem' := ⋯ }
have :
  ∀ (I : Ideal ((i : ι) → R i)) (max : I.IsMaximal) (le : J ≤ I),
    ∃ (I : Ideal ((i : ι) → R i)) (x : I.IsMaximal), { asIdeal := I, isPrime := ⋯ } ∉ Set.range (sigmaToPi R)
⊢ ∃ (I : Ideal ((i : ι) → R i)) (x : I.IsMaximal), { asIdeal := I, isPrime := ⋯ } ∉ Set.range (sigmaToPi R)

Tactic:
have ⟨I, max, le⟩ := J.exists_le_maximal <| (Ideal.ne_top_iff_one _).mpr <| by
    -- take a maximal ideal I containing J
    rintro ⟨x, hx⟩
    have ⟨i, hi⟩ := x.support.exists_notMem
    simpa [DFinsupp.coeFnAddMonoidHom, DFinsupp.notMem_support_iff.mp hi] using congr_fun hx i
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
inst_1 : Infinite ι
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
J : Ideal ((i : ι) → R i) :=
  let __spread.0 : AddSubmonoid ((i : ι) → R i) :=
    AddMonoidHom.mrange (F := (Π₀ (i : ι), R i) →+ (i : ι) → R i) (DFinsupp.coeFnAddMonoidHom (β := R));
  { toAddSubmonoid := __spread.0, smul_mem' := ⋯ }
I : Ideal ((i : ι) → R i)
max : I.IsMaximal
le : J ≤ I
⊢ ∃ (I : Ideal ((i : ι) → R i)) (x : I.IsMaximal), { asIdeal := I, isPrime := ⋯ } ∉ Set.range (sigmaToPi R)

Tactic:
⟨I, max, fun ⟨⟨i, p⟩, eq⟩ ↦ ?_⟩

Premises used: False, _private.0.PrimeSpectrum.exists_maximal_notMem_range_sigmaToPi_of_infinite.match_4, Exists.intro
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
inst_1 : Infinite ι
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
J : Ideal ((i : ι) → R i) :=
  let __spread.0 : AddSubmonoid ((i : ι) → R i) :=
    AddMonoidHom.mrange (F := (Π₀ (i : ι), R i) →+ (i : ι) → R i) (DFinsupp.coeFnAddMonoidHom (β := R));
  { toAddSubmonoid := __spread.0, smul_mem' := ⋯ }
I : Ideal ((i : ι) → R i)
max : I.IsMaximal
le : J ≤ I
refine :
  Membership.mem (γ := Set (PrimeSpectrum ((i : ι) → R i))) (Set.range (sigmaToPi R)) { asIdeal := I, isPrime := ⋯ } →
    ∀ (i : ι) (p : PrimeSpectrum (R i))
      (eq :
        Eq (α := PrimeSpectrum ((i : ι) → R i)) (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))
          { asIdeal := I, isPrime := ⋯ }),
      False
⊢ ∃ (I : Ideal ((i : ι) → R i)) (x : I.IsMaximal), { asIdeal := I, isPrime := ⋯ } ∉ Set.range (sigmaToPi R)

Tactic:
refine ⟨I, max, fun ⟨⟨i, p⟩, eq⟩ ↦ ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
inst_1 : Infinite ι
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
J : Ideal ((i : ι) → R i) :=
  let __spread.0 : AddSubmonoid ((i : ι) → R i) :=
    AddMonoidHom.mrange (F := (Π₀ (i : ι), R i) →+ (i : ι) → R i) (DFinsupp.coeFnAddMonoidHom (β := R));
  { toAddSubmonoid := __spread.0, smul_mem' := ⋯ }
I : Ideal ((i : ι) → R i)
max : I.IsMaximal
le : J ≤ I
h : Membership.mem (γ := Set (PrimeSpectrum ((i : ι) → R i))) (Set.range (sigmaToPi R)) { asIdeal := I, isPrime := ⋯ }
i : ι
p : PrimeSpectrum (R i)
eq :
  Eq (α := PrimeSpectrum ((i : ι) → R i)) (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))
    { asIdeal := I, isPrime := ⋯ }
⊢ (⇑(DFinsupp.single (β := R) i 1) : (a : ι) → R a) ∉
    asIdeal (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))

Tactic:
simpa using p.1.ne_top_iff_one.mp p.2.ne_top

Premises used: Ideal.ne_top_iff_one, PrimeSpectrum.isPrime, Iff.mp, Ideal.IsPrime.ne_top, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
inst_1 : Infinite ι
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
J : Ideal ((i : ι) → R i) :=
  let __spread.0 : AddSubmonoid ((i : ι) → R i) :=
    AddMonoidHom.mrange (F := (Π₀ (i : ι), R i) →+ (i : ι) → R i) (DFinsupp.coeFnAddMonoidHom (β := R));
  { toAddSubmonoid := __spread.0, smul_mem' := ⋯ }
I : Ideal ((i : ι) → R i)
max : I.IsMaximal
le : J ≤ I
h : Membership.mem (γ := Set (PrimeSpectrum ((i : ι) → R i))) (Set.range (sigmaToPi R)) { asIdeal := I, isPrime := ⋯ }
i : ι
p : PrimeSpectrum (R i)
eq :
  Eq (α := PrimeSpectrum ((i : ι) → R i)) (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))
    { asIdeal := I, isPrime := ⋯ }
⊢ (⇑(DFinsupp.single (β := R) i 1) : (a : ι) → R a) ∉
    asIdeal (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))

Tactic:
have : ⇑(DFinsupp.single i 1) ∉ (sigmaToPi R ⟨i, p⟩).asIdeal := by
    simpa using p.1.ne_top_iff_one.mp p.2.ne_top
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
inst_1 : Infinite ι
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
J : Ideal ((i : ι) → R i) :=
  let __spread.0 : AddSubmonoid ((i : ι) → R i) :=
    AddMonoidHom.mrange (F := (Π₀ (i : ι), R i) →+ (i : ι) → R i) (DFinsupp.coeFnAddMonoidHom (β := R));
  { toAddSubmonoid := __spread.0, smul_mem' := ⋯ }
I : Ideal ((i : ι) → R i)
max : I.IsMaximal
le : J ≤ I
h : Membership.mem (γ := Set (PrimeSpectrum ((i : ι) → R i))) (Set.range (sigmaToPi R)) { asIdeal := I, isPrime := ⋯ }
i : ι
p : PrimeSpectrum (R i)
eq :
  Eq (α := PrimeSpectrum ((i : ι) → R i)) (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))
    { asIdeal := I, isPrime := ⋯ }
this :
  (⇑(DFinsupp.single (β := R) i 1) : (a : ι) → R a) ∉
    asIdeal (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))
⊢ (⇑(DFinsupp.single (β := R) i 1) : (a : ι) → R a) ∉ asIdeal { asIdeal := I, isPrime := ⋯ }

Tactic:
rw [eq] at this
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
inst_1 : Infinite ι
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
J : Ideal ((i : ι) → R i) :=
  let __spread.0 : AddSubmonoid ((i : ι) → R i) :=
    AddMonoidHom.mrange (F := (Π₀ (i : ι), R i) →+ (i : ι) → R i) (DFinsupp.coeFnAddMonoidHom (β := R));
  { toAddSubmonoid := __spread.0, smul_mem' := ⋯ }
I : Ideal ((i : ι) → R i)
max : I.IsMaximal
le : J ≤ I
h : Membership.mem (γ := Set (PrimeSpectrum ((i : ι) → R i))) (Set.range (sigmaToPi R)) { asIdeal := I, isPrime := ⋯ }
i : ι
p : PrimeSpectrum (R i)
eq :
  Eq (α := PrimeSpectrum ((i : ι) → R i)) (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))
    { asIdeal := I, isPrime := ⋯ }
this : (⇑(DFinsupp.single (β := R) i 1) : (a : ι) → R a) ∉ asIdeal { asIdeal := I, isPrime := ⋯ }
⊢ False

Tactic:
this (le ⟨.single i 1, rfl⟩)

Premises used: DFinsupp.single, Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
inst_1 : Infinite ι
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
J : Ideal ((i : ι) → R i) :=
  let __spread.0 : AddSubmonoid ((i : ι) → R i) :=
    AddMonoidHom.mrange (F := (Π₀ (i : ι), R i) →+ (i : ι) → R i) (DFinsupp.coeFnAddMonoidHom (β := R));
  { toAddSubmonoid := __spread.0, smul_mem' := ⋯ }
I : Ideal ((i : ι) → R i)
max : I.IsMaximal
le : J ≤ I
h : Membership.mem (γ := Set (PrimeSpectrum ((i : ι) → R i))) (Set.range (sigmaToPi R)) { asIdeal := I, isPrime := ⋯ }
i : ι
p : PrimeSpectrum (R i)
eq :
  Eq (α := PrimeSpectrum ((i : ι) → R i)) (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))
    { asIdeal := I, isPrime := ⋯ }
this : (⇑(DFinsupp.single (β := R) i 1) : (a : ι) → R a) ∉ asIdeal { asIdeal := I, isPrime := ⋯ }
⊢ False

Tactic:
exact this (le ⟨.single i 1, rfl⟩)

Premises used: DFinsupp.single, Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.RingHom
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
inst_1 : Infinite ι
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
⊢ ¬Function.Surjective (α := (i : ι) × PrimeSpectrum (R i)) (sigmaToPi R)

Tactic:
fun surj ↦
  have ⟨_, _, notMem⟩ := exists_maximal_notMem_range_sigmaToPi_of_infinite R
  (Set.range_eq_univ.mpr surj ▸ notMem) ⟨⟩

Premises used: False, _private.0.PrimeSpectrum.sigmaToPi_not_surjective_of_infinite.match_1, PrimeSpectrum.exists_maximal_notMem_range_sigmaToPi_of_infinite, Not
-- 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
⊢ ∃ (i : ι) (q : PrimeSpectrum (R i)), comap (Pi.evalRingHom R i) q = p

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- 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)
val : Fintype ι
e : (i i : ι) → R i := fun (i : ι) ↦ Function.update (β := R) 1 i 0
h : ∀ (j : ι), Eq.{u_4 + 1} (α := R j) ((∏ i : ι, e i) j) (0 j)
⊢ Eq (α := (i : ι) → R i) (∏ i : ι, e i) 0

Tactic:
ext j
-- 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)
val : Fintype ι
e : (i i : ι) → R i := fun (i : ι) ↦ Function.update (β := R) 1 i 0
j : ι
h : e j j = 0
⊢ Eq.{u_4 + 1} (α := R j) ((∏ i : ι, e i) j) (0 j)

Tactic:
rw [Finset.prod_apply, Pi.zero_apply, Finset.prod_eq_zero (Finset.mem_univ j)]

Premises used: Finset.mem_univ, Finset.prod_apply, Pi.zero_apply, Finset.prod_eq_zero
-- 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)
val : Fintype ι
e : (i i : ι) → R i := fun (i : ι) ↦ Function.update (β := R) 1 i 0
j : ι
⊢ e j j = 0

Tactic:
simp [e]
-- 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)
val : Fintype ι
e : (i i : ι) → R i := fun (i : ι) ↦ Function.update (β := R) 1 i 0
⊢ Eq (α := (i : ι) → R i) (∏ i : ι, e i) 0

Tactic:
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]
-- 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)
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 : ι), e i ∈ p.asIdeal

Tactic:
simpa [← H, Ideal.IsPrime.prod_mem_iff] using p.asIdeal.zero_mem

Premises used: Ideal.IsPrime.prod_mem_iff, Ideal.zero_mem, 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 ι
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
intro : ∀ (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

Tactic:
obtain ⟨i, hi⟩ : ∃ i, e i ∈ p.asIdeal := by
    simpa [← H, Ideal.IsPrime.prod_mem_iff] using p.asIdeal.zero_mem

Premises used: 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 ι
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
⊢ x * e i ∈ p.asIdeal

Tactic:
p.asIdeal.mul_mem_left x hi

Premises used: Ideal.mul_mem_left, 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 ι
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
h : x = x * e i
⊢ x ∈ p.asIdeal

Tactic:
convert! p.asIdeal.mul_mem_left x hi

Premises used: Ideal.mul_mem_left, 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 ι
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
h : ∀ (j : ι), x j = (x * e i) j
⊢ x = x * e i

Tactic:
ext j
-- 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)
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
neg : ∀ (hj : ¬i = j), x j = (x * e i) j
⊢ x j = (x * e i) j

Tactic:
by_cases hj : i = j
-- 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)
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
pos : x i = (x * e i) i
⊢ x j = (x * e i) j

Tactic:
subst hj
-- 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)
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
⊢ x i = (x * e i) i

Tactic:
simpa [e]
-- 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)
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

Tactic:
simp [e, Function.update_of_ne (.symm hj)]

Premises used: Ne.symm, Function.update_of_ne
-- 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)
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) := ⋯
⊢ 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)]
-- 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)
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
rwa₁ rwa₂ rwa₃ rwa₄ : 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

Tactic:
rwa [Ideal.comap_map_of_surjective _ h₁, sup_eq_left]

Premises used: sup_eq_left, Ideal.comap_map_of_surjective
-- 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)
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

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]
-- 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)
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
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:
⟨i, ⟨_, Ideal.map_isPrime_of_surjective h₁ h₂⟩, PrimeSpectrum.ext this⟩

Premises used: PrimeSpectrum.mk, PrimeSpectrum.ext, Exists.intro, Ideal.map_isPrime_of_surjective
-- 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)
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
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:
exact ⟨i, ⟨_, Ideal.map_isPrime_of_surjective h₁ h₂⟩, PrimeSpectrum.ext this⟩