∀ (R₁ : Type u_3) [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K]
  [inst_3 : IsFractionRing R₁ K] {ι : Type u_5} (s : Finset ι) (f : ι → K),
  ↑(FractionalIdeal.spanFinset R₁ s f) = Submodule.span R₁ (f '' ↑s)