∀ {ι : Type u_2} (R : ι → Type u_1) [inst : (i : ι) → CommSemiring (R i)]
  (motive : (∃ I, ∃ (x : I.IsMaximal), { asIdeal := I, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)) → Prop)
  (x : ∃ I, ∃ (x : I.IsMaximal), { asIdeal := I, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)),
  (∀ (w : Ideal ((i : ι) → R i)) (w_1 : w.IsMaximal)
      (notMem : { asIdeal := w, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)), motive ⋯) →
    motive x