-- 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)
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),
    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)
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 })
      (this :
        (⇑(DFinsupp.single (β := R) i 1) : (a : ι) → R a) ∉
          asIdeal (sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i p))),
      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⟩)