∀ (A : Type u_3) {K : Type u_4} {L : Type u_2} [inst : CommRing A] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] (R₂ : Type u_1) [inst_4 : CommRing R₂] [inst_5 : Algebra A R₂] [Module.Finite A R₂]
  {F₂ : IntermediateField K L} [inst_7 : Algebra R₂ ↥F₂] [IsDomain A] [IsDedekindDomain R₂] [IsFractionRing R₂ ↥F₂],
  Module.Free A R₂ → IsLocalization (Algebra.algebraMapSubmonoid R₂ (nonZeroDivisors A)) ↥F₂