English
If p < q are primes in R and Q lies over q in S, there exists P < Q prime with P lies over p.
Русский
Если p < q — простые в R и Q лежит над q в S, то существует P < Q, P — простое, и P лежит над p.
LaTeX
$$$\forall R,S\,[\text{CommRing } R][\text{CommRing } S][\text{Algebra } R S]\; [p:q: \text{Ideal } R][p.IsPrime][q.IsPrime] (Q: \text{Ideal } S)[Q.IsPrime][Q.LiesOver q] (hpq: p < q) \Rightarrow \exists P < Q, P.IsPrime \land P.LiesOver p.$$$
Lean4
theorem exists_ideal_lt_liesOver_of_lt [Algebra.HasGoingDown R S] {p q : Ideal R} [p.IsPrime] [q.IsPrime] (Q : Ideal S)
[Q.IsPrime] [Q.LiesOver q] (hpq : p < q) : ∃ P < Q, P.IsPrime ∧ P.LiesOver p :=
by
obtain ⟨P, hPQ, _, _⟩ := Q.exists_ideal_le_liesOver_of_le (p := p) (q := q) hpq.le
refine ⟨P, ?_, inferInstance, inferInstance⟩
by_contra hc
have : P = Q := eq_of_le_of_not_lt hPQ hc
subst this
simp [P.over_def p, P.over_def q] at hpq
