Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type (max w v)
X✝ Y✝ : F.Elementsᵒᵖ
f : X✝ ⟶ Y✝
⊢ ((𝟭 F.Elementsᵒᵖ).map f ≫
        (isoMk
              (F.elementsMk
                (op
                  ({ obj := fun x ↦ CostructuredArrow.mk (uliftYonedaEquiv.symm (unop x).snd),
                          map := fun {X Y} f ↦ CostructuredArrow.homMk (↑(unop f)).unop ⋯, map_id := ⋯,
                          map_comp := ⋯ }.obj
                      Y✝).left)
                (uliftYonedaEquiv
                  ({ obj := fun x ↦ CostructuredArrow.mk (uliftYonedaEquiv.symm (unop x).snd),
                          map := fun {X Y} f ↦ CostructuredArrow.homMk (↑(unop f)).unop ⋯, map_id := ⋯,
                          map_comp := ⋯ }.obj
                      Y✝).hom))
              (unop Y✝)
              (Iso.refl
                (F.elementsMk
                    (op
                      ({ obj := fun x ↦ CostructuredArrow.mk (uliftYonedaEquiv.symm (unop x).snd),
                              map := fun {X Y} f ↦ CostructuredArrow.homMk (↑(unop f)).unop ⋯, map_id := ⋯,
                              map_comp := ⋯ }.obj
                          Y✝).left)
                    (uliftYonedaEquiv
                      ({ obj := fun x ↦ CostructuredArrow.mk (uliftYonedaEquiv.symm (unop x).snd),
                              map := fun {X Y} f ↦ CostructuredArrow.homMk (↑(unop f)).unop ⋯, map_id := ⋯,
                              map_comp := ⋯ }.obj
                          Y✝).hom)).fst)
              ⋯).op.hom).unop =
    ((isoMk
              (F.elementsMk
                (op
                  ({ obj := fun x ↦ CostructuredArrow.mk (uliftYonedaEquiv.symm (unop x).snd),
                          map := fun {X Y} f ↦ CostructuredArrow.homMk (↑(unop f)).unop ⋯, map_id := ⋯,
                          map_comp := ⋯ }.obj
                      X✝).left)
                (uliftYonedaEquiv
                  ({ obj := fun x ↦ CostructuredArrow.mk (uliftYonedaEquiv.symm (unop x).snd),
                          map := fun {X Y} f ↦ CostructuredArrow.homMk (↑(unop f)).unop ⋯, map_id := ⋯,
                          map_comp := ⋯ }.obj
                      X✝).hom))
              (unop X✝)
              (Iso.refl
                (F.elementsMk
                    (op
                      ({ obj := fun x ↦ CostructuredArrow.mk (uliftYonedaEquiv.symm (unop x).snd),
                              map := fun {X Y} f ↦ CostructuredArrow.homMk (↑(unop f)).unop ⋯, map_id := ⋯,
                              map_comp := ⋯ }.obj
                          X✝).left)
                    (uliftYonedaEquiv
                      ({ obj := fun x ↦ CostructuredArrow.mk (uliftYonedaEquiv.symm (unop x).snd),
                              map := fun {X Y} f ↦ CostructuredArrow.homMk (↑(unop f)).unop ⋯, map_id := ⋯,
                              map_comp := ⋯ }.obj
                          X✝).hom)).fst)
              ⋯).op.hom ≫
        ({ obj := fun x ↦ CostructuredArrow.mk (uliftYonedaEquiv.symm (unop x).snd),
                map := fun {X Y} f ↦ CostructuredArrow.homMk (↑(unop f)).unop ⋯, map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun X ↦ op (F.elementsMk (op X.left) (uliftYonedaEquiv X.hom)),
                map := fun {X Y} f ↦
                  (homMk (F.elementsMk (op Y.left) (uliftYonedaEquiv Y.hom))
                      (F.elementsMk (op X.left) (uliftYonedaEquiv X.hom)) f.left.op ⋯).op,
                map_id := ⋯, map_comp := ⋯ }).map
          f).unop

Tactic:
aesop

Goal state after: