∀ {R : Type u_2} [inst : CommSemiring R] {S : Type u_1} [inst_1 : CommRing S] [inst_2 : Algebra R S] {I : Ideal R}
  {J : Ideal S} (q : Ideal S) (motive : q.IsPrime ∧ Ideal.map (algebraMap R S) I ⊔ J ≤ q → Prop)
  (x : q.IsPrime ∧ Ideal.map (algebraMap R S) I ⊔ J ≤ q),
  (∀ (left : q.IsPrime) (hleq : Ideal.map (algebraMap R S) I ⊔ J ≤ q), motive ⋯) → motive x