∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (D : Type u_2)
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D],
  CategoryTheory.Equivalence.symmEquivInverse C D =
    { obj := fun e => Opposite.op e.symm,
        map := fun {e f} α =>
          (CategoryTheory.Equivalence.mkHom
              ((CategoryTheory.conjugateEquiv e.symm.toAdjunction f.symm.toAdjunction).invFun
                (CategoryTheory.Equivalence.asNatTrans α))).op,
        map_id := ⋯, map_comp := ⋯ }.leftOp