-- 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)
hx' : x ∉ P
⊢ False

Tactic:
exact Set.disjoint_left.mp ((IsLocalization.isPrime_iff_isPrime_disjoint
  (Algebra.algebraMapSubmonoid S P.primeCompl) Sₚ M).mp hM.isPrime).2 ⟨_, hx', rfl⟩ hx

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)) (x_1 : ↥(Algebra.algebraMapSubmonoid S P.primeCompl)),
    ¬↑x_1 * ↑x.2 = ↑x_1 * ↑x.1

Tactic:
exact fun x c ↦ hI'.ne_of_mem (mul_mem c.2 x.2.2) (I.mul_mem_left c x.1.2)

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
⊢ ∃ Q ≥ I, Q.IsPrime ∧ comap (algebraMap R S) Q ≤ P

Tactic:
have : Iₚ ≠ ⊤ := by
  rw [Ne, Ideal.eq_top_iff_one, IsLocalization.mem_map_algebraMap_iff
    (Algebra.algebraMapSubmonoid S P.primeCompl) Sₚ, not_exists]
  simp only [one_mul, IsLocalization.eq_iff_exists (Algebra.algebraMapSubmonoid S P.primeCompl),
    not_exists]
  exact fun x c ↦ hI'.ne_of_mem (mul_mem c.2 x.2.2) (I.mul_mem_left c x.1.2)

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
this : Iₚ ≠ ⊤
⊢ ∃ 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)
Iₚ : Ideal Sₚ := map (algebraMap S Sₚ) I
⊢ ∃ Q ≥ I, Q.IsPrime ∧ comap (algebraMap R S) Q ≤ P

Tactic:
have hI' : Disjoint (Algebra.algebraMapSubmonoid S P.primeCompl : Set S) I := by
  rw [Set.disjoint_iff]
  rintro _ ⟨⟨x, hx : x ∉ P, rfl⟩, hx'⟩
  exact (hx (hI hx')).elim

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
⊢ ∃ 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)
Iₚ : Ideal Sₚ := map (algebraMap S Sₚ) I
hI' : Disjoint ↑(Algebra.algebraMapSubmonoid S P.primeCompl) ↑I
this : Iₚ ≠ ⊤
⊢ ∃ Q ≥ I, Q.IsPrime ∧ comap (algebraMap R S) Q ≤ P

Tactic:
obtain ⟨M, hM, hM'⟩ := Ideal.exists_le_maximal _ this

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
⊢ ∃ 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)
Iₚ : Ideal Sₚ := map (algebraMap S Sₚ) I
hI' : Disjoint ↑(Algebra.algebraMapSubmonoid S P.primeCompl) ↑I
⊢ Iₚ ≠ ⊤

Tactic:
rw [Ne, Ideal.eq_top_iff_one, IsLocalization.mem_map_algebraMap_iff
  (Algebra.algebraMapSubmonoid S P.primeCompl) Sₚ, 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)), ¬1 * (algebraMap S Sₚ) ↑x.2 = (algebraMap S Sₚ) ↑x.1