R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
f : R →+* S
I J : Ideal S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
inst✝ : IsDomain S
hRS : Algebra.IsIntegral R S
hI : comap (algebraMap R S) I = ⊥
x : S
hx : x ∈ I
⊢ x ∈ ⊥
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
f : R →+* S
I J : Ideal S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
inst✝ : IsDomain S
hRS : Algebra.IsIntegral R S
hI : comap (algebraMap R S) I = ⊥
⊢ I = ⊥
refine' eq_bot_iff.2 fun x hx => _
case pos
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
f : R →+* S
I J : Ideal S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
inst✝ : IsDomain S
hRS : Algebra.IsIntegral R S
hI : comap (algebraMap R S) I = ⊥
x : S
hx : x ∈ I
hx0 : x = 0
⊢ x ∈ ⊥

case neg
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
f : R →+* S
I J : Ideal S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
inst✝ : IsDomain S
hRS : Algebra.IsIntegral R S
hI : comap (algebraMap R S) I = ⊥
x : S
hx : x ∈ I
hx0 : ¬x = 0
⊢ x ∈ ⊥
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
f : R →+* S
I J : Ideal S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
inst✝ : IsDomain S
hRS : Algebra.IsIntegral R S
hI : comap (algebraMap R S) I = ⊥
x : S
hx : x ∈ I
⊢ x ∈ ⊥
by_cases hx0 : x = 0
no goals
case pos
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
f : R →+* S
I J : Ideal S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
inst✝ : IsDomain S
hRS : Algebra.IsIntegral R S
hI : comap (algebraMap R S) I = ⊥
x : S
hx : x ∈ I
hx0 : x = 0
⊢ x ∈ ⊥
exact hx0.symm ▸ Ideal.zero_mem ⊥
no goals
case neg
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
f : R →+* S
I J : Ideal S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
inst✝ : IsDomain S
hRS : Algebra.IsIntegral R S
hI : comap (algebraMap R S) I = ⊥
x : S
hx : x ∈ I
hx0 : ¬x = 0
⊢ x ∈ ⊥
exact absurd hI (comap_ne_bot_of_integral_mem hx0 hx (hRS x))