∀ {R : Type u_2} (K : Type u_1) [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDomain R],
  Subgroup.map
      (Units.mapEquiv (FractionalIdeal.canonicalEquiv (nonZeroDivisors R) (FractionRing R) K).toMulEquiv).toMonoidHom
      (toPrincipalIdeal R (FractionRing R)).range =
    (toPrincipalIdeal R K).range