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_2
inst : (i : ι) → CommSemiring (R i)
x x_1 : (i : ι) × PrimeSpectrum (R i)
i : ι
p : PrimeSpectrum (R i)
j : ι
q : PrimeSpectrum (R j)
eq :
  Eq (α := PrimeSpectrum ((i : ι) → R i)) (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))
    (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) j q))
inl :
  ∀ (q : PrimeSpectrum (R i))
    (eq :
      Eq (α := PrimeSpectrum ((i : ι) → R i)) (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))
        (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i q))),
    Eq (α := (i : ι) × PrimeSpectrum (R i)) (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p)
      (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i q)
⊢ Eq (α := (i : ι) × PrimeSpectrum (R i)) (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p)
    (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) j q)
have inr : ∀ (ne : i ≠ j),
  Eq (α := (i : ι) × PrimeSpectrum (R i)) (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p)
    (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) j q)
Tactic: obtain rfl | ne := eq_or_ne i j
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
x x_1 : (i : ι) × PrimeSpectrum (R i)
i : ι
p q : PrimeSpectrum (R i)
eq :
  Eq (α := PrimeSpectrum ((i : ι) → R i)) (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))
    (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i q))
⊢ Eq (α := (i : ι) × PrimeSpectrum (R i)) (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p)
    (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i q)
have inl : p = q
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
x x_1 : (i : ι) × PrimeSpectrum (R i)
i : ι
p q : PrimeSpectrum (R i)
eq :
  Eq (α := PrimeSpectrum ((i : ι) → R i)) (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))
    (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i q))
⊢ p = q
have inl : ∀ (x : R i), x ∈ p.asIdeal ↔ x ∈ q.asIdeal
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
x x_1 : (i : ι) × PrimeSpectrum (R i)
i : ι
p : PrimeSpectrum (R i)
j : ι
q : PrimeSpectrum (R j)
eq :
  Eq (α := PrimeSpectrum ((i : ι) → R i)) (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))
    (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) j q))
ne : i ≠ j
⊢ Eq (α := (i : ι) × PrimeSpectrum (R i)) (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p)
    (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) j q)
have inr : 1 ∈ p.asIdeal
Tactic: refine (p.1.ne_top_iff_one.mp p.2.ne_top ?_).elim
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (hypothesis)
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
x x_1 : (i : ι) × PrimeSpectrum (R i)
i : ι
p : PrimeSpectrum (R i)
j : ι
q : PrimeSpectrum (R j)
eq :
  Eq (α := PrimeSpectrum ((i : ι) → R i)) (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))
    (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) j q))
ne : i ≠ j
⊢ 1 ∈ p.asIdeal
have this : Membership.mem (γ := Ideal ((i : ι) → R i))
  (asIdeal (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) j q))) (Function.update (β := R) 1 j 0)
Tactic: have : Function.update (1 : ∀ i, R i) j 0 ∈ (sigmaToPi R ⟨j, q⟩).asIdeal := by simp
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
x x_1 : (i : ι) × PrimeSpectrum (R i)
i : ι
p : PrimeSpectrum (R i)
j : ι
q : PrimeSpectrum (R j)
eq :
  Eq (α := PrimeSpectrum ((i : ι) → R i)) (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))
    (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) j q))
⊢ Eq (α := (i : ι) × PrimeSpectrum (R i)) (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p)
    (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) j q)
have inl : ∀ (q : PrimeSpectrum (R i))
  (eq :
    Eq (α := PrimeSpectrum ((i : ι) → R i)) (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))
      (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i q))),
  Eq (α := (i : ι) × PrimeSpectrum (R i)) (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p)
    (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i q)
Tactic: classical
  obtain rfl | ne := eq_or_ne i j
  · congr; ext x
    simpa using congr_arg (Function.update (0 : ∀ i, R i) i x ∈ ·.asIdeal) eq
  · refine (p.1.ne_top_iff_one.mp p.2.ne_top ?_).elim
    have : Function.update (1 : ∀ i, R i) j 0 ∈ (sigmaToPi R ⟨j, q⟩).asIdeal := by simp
    simpa [← eq, Function.update_of_ne ne]
Cleared hypotheses: j, q, eq
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
x x_1 : (i : ι) × PrimeSpectrum (R i)
i : ι
p : PrimeSpectrum (R i)
j : ι
q : PrimeSpectrum (R j)
eq :
  Eq (α := PrimeSpectrum ((i : ι) → R i)) (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))
    (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) j q))
inl :
  ∀ (q : PrimeSpectrum (R i))
    (eq :
      Eq (α := PrimeSpectrum ((i : ι) → R i)) (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))
        (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i q))),
    Eq (α := (i : ι) × PrimeSpectrum (R i)) (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p)
      (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i q)
⊢ Eq (α := (i : ι) × PrimeSpectrum (R i)) (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p)
    (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) j q)
have inr : ∀ (ne : i ≠ j),
  Eq (α := (i : ι) × PrimeSpectrum (R i)) (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p)
    (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) j q)
Tactic: classical
  obtain rfl | ne := eq_or_ne i j
  · congr; ext x
    simpa using congr_arg (Function.update (0 : ∀ i, R i) i x ∈ ·.asIdeal) eq
  · refine (p.1.ne_top_iff_one.mp p.2.ne_top ?_).elim
    have : Function.update (1 : ∀ i, R i) j 0 ∈ (sigmaToPi R ⟨j, q⟩).asIdeal := by simp
    simpa [← eq, Function.update_of_ne ne]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
inst_1 : Infinite ι
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
r : (i : ι) → R i
x : Π₀ (i : ι), R i
⊢ HSMul.hSMul (β := (i : ι) → R i) r
      ((DFinsupp.coeFnAddMonoidHom (β := R) : (a : Π₀ (i : ι), R i) → (i : ι) → R i) x : (i : ι) → R i) ∈
    AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (AddMonoidHom.mrange (F := (Π₀ (i : ι), R i) →+ (i : ι) → R i) (DFinsupp.coeFnAddMonoidHom (β := R))))
have refine : ∀ (i : ι),
  (if H : i ∈ x.support (β := R) then
      (fun (i : (↑(↑(x.support (β := R)) : Set ι) : Type u_3)) ↦
          HMul.hMul (α := R (↑i : ι)) (r (↑i : ι)) ((x : (a : ι) → R a) (↑i : ι)))
        (Subtype.mk (p := fun (x_1 : ι) ↦ x_1 ∈ (↑(x.support (β := R)) : Set ι)) i H)
    else 0) =
    HSMul.hSMul (β := (i : ι) → R i) r
      ((DFinsupp.coeFnAddMonoidHom (β := R) : (a : Π₀ (i : ι), R i) → (i : ι) → R i) x : (i : ι) → R i) i
Tactic: refine ⟨.mk x.support fun i ↦ r i * x i, funext fun i ↦ show dite _ _ _ = _ from ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
inst_1 : Infinite ι
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
r : (i : ι) → R i
x : Π₀ (i : ι), R i
i : ι
⊢ (if H : i ∈ x.support (β := R) then
      (fun (i : (↑(↑(x.support (β := R)) : Set ι) : Type u_3)) ↦
          HMul.hMul (α := R (↑i : ι)) (r (↑i : ι)) ((x : (a : ι) → R a) (↑i : ι)))
        (Subtype.mk (p := fun (x_1 : ι) ↦ x_1 ∈ (↑(x.support (β := R)) : Set ι)) i H)
    else 0) =
    HSMul.hSMul (β := (i : ι) → R i) r
      ((DFinsupp.coeFnAddMonoidHom (β := R) : (a : Π₀ (i : ι), R i) → (i : ι) → R i) x : (i : ι) → R i) i
have simp_rw : (if h : i ∈ x.support (β := R) then r i * (x : (a : ι) → R a) i else 0) =
  HSMul.hSMul (β := (i : ι) → R i) r
    (({ toFun := DFunLike.coe (β := R), map_zero' := sorry, map_add' := sorry : (Π₀ (i : ι), R i) →+ (i : ι) → R i } :
          (a : Π₀ (i : ι), R i) → (i : ι) → R i)
        x :
      (i : ι) → R i)
    i
Tactic: simp_rw +instances [DFinsupp.coeFnAddMonoidHom]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
inst_1 : Infinite ι
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
r : (i : ι) → R i
x : Π₀ (i : ι), R i
i : ι
⊢ (if h : i ∈ x.support (β := R) then r i * (x : (a : ι) → R a) i else 0) =
    HSMul.hSMul (β := (i : ι) → R i) r
      (({ toFun := DFunLike.coe (β := R), map_zero' := ⋯, map_add' := ⋯ : (Π₀ (i : ι), R i) →+ (i : ι) → R i } :
            (a : Π₀ (i : ι), R i) → (i : ι) → R i)
          x :
        (i : ι) → R i)
      i
have refine : ∀ (h : i ∉ x.support (β := R)), 0 = r i * (x : (a : ι) → R a) i
Tactic: refine dite_eq_left_iff.mpr fun h ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
inst_1 : Infinite ι
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
r : (i : ι) → R i
x : Π₀ (i : ι), R i
i : ι
h : i ∉ x.support (β := R)
⊢ 0 = r i * (x : (a : ι) → R a) i
have rw : 0 = r i * 0
Tactic: rw [DFinsupp.notMem_support_iff.mp h, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
inst_1 : Infinite ι
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
r : (i : ι) → R i
x : Π₀ (i : ι), R i
i : ι
h : i ∉ x.support (β := R)
rw : 0 = r i * 0
⊢ 0 = r i * (x : (a : ι) → R a) i
have rw₁ : Eq.{u_2 + 1} (α := R i) 0 0
Tactic: rw [DFinsupp.notMem_support_iff.mp h, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
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)
⊢ False
have have : ∀ (i : ι) (hi : i ∉ x.support (β := R)), False
Tactic: have ⟨i, hi⟩ := x.support.exists_notMem
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
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)) (x : I.IsMaximal), { asIdeal := I, isPrime := ⋯ } ∉ Set.range (sigmaToPi R)
have have : ∀ (I : Ideal ((i : ι) → R i)) (max : I.IsMaximal) (le : J ≤ I),
  ∃ (I : Ideal ((i : ι) → R i)) (x : I.IsMaximal), { asIdeal := I, isPrime := sorry } ∉ 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
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
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)
have refine : Membership.mem (γ := Set (PrimeSpectrum ((i : ι) → R i))) (Set.range (sigmaToPi R)) { asIdeal := I, isPrime := sorry } →
  ∀ (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 := sorry }),
    False
Tactic: refine ⟨I, max, fun ⟨⟨i, p⟩, eq⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (hypothesis)
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 := ⋯ }
⊢ False
have this : (⇑(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
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (hypothesis)
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))
⊢ False
have this₁ : (⇑(DFinsupp.single (β := R) i 1) : (a : ι) → R a) ∉ asIdeal { asIdeal := I, isPrime := sorry }
Tactic: rw [eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
inst_1 : Infinite ι
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
let let₁ let₂ :
  ∃ (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)
have let₃ : let 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' := sorry };
∀ (I : Ideal ((i : ι) → R i)) (max : I.IsMaximal) (le : J ≤ I),
  ∃ (I : Ideal ((i : ι) → R i)) (x : I.IsMaximal), { asIdeal := I, isPrime := sorry } ∉ Set.range (sigmaToPi R)
Tactic: classical
  let J : Ideal (Π i, R i) := -- `J := Π₀ i, R i` is an ideal in `Π i, R i`
  { __ := AddMonoidHom.mrange DFinsupp.coeFnAddMonoidHom
    smul_mem' := by
      rintro r _ ⟨x, rfl⟩
      refine ⟨.mk x.support fun i ↦ r i * x i, funext fun i ↦ show dite _ _ _ = _ from ?_⟩
      simp_rw +instances [DFinsupp.coeFnAddMonoidHom]
      refine dite_eq_left_iff.mpr fun h ↦ ?_
      rw [DFinsupp.notMem_support_iff.mp h, mul_zero] }
  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
  refine ⟨I, max, fun ⟨⟨i, p⟩, eq⟩ ↦ ?_⟩
  -- then I is not in the range of `sigmaToPi`
  have : ⇑(DFinsupp.single i 1) ∉ (sigmaToPi R ⟨i, p⟩).asIdeal := by
    simpa using p.1.ne_top_iff_one.mp p.2.ne_top
  rw [eq] at this
  exact this (le ⟨.single i 1, rfl⟩)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.RingHom (goal)
Goal:
ι : Type u_3
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
inst_1 : Infinite ι
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
let let₁ let₂ :
  ∃ (I : Ideal ((i : ι) → R i)) (x : I.IsMaximal), { asIdeal := I, isPrime := ⋯ } ∉ Set.range (sigmaToPi R)
let₃ :
  let 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)
⊢ ∃ (I : Ideal ((i : ι) → R i)) (x : I.IsMaximal), { asIdeal := I, isPrime := ⋯ } ∉ Set.range (sigmaToPi R)
have let₄ : let 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' := sorry };
∀ (I : Ideal ((i : ι) → R i)) (max : I.IsMaximal) (le : J ≤ I),
  Membership.mem (γ := Set (PrimeSpectrum ((i : ι) → R i))) (Set.range (sigmaToPi R)) { asIdeal := I, isPrime := sorry } →
    ∀ (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 := sorry }),
      False
Tactic: classical
  let J : Ideal (Π i, R i) := -- `J := Π₀ i, R i` is an ideal in `Π i, R i`
  { __ := AddMonoidHom.mrange DFinsupp.coeFnAddMonoidHom
    smul_mem' := by
      rintro r _ ⟨x, rfl⟩
      refine ⟨.mk x.support fun i ↦ r i * x i, funext fun i ↦ show dite _ _ _ = _ from ?_⟩
      simp_rw +instances [DFinsupp.coeFnAddMonoidHom]
      refine dite_eq_left_iff.mpr fun h ↦ ?_
      rw [DFinsupp.notMem_support_iff.mp h, mul_zero] }
  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
  refine ⟨I, max, fun ⟨⟨i, p⟩, eq⟩ ↦ ?_⟩
  -- then I is not in the range of `sigmaToPi`
  have : ⇑(DFinsupp.single i 1) ∉ (sigmaToPi R ⟨i, p⟩).asIdeal := by
    simpa using p.1.ne_top_iff_one.mp p.2.ne_top
  rw [eq] at this
  exact this (le ⟨.single i 1, rfl⟩)
-- 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: cases nonempty_fintype ι
-- 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
⊢ Eq (α := (i : ι) → R i) (∏ i : ι, e i) 0
have h : ∀ (j : ι), Eq.{u_4 + 1} (α := R j) ((∏ i : ι, e i) j) (0 j)
Tactic: ext 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
j : ι
⊢ Eq.{u_4 + 1} (α := R j) ((∏ i : ι, e i) j) (0 j)
have h : e j j = 0
Tactic: rw [Finset.prod_apply, Pi.zero_apply, Finset.prod_eq_zero (Finset.mem_univ j)]
-- 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
⊢ ∃ (i : ι) (q : PrimeSpectrum (R i)), comap (Pi.evalRingHom R i) q = p
have H : 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]
-- 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 : ι) (q : PrimeSpectrum (R i)), comap (Pi.evalRingHom R i) q = p
have intro : ∀ (i : ι) (hi : e i ∈ p.asIdeal), ∃ (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
-- 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
⊢ x ∈ p.asIdeal
have h : x = x * e i
Tactic: convert! p.asIdeal.mul_mem_left x hi
-- 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
⊢ x = x * e i
have h : ∀ (j : ι), x j = (x * e i) j
Tactic: ext 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 : ι
⊢ x j = (x * e i) j
have pos : ∀ (hj : i = j), x j = (x * e i) j
Tactic: by_cases hj : i = j