-- Mathlib/RingTheory/Ideal/GoingDown.lean
lemma Ideal.exists_ideal_le_liesOver_of_le [Algebra.HasGoingDown R S]
    {p q : Ideal R} [p.IsPrime] [q.IsPrime] (Q : Ideal S) [Q.IsPrime] [Q.LiesOver q]
    (hle : p ≤ q) :
    ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Proof state:
case pos
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra.HasGoingDown R S
p q : Ideal R
inst✝³ : p.IsPrime
inst✝² : q.IsPrime
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : Q.LiesOver q
hle : p ≤ q
h : p = q
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
subst h

Result:
case pos
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra.HasGoingDown R S
p : Ideal R
inst✝³ : p.IsPrime
Q : Ideal S
inst✝² : Q.IsPrime
inst✝¹ : p.IsPrime
inst✝ : Q.LiesOver p
hle : p ≤ p
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Proof state:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra.HasGoingDown R S
p q : Ideal R
inst✝³ : p.IsPrime
inst✝² : q.IsPrime
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : Q.LiesOver q
hle : p ≤ q
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
by_cases h : p = q

Result:
case pos
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra.HasGoingDown R S
p q : Ideal R
inst✝³ : p.IsPrime
inst✝² : q.IsPrime
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : Q.LiesOver q
hle : p ≤ q
h : p = q
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

case neg
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra.HasGoingDown R S
p q : Ideal R
inst✝³ : p.IsPrime
inst✝² : q.IsPrime
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : Q.LiesOver q
hle : p ≤ q
h : ¬p = q
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Proof state:
case neg
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra.HasGoingDown R S
p q : Ideal R
inst✝³ : p.IsPrime
inst✝² : q.IsPrime
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : Q.LiesOver q
hle : p ≤ q
h : ¬p = q
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
have := Q.over_def q

Result:
case neg
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra.HasGoingDown R S
p q : Ideal R
inst✝³ : p.IsPrime
inst✝² : q.IsPrime
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : Q.LiesOver q
hle : p ≤ q
h : ¬p = q
this : q = under R Q
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Proof state:
case neg
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra.HasGoingDown R S
p q : Ideal R
inst✝³ : p.IsPrime
inst✝² : q.IsPrime
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : Q.LiesOver q
hle : p ≤ q
h : ¬p = q
this : q = under R Q
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
subst this

Result:
case neg
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra.HasGoingDown R S
p : Ideal R
inst✝³ : p.IsPrime
Q : Ideal S
inst✝² : Q.IsPrime
inst✝¹ : (under R Q).IsPrime
inst✝ : Q.LiesOver (under R Q)
hle : p ≤ under R Q
h : ¬p = under R Q
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Proof state:
case neg
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra.HasGoingDown R S
p : Ideal R
inst✝³ : p.IsPrime
Q : Ideal S
inst✝² : Q.IsPrime
inst✝¹ : (under R Q).IsPrime
inst✝ : Q.LiesOver (under R Q)
hle : p ≤ under R Q
h : ¬p = under R Q
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
exact Algebra.HasGoingDown.exists_ideal_le_liesOver_of_lt Q (lt_of_le_of_ne hle h)

Result:
no goals

Proof state:
case pos
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra.HasGoingDown R S
p : Ideal R
inst✝³ : p.IsPrime
Q : Ideal S
inst✝² : Q.IsPrime
inst✝¹ : p.IsPrime
inst✝ : Q.LiesOver p
hle : p ≤ p
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
use Q

Result:
no goals