case intro.intro
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1079360
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
K : Type u_2
K' : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Field K'
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : Algebra R K'
inst✝¹ : IsFractionRing R K'
I J : FractionalIdeal R⁰ K
h : K →ₐ[R] K'
inst✝ : Nontrivial R
hI : I ≠ 0
x : R
x_ne_zero : x ≠ 0
hx : ↑(algebraMap R K) x ∈ I
⊢ map h I ≠ 0
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1079360
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
K : Type u_2
K' : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Field K'
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : Algebra R K'
inst✝¹ : IsFractionRing R K'
I J : FractionalIdeal R⁰ K
h : K →ₐ[R] K'
inst✝ : Nontrivial R
hI : I ≠ 0
⊢ map h I ≠ 0
obtain ⟨x, x_ne_zero, hx⟩ := exists_ne_zero_mem_isInteger hI
case intro.intro
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1079360
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
K : Type u_2
K' : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Field K'
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : Algebra R K'
inst✝¹ : IsFractionRing R K'
I J : FractionalIdeal R⁰ K
h : K →ₐ[R] K'
inst✝ : Nontrivial R
hI : I ≠ 0
x : R
hx : ↑(algebraMap R K) x ∈ I
map_eq_zero : map h I = 0
⊢ x = 0
case intro.intro
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1079360
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
K : Type u_2
K' : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Field K'
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : Algebra R K'
inst✝¹ : IsFractionRing R K'
I J : FractionalIdeal R⁰ K
h : K →ₐ[R] K'
inst✝ : Nontrivial R
hI : I ≠ 0
x : R
x_ne_zero : x ≠ 0
hx : ↑(algebraMap R K) x ∈ I
⊢ map h I ≠ 0
contrapose! x_ne_zero with map_eq_zero
case intro.intro
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1079360
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
K : Type u_2
K' : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Field K'
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : Algebra R K'
inst✝¹ : IsFractionRing R K'
I J : FractionalIdeal R⁰ K
h : K →ₐ[R] K'
inst✝ : Nontrivial R
hI : I ≠ 0
x : R
hx : ↑(algebraMap R K) x ∈ I
map_eq_zero : map h I = 0
⊢ ∃ x_1, x_1 ∈ I ∧ ↑h x_1 = ↑(algebraMap R K') x
case intro.intro
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1079360
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
K : Type u_2
K' : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Field K'
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : Algebra R K'
inst✝¹ : IsFractionRing R K'
I J : FractionalIdeal R⁰ K
h : K →ₐ[R] K'
inst✝ : Nontrivial R
hI : I ≠ 0
x : R
hx : ↑(algebraMap R K) x ∈ I
map_eq_zero : map h I = 0
⊢ x = 0
refine' IsFractionRing.to_map_eq_zero_iff.mp (eq_zero_iff.mp map_eq_zero _ (mem_map.mpr _))
no goals
case intro.intro
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1079360
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
K : Type u_2
K' : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Field K'
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : Algebra R K'
inst✝¹ : IsFractionRing R K'
I J : FractionalIdeal R⁰ K
h : K →ₐ[R] K'
inst✝ : Nontrivial R
hI : I ≠ 0
x : R
hx : ↑(algebraMap R K) x ∈ I
map_eq_zero : map h I = 0
⊢ ∃ x_1, x_1 ∈ I ∧ ↑h x_1 = ↑(algebraMap R K') x
exact ⟨algebraMap R K x, hx, h.commutes x⟩