case intro.intro
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1050336
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
K : Type u_2
K' : Type ?u.1050800
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
y : K
y_mem : y ∈ ?m.1074732
y_not_mem : ¬y ∈ ?m.1074731
⊢ ∃ x x_1, ↑(algebraMap R K) x ∈ I
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1050336
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
K : Type u_2
K' : Type ?u.1050800
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 x_1, ↑(algebraMap R K) x ∈ I
obtain ⟨y : K, y_mem, y_not_mem⟩ :=
  SetLike.exists_of_lt (by simpa only using bot_lt_iff_ne_bot.mpr hI)
case intro.intro
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1050336
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
K : Type u_2
K' : Type ?u.1050800
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
y : K
y_mem : y ∈ I
y_not_mem : ¬y ∈ ⊥
y_ne_zero : y ≠ 0
⊢ ∃ x x_1, ↑(algebraMap R K) x ∈ I
case intro.intro
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1050336
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
K : Type u_2
K' : Type ?u.1050800
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
y : K
y_mem : y ∈ ?m.1074732
y_not_mem : ¬y ∈ ?m.1074731
⊢ ∃ x x_1, ↑(algebraMap R K) x ∈ I
have y_ne_zero : y ≠ 0 := by simpa using y_not_mem
case intro.intro.intro.intro
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1050336
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
K : Type u_2
K' : Type ?u.1050800
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
y : K
y_mem : y ∈ I
y_not_mem : ¬y ∈ ⊥
y_ne_zero : y ≠ 0
z : { x // x ∈ R⁰ }
x : R
hx : ↑(algebraMap R K) x = ↑z • y
⊢ ∃ x x_1, ↑(algebraMap R K) x ∈ I
case intro.intro
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1050336
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
K : Type u_2
K' : Type ?u.1050800
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
y : K
y_mem : y ∈ I
y_not_mem : ¬y ∈ ⊥
y_ne_zero : y ≠ 0
⊢ ∃ x x_1, ↑(algebraMap R K) x ∈ I
obtain ⟨z, ⟨x, hx⟩⟩ := exists_integer_multiple R⁰ y
case intro.intro.intro.intro.refine'_1
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1050336
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
K : Type u_2
K' : Type ?u.1050800
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
y : K
y_mem : y ∈ I
y_not_mem : ¬y ∈ ⊥
y_ne_zero : y ≠ 0
z : { x // x ∈ R⁰ }
x : R
hx : ↑(algebraMap R K) x = ↑z • y
⊢ x ≠ 0

case intro.intro.intro.intro.refine'_2
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1050336
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
K : Type u_2
K' : Type ?u.1050800
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
y : K
y_mem : y ∈ I
y_not_mem : ¬y ∈ ⊥
y_ne_zero : y ≠ 0
z : { x // x ∈ R⁰ }
x : R
hx : ↑(algebraMap R K) x = ↑z • y
⊢ ↑(algebraMap R K) x ∈ I
case intro.intro.intro.intro
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1050336
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
K : Type u_2
K' : Type ?u.1050800
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
y : K
y_mem : y ∈ I
y_not_mem : ¬y ∈ ⊥
y_ne_zero : y ≠ 0
z : { x // x ∈ R⁰ }
x : R
hx : ↑(algebraMap R K) x = ↑z • y
⊢ ∃ x x_1, ↑(algebraMap R K) x ∈ I
refine' ⟨x, _, _⟩
no goals
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1050336
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
K : Type u_2
K' : Type ?u.1050800
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
⊢ ?m.1074731 < ?m.1074732
simpa only using bot_lt_iff_ne_bot.mpr hI
no goals
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1050336
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
K : Type u_2
K' : Type ?u.1050800
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
y : K
y_mem : y ∈ I
y_not_mem : ¬y ∈ ⊥
⊢ y ≠ 0
simpa using y_not_mem
case intro.intro.intro.intro.refine'_1
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1050336
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
K : Type u_2
K' : Type ?u.1050800
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
y : K
y_mem : y ∈ I
y_not_mem : ¬y ∈ ⊥
y_ne_zero : y ≠ 0
z : { x // x ∈ R⁰ }
x : R
hx : ↑(algebraMap R K) x = ↑z • y
⊢ ¬↑(algebraMap R K) ↑z * y = 0
case intro.intro.intro.intro.refine'_1
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1050336
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
K : Type u_2
K' : Type ?u.1050800
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
y : K
y_mem : y ∈ I
y_not_mem : ¬y ∈ ⊥
y_ne_zero : y ≠ 0
z : { x // x ∈ R⁰ }
x : R
hx : ↑(algebraMap R K) x = ↑z • y
⊢ x ≠ 0
rw [Ne.def, ← @IsFractionRing.to_map_eq_zero_iff R _ K, hx, Algebra.smul_def]
no goals
case intro.intro.intro.intro.refine'_1
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1050336
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
K : Type u_2
K' : Type ?u.1050800
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
y : K
y_mem : y ∈ I
y_not_mem : ¬y ∈ ⊥
y_ne_zero : y ≠ 0
z : { x // x ∈ R⁰ }
x : R
hx : ↑(algebraMap R K) x = ↑z • y
⊢ ¬↑(algebraMap R K) ↑z * y = 0
exact mul_ne_zero (IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors z.2) y_ne_zero
case intro.intro.intro.intro.refine'_2
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1050336
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
K : Type u_2
K' : Type ?u.1050800
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
y : K
y_mem : y ∈ I
y_not_mem : ¬y ∈ ⊥
y_ne_zero : y ≠ 0
z : { x // x ∈ R⁰ }
x : R
hx : ↑(algebraMap R K) x = ↑z • y
⊢ ↑z • y ∈ I
case intro.intro.intro.intro.refine'_2
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1050336
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
K : Type u_2
K' : Type ?u.1050800
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
y : K
y_mem : y ∈ I
y_not_mem : ¬y ∈ ⊥
y_ne_zero : y ≠ 0
z : { x // x ∈ R⁰ }
x : R
hx : ↑(algebraMap R K) x = ↑z • y
⊢ ↑(algebraMap R K) x ∈ I
rw [hx]
no goals
case intro.intro.intro.intro.refine'_2
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1050336
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
K : Type u_2
K' : Type ?u.1050800
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
y : K
y_mem : y ∈ I
y_not_mem : ¬y ∈ ⊥
y_ne_zero : y ≠ 0
z : { x // x ∈ R⁰ }
x : R
hx : ↑(algebraMap R K) x = ↑z • y
⊢ ↑z • y ∈ I
exact smul_mem _ _ y_mem