case 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
aI : R
haI : aI ∈ S
hI : ∀ (b : P), b ∈ I → IsInteger R (aI • b)
J : Submodule R P
b : P
hb : b ∈ I ⊓ J
hbI : b ∈ I
right✝ : b ∈ J
⊢ IsInteger R (aI • b)
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
aI : R
haI : aI ∈ S
hI : ∀ (b : P), b ∈ I → IsInteger R (aI • b)
J : Submodule R P
b : P
hb : b ∈ I ⊓ J
⊢ IsInteger R (aI • b)
rcases mem_inf.mp hb with ⟨hbI, _⟩
no goals
case 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
aI : R
haI : aI ∈ S
hI : ∀ (b : P), b ∈ I → IsInteger R (aI • b)
J : Submodule R P
b : P
hb : b ∈ I ⊓ J
hbI : b ∈ I
right✝ : b ∈ J
⊢ IsInteger R (aI • b)
exact hI b hbI