-- Mathlib/RingTheory/Ideal/GoingUp.lean
lemma exists_ideal_comap_le_prime (P : Ideal R) [P.IsPrime]
    (I : Ideal S) (hI : I.comap (algebraMap R S) ≤ P) :
    ∃ Q ≥ I, Q.IsPrime ∧ Q.comap (algebraMap R S) ≤ P

Proof state:
case intro.intro
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Ideal R
inst✝ : P.IsPrime
I : Ideal S
hI : comap (algebraMap R S) I ≤ P
Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)
Iₚ : Ideal Sₚ := map (algebraMap S Sₚ) I
hI' : Disjoint ↑(Algebra.algebraMapSubmonoid S P.primeCompl) ↑I
this : Iₚ ≠ ⊤
M : Ideal Sₚ
hM : M.IsMaximal
hM' : Iₚ ≤ M
x : R
hx : x ∈ comap (algebraMap R S) (comap (algebraMap S Sₚ) M)
⊢ x ∈ P

Tactic:
by_contra hx'

Result:
case intro.intro
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Ideal R
inst✝ : P.IsPrime
I : Ideal S
hI : comap (algebraMap R S) I ≤ P
Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)
Iₚ : Ideal Sₚ := map (algebraMap S Sₚ) I
hI' : Disjoint ↑(Algebra.algebraMapSubmonoid S P.primeCompl) ↑I
this : Iₚ ≠ ⊤
M : Ideal Sₚ
hM : M.IsMaximal
hM' : Iₚ ≤ M
x : R
hx : x ∈ comap (algebraMap R S) (comap (algebraMap S Sₚ) M)
hx' : x ∉ P
⊢ False

Proof state:
case intro.intro
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Ideal R
inst✝ : P.IsPrime
I : Ideal S
hI : comap (algebraMap R S) I ≤ P
Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)
Iₚ : Ideal Sₚ := map (algebraMap S Sₚ) I
hI' : Disjoint ↑(Algebra.algebraMapSubmonoid S P.primeCompl) ↑I
this : Iₚ ≠ ⊤
M : Ideal Sₚ
hM : M.IsMaximal
hM' : Iₚ ≤ M
⊢ ∃ Q ≥ I, Q.IsPrime ∧ comap (algebraMap R S) Q ≤ P

Tactic:
refine ⟨_, Ideal.map_le_iff_le_comap.mp hM', hM.isPrime.comap _, ?_⟩

Result:
case intro.intro
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Ideal R
inst✝ : P.IsPrime
I : Ideal S
hI : comap (algebraMap R S) I ≤ P
Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)
Iₚ : Ideal Sₚ := map (algebraMap S Sₚ) I
hI' : Disjoint ↑(Algebra.algebraMapSubmonoid S P.primeCompl) ↑I
this : Iₚ ≠ ⊤
M : Ideal Sₚ
hM : M.IsMaximal
hM' : Iₚ ≤ M
⊢ comap (algebraMap R S) (comap (algebraMap S Sₚ) M) ≤ P

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Ideal R
inst✝ : P.IsPrime
I : Ideal S
hI : comap (algebraMap R S) I ≤ P
⊢ ∃ Q ≥ I, Q.IsPrime ∧ comap (algebraMap R S) Q ≤ P

Tactic:
let Sₚ := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)

Result:
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Ideal R
inst✝ : P.IsPrime
I : Ideal S
hI : comap (algebraMap R S) I ≤ P
Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)
⊢ ∃ Q ≥ I, Q.IsPrime ∧ comap (algebraMap R S) Q ≤ P

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Ideal R
inst✝ : P.IsPrime
I : Ideal S
hI : comap (algebraMap R S) I ≤ P
Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)
⊢ ∃ Q ≥ I, Q.IsPrime ∧ comap (algebraMap R S) Q ≤ P

Tactic:
let Iₚ := I.map (algebraMap S Sₚ)

Result:
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Ideal R
inst✝ : P.IsPrime
I : Ideal S
hI : comap (algebraMap R S) I ≤ P
Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)
Iₚ : Ideal Sₚ := map (algebraMap S Sₚ) I
⊢ ∃ Q ≥ I, Q.IsPrime ∧ comap (algebraMap R S) Q ≤ P

Proof state:
case intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Ideal R
inst✝ : P.IsPrime
I : Ideal S
hI : comap (algebraMap R S) I ≤ P
Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)
Iₚ : Ideal Sₚ := map (algebraMap S Sₚ) I
x : R
hx : x ∉ P
hx' : (algebraMap R S) x ∈ ↑I
⊢ (algebraMap R S) x ∈ ∅

Tactic:
exact (hx (hI hx')).elim

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Ideal R
inst✝ : P.IsPrime
I : Ideal S
hI : comap (algebraMap R S) I ≤ P
Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)
Iₚ : Ideal Sₚ := map (algebraMap S Sₚ) I
hI' : Disjoint ↑(Algebra.algebraMapSubmonoid S P.primeCompl) ↑I
⊢ ∀ (x : ↥I × ↥(Algebra.algebraMapSubmonoid S P.primeCompl)), ¬1 * (algebraMap S Sₚ) ↑x.2 = (algebraMap S Sₚ) ↑x.1

Tactic:
simp only [one_mul, IsLocalization.eq_iff_exists (Algebra.algebraMapSubmonoid S P.primeCompl),
  not_exists]

Result:
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Ideal R
inst✝ : P.IsPrime
I : Ideal S
hI : comap (algebraMap R S) I ≤ P
Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)
Iₚ : Ideal Sₚ := map (algebraMap S Sₚ) I
hI' : Disjoint ↑(Algebra.algebraMapSubmonoid S P.primeCompl) ↑I
⊢ ∀ (x : ↥I × ↥(Algebra.algebraMapSubmonoid S P.primeCompl)) (x_1 : ↥(Algebra.algebraMapSubmonoid S P.primeCompl)),
    ¬↑x_1 * ↑x.2 = ↑x_1 * ↑x.1

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Ideal R
inst✝ : P.IsPrime
I : Ideal S
hI : comap (algebraMap R S) I ≤ P
Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)
Iₚ : Ideal Sₚ := map (algebraMap S Sₚ) I
⊢ ↑(Algebra.algebraMapSubmonoid S P.primeCompl) ∩ ↑I ⊆ ∅

Tactic:
rintro _ ⟨⟨x, hx : x ∉ P, rfl⟩, hx'⟩

Result:
case intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Ideal R
inst✝ : P.IsPrime
I : Ideal S
hI : comap (algebraMap R S) I ≤ P
Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)
Iₚ : Ideal Sₚ := map (algebraMap S Sₚ) I
x : R
hx : x ∉ P
hx' : (algebraMap R S) x ∈ ↑I
⊢ (algebraMap R S) x ∈ ∅

Proof state:
case intro.intro
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Ideal R
inst✝ : P.IsPrime
I : Ideal S
hI : comap (algebraMap R S) I ≤ P
Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)
Iₚ : Ideal Sₚ := map (algebraMap S Sₚ) I
hI' : Disjoint ↑(Algebra.algebraMapSubmonoid S P.primeCompl) ↑I
this : Iₚ ≠ ⊤
M : Ideal Sₚ
hM : M.IsMaximal
hM' : Iₚ ≤ M
⊢ comap (algebraMap R S) (comap (algebraMap S Sₚ) M) ≤ P

Tactic:
intro x hx

Result:
case intro.intro
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Ideal R
inst✝ : P.IsPrime
I : Ideal S
hI : comap (algebraMap R S) I ≤ P
Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)
Iₚ : Ideal Sₚ := map (algebraMap S Sₚ) I
hI' : Disjoint ↑(Algebra.algebraMapSubmonoid S P.primeCompl) ↑I
this : Iₚ ≠ ⊤
M : Ideal Sₚ
hM : M.IsMaximal
hM' : Iₚ ≤ M
x : R
hx : x ∈ comap (algebraMap R S) (comap (algebraMap S Sₚ) M)
⊢ x ∈ P

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Ideal R
inst✝ : P.IsPrime
I : Ideal S
hI : comap (algebraMap R S) I ≤ P
Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)
Iₚ : Ideal Sₚ := map (algebraMap S Sₚ) I
⊢ Disjoint ↑(Algebra.algebraMapSubmonoid S P.primeCompl) ↑I

Tactic:
rw [Set.disjoint_iff]

Result:
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Ideal R
inst✝ : P.IsPrime
I : Ideal S
hI : comap (algebraMap R S) I ≤ P
Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)
Iₚ : Ideal Sₚ := map (algebraMap S Sₚ) I
⊢ ↑(Algebra.algebraMapSubmonoid S P.primeCompl) ∩ ↑I ⊆ ∅