∀ (R : Type u_5) [inst : CommRing R] [inst_1 : IsDomain R] (a : CommRing.Pic R),
  (ClassGroup.equivPic R).symm a =
    (ClassGroup.mulEquivUnitsSubmoduleQuotRange R).symm
      ((QuotientGroup.congr (Submodule.unitsToPic R (FractionRing R)).ker (Units.map ↑(Submodule.spanSingleton R)).range
          (MulEquiv.refl (Submodule R (FractionRing R))ˣ) ⋯)
        ((QuotientGroup.quotientKerEquivRange (Submodule.unitsToPic R (FractionRing R))).symm
          ((MulEquiv.subgroupCongr ⋯).symm ((MulEquiv.subgroupCongr ⋯).symm (Subgroup.topEquiv.symm a)))))