-- Mathlib/RingTheory/Ideal/GoingUp.lean
theorem exists_ideal_over_prime_of_isIntegral_of_isDomain [Algebra.IsIntegral R S] (P : Ideal R)
    [IsPrime P] (hP : RingHom.ker (algebraMap R S) ≤ P) :
    ∃ Q : Ideal S, IsPrime Q ∧ Q.comap (algebraMap R S) = P

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : Algebra.IsIntegral R S
P : Ideal R
inst✝ : P.IsPrime
hP : RingHom.ker (algebraMap R S) ≤ P
⊢ ∃ Q, Q.IsPrime ∧ comap (algebraMap R S) Q = P

Tactic:
have hP0 : (0 : S) ∉ Algebra.algebraMapSubmonoid S P.primeCompl := by
  rintro ⟨x, ⟨hx, x0⟩⟩
  exact absurd (hP x0) hx

Result:
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : Algebra.IsIntegral R S
P : Ideal R
inst✝ : P.IsPrime
hP : RingHom.ker (algebraMap R S) ≤ P
hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl
⊢ ∃ Q, Q.IsPrime ∧ comap (algebraMap R S) Q = P

Proof state:
case intro
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : Algebra.IsIntegral R S
P : Ideal R
inst✝ : P.IsPrime
hP : RingHom.ker (algebraMap R S) ≤ P
hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization P.primeCompl
Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)
this✝ : IsDomain (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) :=
  IsLocalization.isDomain_localization (le_nonZeroDivisors_of_noZeroDivisors hP0)
Qₚ : Ideal Sₚ
Qₚ_maximal : Qₚ.IsMaximal
x✝ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this : Algebra.IsIntegral Rₚ Sₚ
⊢ ∃ Q, Q.IsPrime ∧ comap (algebraMap R S) Q = P

Tactic:
have Qₚ_max : IsMaximal (comap _ Qₚ) :=
  isMaximal_comap_of_isIntegral_of_isMaximal (R := Rₚ) (S := Sₚ) Qₚ

Result:
case intro
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : Algebra.IsIntegral R S
P : Ideal R
inst✝ : P.IsPrime
hP : RingHom.ker (algebraMap R S) ≤ P
hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization P.primeCompl
Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)
this✝ : IsDomain (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) :=
  IsLocalization.isDomain_localization (le_nonZeroDivisors_of_noZeroDivisors hP0)
Qₚ : Ideal Sₚ
Qₚ_maximal : Qₚ.IsMaximal
x✝ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this : Algebra.IsIntegral Rₚ Sₚ
Qₚ_max : (comap (algebraMap Rₚ Sₚ) Qₚ).IsMaximal
⊢ ∃ Q, Q.IsPrime ∧ comap (algebraMap R S) Q = P

Proof state:
case intro
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : Algebra.IsIntegral R S
P : Ideal R
inst✝ : P.IsPrime
hP : RingHom.ker (algebraMap R S) ≤ P
hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization P.primeCompl
Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)
this : IsDomain (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) :=
  IsLocalization.isDomain_localization (le_nonZeroDivisors_of_noZeroDivisors hP0)
Qₚ : Ideal Sₚ
Qₚ_maximal : Qₚ.IsMaximal
x✝ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
⊢ ∃ Q, Q.IsPrime ∧ comap (algebraMap R S) Q = P

Tactic:
have : Algebra.IsIntegral Rₚ Sₚ := ⟨isIntegral_localization⟩

Result:
case intro
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : Algebra.IsIntegral R S
P : Ideal R
inst✝ : P.IsPrime
hP : RingHom.ker (algebraMap R S) ≤ P
hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization P.primeCompl
Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)
this✝ : IsDomain (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) :=
  IsLocalization.isDomain_localization (le_nonZeroDivisors_of_noZeroDivisors hP0)
Qₚ : Ideal Sₚ
Qₚ_maximal : Qₚ.IsMaximal
x✝ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this : Algebra.IsIntegral Rₚ Sₚ
⊢ ∃ Q, Q.IsPrime ∧ comap (algebraMap R S) Q = P

Proof state:
case intro.intro
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : Algebra.IsIntegral R S
P : Ideal R
inst✝ : P.IsPrime
hP : RingHom.ker (algebraMap R S) ≤ P
x : R
hx : x ∈ ↑P.primeCompl
x0 : (algebraMap R S) x = 0
⊢ False

Tactic:
exact absurd (hP x0) hx

Result:
no goals

Proof state:
case intro
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : Algebra.IsIntegral R S
P : Ideal R
inst✝ : P.IsPrime
hP : RingHom.ker (algebraMap R S) ≤ P
hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization P.primeCompl
Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)
this✝ : IsDomain (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) :=
  IsLocalization.isDomain_localization (le_nonZeroDivisors_of_noZeroDivisors hP0)
Qₚ : Ideal Sₚ
Qₚ_maximal : Qₚ.IsMaximal
x✝ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this : Algebra.IsIntegral Rₚ Sₚ
Qₚ_max : (comap (algebraMap Rₚ Sₚ) Qₚ).IsMaximal
⊢ ∃ Q, Q.IsPrime ∧ comap (algebraMap R S) Q = P

Tactic:
refine ⟨comap (algebraMap S Sₚ) Qₚ, ⟨comap_isPrime _ Qₚ, ?_⟩⟩

Result:
case intro
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : Algebra.IsIntegral R S
P : Ideal R
inst✝ : P.IsPrime
hP : RingHom.ker (algebraMap R S) ≤ P
hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization P.primeCompl
Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)
this✝ : IsDomain (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) :=
  IsLocalization.isDomain_localization (le_nonZeroDivisors_of_noZeroDivisors hP0)
Qₚ : Ideal Sₚ
Qₚ_maximal : Qₚ.IsMaximal
x✝ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this : Algebra.IsIntegral Rₚ Sₚ
Qₚ_max : (comap (algebraMap Rₚ Sₚ) Qₚ).IsMaximal
⊢ comap (algebraMap R S) (comap (algebraMap S Sₚ) Qₚ) = P

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : Algebra.IsIntegral R S
P : Ideal R
inst✝ : P.IsPrime
hP : RingHom.ker (algebraMap R S) ≤ P
⊢ 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl

Tactic:
rintro ⟨x, ⟨hx, x0⟩⟩

Result:
case intro.intro
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : Algebra.IsIntegral R S
P : Ideal R
inst✝ : P.IsPrime
hP : RingHom.ker (algebraMap R S) ≤ P
x : R
hx : x ∈ ↑P.primeCompl
x0 : (algebraMap R S) x = 0
⊢ False

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : Algebra.IsIntegral R S
P : Ideal R
inst✝ : P.IsPrime
hP : RingHom.ker (algebraMap R S) ≤ P
hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization P.primeCompl
Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)
⊢ ∃ Q, Q.IsPrime ∧ comap (algebraMap R S) Q = P

Tactic:
letI : IsDomain (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) :=
  IsLocalization.isDomain_localization (le_nonZeroDivisors_of_noZeroDivisors hP0)

Result:
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : Algebra.IsIntegral R S
P : Ideal R
inst✝ : P.IsPrime
hP : RingHom.ker (algebraMap R S) ≤ P
hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization P.primeCompl
Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)
this : IsDomain (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) :=
  IsLocalization.isDomain_localization (le_nonZeroDivisors_of_noZeroDivisors hP0)
⊢ ∃ Q, Q.IsPrime ∧ comap (algebraMap R S) Q = P