case intro.intro
R : Type u_2
inst✝³ : CommRing R
S : Type u_1
inst✝² : CommRing S
f : R →+* S
I J : Ideal S
inst✝¹ : Algebra R S
inst✝ : IsDomain S
H : Algebra.IsIntegral R S
P : Ideal R
P_max : IsMaximal P
hP : RingHom.ker (algebraMap R S) ≤ P
Q : Ideal S
Q_prime : IsPrime Q
hQ : comap (algebraMap R S) Q = P
⊢ ∃ Q, IsMaximal Q ∧ comap (algebraMap R S) Q = P
R : Type u_2
inst✝³ : CommRing R
S : Type u_1
inst✝² : CommRing S
f : R →+* S
I J : Ideal S
inst✝¹ : Algebra R S
inst✝ : IsDomain S
H : Algebra.IsIntegral R S
P : Ideal R
P_max : IsMaximal P
hP : RingHom.ker (algebraMap R S) ≤ P
⊢ ∃ Q, IsMaximal Q ∧ comap (algebraMap R S) Q = P
obtain ⟨Q, ⟨Q_prime, hQ⟩⟩ := exists_ideal_over_prime_of_is_integral' H P hP
case intro.intro
R : Type u_2
inst✝³ : CommRing R
S : Type u_1
inst✝² : CommRing S
f : R →+* S
I J : Ideal S
inst✝¹ : Algebra R S
inst✝ : IsDomain S
H : Algebra.IsIntegral R S
P : Ideal R
P_max : IsMaximal P
hP : RingHom.ker (algebraMap R S) ≤ P
Q : Ideal S
Q_prime : IsPrime Q
hQ : comap (algebraMap R S) Q = P
this : IsPrime Q
⊢ ∃ Q, IsMaximal Q ∧ comap (algebraMap R S) Q = P
case intro.intro
R : Type u_2
inst✝³ : CommRing R
S : Type u_1
inst✝² : CommRing S
f : R →+* S
I J : Ideal S
inst✝¹ : Algebra R S
inst✝ : IsDomain S
H : Algebra.IsIntegral R S
P : Ideal R
P_max : IsMaximal P
hP : RingHom.ker (algebraMap R S) ≤ P
Q : Ideal S
Q_prime : IsPrime Q
hQ : comap (algebraMap R S) Q = P
⊢ ∃ Q, IsMaximal Q ∧ comap (algebraMap R S) Q = P
haveI : Q.IsPrime := Q_prime
no goals
case intro.intro
R : Type u_2
inst✝³ : CommRing R
S : Type u_1
inst✝² : CommRing S
f : R →+* S
I J : Ideal S
inst✝¹ : Algebra R S
inst✝ : IsDomain S
H : Algebra.IsIntegral R S
P : Ideal R
P_max : IsMaximal P
hP : RingHom.ker (algebraMap R S) ≤ P
Q : Ideal S
Q_prime : IsPrime Q
hQ : comap (algebraMap R S) Q = P
this : IsPrime Q
⊢ ∃ Q, IsMaximal Q ∧ comap (algebraMap R S) Q = P
exact ⟨Q, isMaximal_of_isIntegral_of_isMaximal_comap H _ (hQ.symm ▸ P_max), hQ⟩