∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P Q : Ideal S}
  [P.IsPrime] [inst_4 : Q.IsPrime], P ≤ Q → Ideal.under R P = Ideal.under R Q → ∀ [Algebra.QuasiFiniteAt R Q], P = Q