R : Type ?u.1255271
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1255478
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1255939
K : Type u_1
L : Type u_2
inst✝⁶ : CommRing R₁
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra R₁ K
inst✝² : IsFractionRing R₁ K
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
⊢ ¬I = 0 → I = 1
R : Type ?u.1255271
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1255478
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1255939
K : Type u_1
L : Type u_2
inst✝⁶ : CommRing R₁
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra R₁ K
inst✝² : IsFractionRing R₁ K
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
⊢ I = 0 ∨ I = 1
rw [or_iff_not_imp_left]
R : Type ?u.1255271
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1255478
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1255939
K : Type u_1
L : Type u_2
inst✝⁶ : CommRing R₁
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra R₁ K
inst✝² : IsFractionRing R₁ K
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
⊢ I = 1
R : Type ?u.1255271
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1255478
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1255939
K : Type u_1
L : Type u_2
inst✝⁶ : CommRing R₁
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra R₁ K
inst✝² : IsFractionRing R₁ K
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
⊢ ¬I = 0 → I = 1
intro hI
R : Type ?u.1255271
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1255478
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1255939
K : Type u_1
L : Type u_2
inst✝⁶ : CommRing R₁
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra R₁ K
inst✝² : IsFractionRing R₁ K
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
⊢ ∀ (x : L), x ∈ I ↔ ∃ x', ↑(algebraMap K L) x' = x
R : Type ?u.1255271
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1255478
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1255939
K : Type u_1
L : Type u_2
inst✝⁶ : CommRing R₁
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra R₁ K
inst✝² : IsFractionRing R₁ K
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
⊢ I = 1
simp_rw [@SetLike.ext_iff _ _ _ I 1, mem_one_iff]
R : Type ?u.1255271
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1255478
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1255939
K : Type u_1
L : Type u_2
inst✝⁶ : CommRing R₁
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra R₁ K
inst✝² : IsFractionRing R₁ K
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
x : L
⊢ x ∈ I ↔ ∃ x', ↑(algebraMap K L) x' = x
R : Type ?u.1255271
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1255478
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1255939
K : Type u_1
L : Type u_2
inst✝⁶ : CommRing R₁
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra R₁ K
inst✝² : IsFractionRing R₁ K
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
⊢ ∀ (x : L), x ∈ I ↔ ∃ x', ↑(algebraMap K L) x' = x
intro x
case mp
R : Type ?u.1255271
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1255478
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1255939
K : Type u_1
L : Type u_2
inst✝⁶ : CommRing R₁
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra R₁ K
inst✝² : IsFractionRing R₁ K
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
x : L
⊢ x ∈ I → ∃ x', ↑(algebraMap K L) x' = x

case mpr
R : Type ?u.1255271
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1255478
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1255939
K : Type u_1
L : Type u_2
inst✝⁶ : CommRing R₁
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra R₁ K
inst✝² : IsFractionRing R₁ K
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
x : L
⊢ (∃ x', ↑(algebraMap K L) x' = x) → x ∈ I
R : Type ?u.1255271
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1255478
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1255939
K : Type u_1
L : Type u_2
inst✝⁶ : CommRing R₁
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra R₁ K
inst✝² : IsFractionRing R₁ K
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
x : L
⊢ x ∈ I ↔ ∃ x', ↑(algebraMap K L) x' = x
constructor
case mp
R : Type ?u.1255271
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1255478
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1255939
K : Type u_1
L : Type u_2
inst✝⁶ : CommRing R₁
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra R₁ K
inst✝² : IsFractionRing R₁ K
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
x : L
x_mem : x ∈ I
⊢ ∃ x', ↑(algebraMap K L) x' = x
case mp
R : Type ?u.1255271
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1255478
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1255939
K : Type u_1
L : Type u_2
inst✝⁶ : CommRing R₁
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra R₁ K
inst✝² : IsFractionRing R₁ K
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
x : L
⊢ x ∈ I → ∃ x', ↑(algebraMap K L) x' = x
intro x_mem
case mp.intro.intro
R : Type ?u.1255271
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1255478
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1255939
K : Type u_1
L : Type u_2
inst✝⁶ : CommRing R₁
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra R₁ K
inst✝² : IsFractionRing R₁ K
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
n : K
d : { x // x ∈ K⁰ }
x_mem : mk' L n d ∈ I
⊢ ∃ x', ↑(algebraMap K L) x' = mk' L n d
case mp
R : Type ?u.1255271
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1255478
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1255939
K : Type u_1
L : Type u_2
inst✝⁶ : CommRing R₁
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra R₁ K
inst✝² : IsFractionRing R₁ K
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
x : L
x_mem : x ∈ I
⊢ ∃ x', ↑(algebraMap K L) x' = x
obtain ⟨n, d, rfl⟩ := IsLocalization.mk'_surjective K⁰ x
case mp.intro.intro
R : Type ?u.1255271
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1255478
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1255939
K : Type u_1
L : Type u_2
inst✝⁶ : CommRing R₁
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra R₁ K
inst✝² : IsFractionRing R₁ K
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
n : K
d : { x // x ∈ K⁰ }
x_mem : mk' L n d ∈ I
⊢ ↑(algebraMap K L) (n / ↑d) = mk' L n d
case mp.intro.intro
R : Type ?u.1255271
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1255478
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1255939
K : Type u_1
L : Type u_2
inst✝⁶ : CommRing R₁
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra R₁ K
inst✝² : IsFractionRing R₁ K
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
n : K
d : { x // x ∈ K⁰ }
x_mem : mk' L n d ∈ I
⊢ ∃ x', ↑(algebraMap K L) x' = mk' L n d
refine' ⟨n / d, _⟩
no goals
case mp.intro.intro
R : Type ?u.1255271
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1255478
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1255939
K : Type u_1
L : Type u_2
inst✝⁶ : CommRing R₁
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra R₁ K
inst✝² : IsFractionRing R₁ K
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
n : K
d : { x // x ∈ K⁰ }
x_mem : mk' L n d ∈ I
⊢ ↑(algebraMap K L) (n / ↑d) = mk' L n d
rw [map_div₀, IsFractionRing.mk'_eq_div]
case mpr.intro
R : Type ?u.1255271
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1255478
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1255939
K : Type u_1
L : Type u_2
inst✝⁶ : CommRing R₁
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra R₁ K
inst✝² : IsFractionRing R₁ K
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
x : K
⊢ ↑(algebraMap K L) x ∈ I
case mpr
R : Type ?u.1255271
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1255478
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1255939
K : Type u_1
L : Type u_2
inst✝⁶ : CommRing R₁
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra R₁ K
inst✝² : IsFractionRing R₁ K
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
x : L
⊢ (∃ x', ↑(algebraMap K L) x' = x) → x ∈ I
rintro ⟨x, rfl⟩
case mpr.intro.intro.intro
R : Type ?u.1255271
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1255478
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1255939
K : Type u_1
L : Type u_2
inst✝⁶ : CommRing R₁
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra R₁ K
inst✝² : IsFractionRing R₁ K
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
x y : K
y_ne : y ≠ 0
y_mem : ↑(algebraMap K L) y ∈ I
⊢ ↑(algebraMap K L) x ∈ I
case mpr.intro
R : Type ?u.1255271
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1255478
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1255939
K : Type u_1
L : Type u_2
inst✝⁶ : CommRing R₁
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra R₁ K
inst✝² : IsFractionRing R₁ K
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
x : K
⊢ ↑(algebraMap K L) x ∈ I
obtain ⟨y, y_ne, y_mem⟩ := exists_ne_zero_mem_isInteger hI
case mpr.intro.intro.intro
R : Type ?u.1255271
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1255478
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1255939
K : Type u_1
L : Type u_2
inst✝⁶ : CommRing R₁
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra R₁ K
inst✝² : IsFractionRing R₁ K
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
x y : K
y_ne : y ≠ 0
y_mem : ↑(algebraMap K L) y ∈ I
⊢ (x / y) • ↑(algebraMap K L) y ∈ I
case mpr.intro.intro.intro
R : Type ?u.1255271
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1255478
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1255939
K : Type u_1
L : Type u_2
inst✝⁶ : CommRing R₁
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra R₁ K
inst✝² : IsFractionRing R₁ K
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
x y : K
y_ne : y ≠ 0
y_mem : ↑(algebraMap K L) y ∈ I
⊢ ↑(algebraMap K L) x ∈ I
rw [← div_mul_cancel x y_ne, RingHom.map_mul, ← Algebra.smul_def]
no goals
case mpr.intro.intro.intro
R : Type ?u.1255271
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1255478
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1255939
K : Type u_1
L : Type u_2
inst✝⁶ : CommRing R₁
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra R₁ K
inst✝² : IsFractionRing R₁ K
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
x y : K
y_ne : y ≠ 0
y_mem : ↑(algebraMap K L) y ∈ I
⊢ (x / y) • ↑(algebraMap K L) y ∈ I
exact smul_mem (M := L) I (x / y) y_mem