∀ {G : Type u_2} [inst : CategoryTheory.Groupoid G] (r : HomRel G) {X Y : CategoryTheory.Quotient r} (f : X.as ⟶ Y.as),
  CategoryTheory.Quotient.inv r (Quot.mk (CategoryTheory.HomRel.CompClosure r) f) =
    Quot.mk (CategoryTheory.HomRel.CompClosure r) (CategoryTheory.Groupoid.inv f)