∀ (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop),
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) →
    (∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (s : Set R),
        Ideal.span s = ⊤ →
          (∀ r ∈ s, P (algebraMap (Localization.Away r) (TensorProduct R (Localization.Away r) S))) →
            P (algebraMap R S)) →
      RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => P