R : Type ?u.1217298
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1217505
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I✝ J I : FractionalIdeal R₁⁰ K
⊢ { val := ↑I / ↑1, property := (_ : IsFractional R₁⁰ (↑I / ↑1)) } = I
R : Type ?u.1217298
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1217505
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I✝ J I : FractionalIdeal R₁⁰ K
⊢ I / 1 = I
rw [div_nonzero (one_ne_zero' (FractionalIdeal R₁⁰ K))]
case a
R : Type ?u.1217298
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1217505
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I✝ J I : FractionalIdeal R₁⁰ K
x✝ : K
⊢ x✝ ∈ { val := ↑I / ↑1, property := (_ : IsFractional R₁⁰ (↑I / ↑1)) } ↔ x✝ ∈ I
R : Type ?u.1217298
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1217505
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I✝ J I : FractionalIdeal R₁⁰ K
⊢ { val := ↑I / ↑1, property := (_ : IsFractional R₁⁰ (↑I / ↑1)) } = I
ext
case a.mp
R : Type ?u.1217298
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1217505
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I✝ J I : FractionalIdeal R₁⁰ K
x✝ : K
h : x✝ ∈ { val := ↑I / ↑1, property := (_ : IsFractional R₁⁰ (↑I / ↑1)) }
⊢ x✝ ∈ I

case a.mpr
R : Type ?u.1217298
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1217505
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I✝ J I : FractionalIdeal R₁⁰ K
x✝ : K
h : x✝ ∈ I
⊢ x✝ ∈ { val := ↑I / ↑1, property := (_ : IsFractional R₁⁰ (↑I / ↑1)) }
case a
R : Type ?u.1217298
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1217505
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I✝ J I : FractionalIdeal R₁⁰ K
x✝ : K
⊢ x✝ ∈ { val := ↑I / ↑1, property := (_ : IsFractional R₁⁰ (↑I / ↑1)) } ↔ x✝ ∈ I
constructor <;> intro h
no goals
case a.mp
R : Type ?u.1217298
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1217505
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I✝ J I : FractionalIdeal R₁⁰ K
x✝ : K
h : x✝ ∈ { val := ↑I / ↑1, property := (_ : IsFractional R₁⁰ (↑I / ↑1)) }
⊢ x✝ ∈ I
simpa using mem_div_iff_forall_mul_mem.mp h 1 ((algebraMap R₁ K).map_one ▸ coe_mem_one R₁⁰ 1)
case a.mpr
R : Type ?u.1217298
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1217505
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I✝ J I : FractionalIdeal R₁⁰ K
x✝ : K
h : x✝ ∈ I
⊢ ∀ (y : K), y ∈ ↑1 → x✝ * y ∈ ↑I
case a.mpr
R : Type ?u.1217298
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1217505
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I✝ J I : FractionalIdeal R₁⁰ K
x✝ : K
h : x✝ ∈ I
⊢ x✝ ∈ { val := ↑I / ↑1, property := (_ : IsFractional R₁⁰ (↑I / ↑1)) }
apply mem_div_iff_forall_mul_mem.mpr
case a.mpr.intro.intro
R : Type ?u.1217298
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1217505
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I✝ J I : FractionalIdeal R₁⁰ K
x✝ : K
h : x✝ ∈ I
y' : R₁
left✝ : y' ∈ ↑⊤
⊢ x✝ * ↑(Algebra.linearMap R₁ K) y' ∈ ↑I
case a.mpr
R : Type ?u.1217298
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1217505
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I✝ J I : FractionalIdeal R₁⁰ K
x✝ : K
h : x✝ ∈ I
⊢ ∀ (y : K), y ∈ ↑1 → x✝ * y ∈ ↑I
rintro y ⟨y', _, rfl⟩
case a.mpr.intro.intro
R : Type ?u.1217298
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1217505
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I✝ J I : FractionalIdeal R₁⁰ K
x✝ : K
h : x✝ ∈ I
y' : R₁
left✝ : y' ∈ ↑⊤
⊢ y' • x✝ ∈ ↑I
case a.mpr.intro.intro
R : Type ?u.1217298
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1217505
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I✝ J I : FractionalIdeal R₁⁰ K
x✝ : K
h : x✝ ∈ I
y' : R₁
left✝ : y' ∈ ↑⊤
⊢ x✝ * ↑(Algebra.linearMap R₁ K) y' ∈ ↑I
rw [mul_comm, Algebra.linearMap_apply, ← Algebra.smul_def]
no goals
case a.mpr.intro.intro
R : Type ?u.1217298
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1217505
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I✝ J I : FractionalIdeal R₁⁰ K
x✝ : K
h : x✝ ∈ I
y' : R₁
left✝ : y' ∈ ↑⊤
⊢ y' • x✝ ∈ ↑I
exact Submodule.smul_mem _ y' h