no goals
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
R₁ : Type ?u.1730977
inst✝⁴ : CommRing R₁
K : Type ?u.1730983
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
x : P
I J : FractionalIdeal S P
⊢ (∀ {zI : P}, zI ∈ I → zI ∈ spanSingleton S x * J) ↔ ∀ (zI : P), zI ∈ I → ∃ zJ, zJ ∈ J ∧ x * zJ = zI
simp only [mem_singleton_mul, eq_comm]