no goals
R : Type ?u.1277042
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1277249
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
ι : Type u_1
s : Finset ι
f : ι → K
⊢ spanFinset R₁ s f = 0 ↔ ∀ (j : ι), j ∈ s → f j = 0
simp only [← coeToSubmodule_inj, spanFinset_coe, coe_zero, Submodule.span_eq_bot,
  Set.mem_image, Finset.mem_coe, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]