R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.21895
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
a : S
⊢ ∃ b, IsInteger R (a * ↑(algebraMap R S) ↑b)
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.21895
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
a : S
⊢ ∃ b, IsInteger R (↑b • a)
simp_rw [Algebra.smul_def, mul_comm _ a]
no goals
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.21895
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
a : S
⊢ ∃ b, IsInteger R (a * ↑(algebraMap R S) ↑b)
apply exists_integer_multiple'