no goals
R : Type ?u.1518060
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1518267
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
inst✝ : IsFractionRing R₁ K
I J : Ideal R₁
z : K
⊢ spanSingleton R₁⁰ z * ↑I = ↑J ↔ Ideal.span {(sec R₁⁰ z).fst} * I = Ideal.span {↑(sec R₁⁰ z).snd} * J
erw [← mk'_mul_coeIdeal_eq_coeIdeal K (IsLocalization.sec R₁⁰ z).2.prop,
  IsLocalization.mk'_sec K z]