-- Mathlib/RingTheory/Ideal/GoingDown.lean
lemma Ideal.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

Proof state:
case intro.intro.intro
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
hpq : p < q
P : Ideal S
hPQ : P ≤ Q
left✝ : P.IsPrime
right✝ : P.LiesOver p
hc : ¬P < Q
this : P = Q
⊢ False

Tactic:
subst this

Result:
case intro.intro.intro
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
hpq : p < q
P : Ideal S
left✝ : P.IsPrime
right✝ : P.LiesOver p
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver q
hPQ : P ≤ P
hc : ¬P < P
⊢ False

Proof state:
case intro.intro.intro
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
hpq : p < q
P : Ideal S
hPQ : P ≤ Q
left✝ : P.IsPrime
right✝ : P.LiesOver p
⊢ P < Q

Tactic:
by_contra hc

Result:
case intro.intro.intro
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
hpq : p < q
P : Ideal S
hPQ : P ≤ Q
left✝ : P.IsPrime
right✝ : P.LiesOver p
hc : ¬P < Q
⊢ False

Proof state:
case intro.intro.intro
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
hpq : p < q
P : Ideal S
left✝ : P.IsPrime
right✝ : P.LiesOver p
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver q
hPQ : P ≤ P
hc : ¬P < P
⊢ False

Tactic:
simp [P.over_def p, P.over_def q] at hpq

Result:
no goals

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
hpq : p < q
⊢ ∃ P < Q, P.IsPrime ∧ P.LiesOver p

Tactic:
obtain ⟨P, hPQ, _, _⟩ := Q.exists_ideal_le_liesOver_of_le (p := p) (q := q) hpq.le

Result:
case intro.intro.intro
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
hpq : p < q
P : Ideal S
hPQ : P ≤ Q
left✝ : P.IsPrime
right✝ : P.LiesOver p
⊢ ∃ P < Q, P.IsPrime ∧ P.LiesOver p

Proof state:
case intro.intro.intro
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
hpq : p < q
P : Ideal S
hPQ : P ≤ Q
left✝ : P.IsPrime
right✝ : P.LiesOver p
hc : ¬P < Q
⊢ False

Tactic:
have : P = Q := eq_of_le_of_not_lt hPQ hc

Result:
case intro.intro.intro
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
hpq : p < q
P : Ideal S
hPQ : P ≤ Q
left✝ : P.IsPrime
right✝ : P.LiesOver p
hc : ¬P < Q
this : P = Q
⊢ False

Proof state:
case intro.intro.intro
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
hpq : p < q
P : Ideal S
hPQ : P ≤ Q
left✝ : P.IsPrime
right✝ : P.LiesOver p
⊢ ∃ P < Q, P.IsPrime ∧ P.LiesOver p

Tactic:
refine ⟨P, ?_, inferInstance, inferInstance⟩

Result:
case intro.intro.intro
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
hpq : p < q
P : Ideal S
hPQ : P ≤ Q
left✝ : P.IsPrime
right✝ : P.LiesOver p
⊢ P < Q