case intro.intro
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I : Submodule R P
J : FractionalIdeal S P
hIJ : I ≤ ↑J
a : R
a_mem : a ∈ S
ha : ∀ (b : P), b ∈ ↑J → IsInteger R (a • b)
⊢ IsFractional S I
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I : Submodule R P
J : FractionalIdeal S P
hIJ : I ≤ ↑J
⊢ IsFractional S I
obtain ⟨a, a_mem, ha⟩ := J.isFractional
case intro.intro
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I : Submodule R P
J : FractionalIdeal S P
hIJ : I ≤ ↑J
a : R
a_mem : a ∈ S
ha : ∀ (b : P), b ∈ ↑J → IsInteger R (a • b)
⊢ ∀ (b : P), b ∈ I → IsInteger R (a • b)
case intro.intro
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I : Submodule R P
J : FractionalIdeal S P
hIJ : I ≤ ↑J
a : R
a_mem : a ∈ S
ha : ∀ (b : P), b ∈ ↑J → IsInteger R (a • b)
⊢ IsFractional S I
use a, a_mem
case intro.intro
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I : Submodule R P
J : FractionalIdeal S P
hIJ : I ≤ ↑J
a : R
a_mem : a ∈ S
ha : ∀ (b : P), b ∈ ↑J → IsInteger R (a • b)
b : P
b_mem : b ∈ I
⊢ IsInteger R (a • b)
case intro.intro
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I : Submodule R P
J : FractionalIdeal S P
hIJ : I ≤ ↑J
a : R
a_mem : a ∈ S
ha : ∀ (b : P), b ∈ ↑J → IsInteger R (a • b)
⊢ ∀ (b : P), b ∈ I → IsInteger R (a • b)
intro b b_mem
no goals
case intro.intro
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I : Submodule R P
J : FractionalIdeal S P
hIJ : I ≤ ↑J
a : R
a_mem : a ∈ S
ha : ∀ (b : P), b ∈ ↑J → IsInteger R (a • b)
b : P
b_mem : b ∈ I
⊢ IsInteger R (a • b)
exact ha b (hIJ b_mem)