-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A_1 A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ {X Y : (CostructuredArrow yoneda A)ᵒᵖ} (f : X ⟶ Y),
    Eq (α :=
      Functor.obj (Functor.op (toOver yoneda A) ⋙ coyoneda) X ⟶
        (Functor.op yoneda ⋙
              coyoneda ⋙
                Functor.obj (Functor.whiskeringLeft (Over A) ((CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v) (Type (max u v)))
                  (overEquivPresheafCostructuredArrow A).functor).obj
          Y)
      (Functor.map (Functor.op (toOver yoneda A) ⋙ coyoneda) f ≫
        Iso.hom
          ((fun (X : (CostructuredArrow yoneda A)ᵒᵖ) ↦
              NatIso.ofComponents
                (fun (Y : Over A) ↦
                  Equiv.toIso (overEquivPresheafCostructuredArrow A).fullyFaithfulFunctor.homEquiv ≪≫
                    Equiv.toIso
                      (Iso.homCongr ((toOverCompOverEquivPresheafCostructuredArrow A).app (unop X))
                        (Iso.refl ((overEquivPresheafCostructuredArrow A).functor.obj Y))))
                ⋯)
            Y))
      (Iso.hom
          ((fun (X : (CostructuredArrow yoneda A)ᵒᵖ) ↦
              NatIso.ofComponents
                (fun (Y : Over A) ↦
                  Equiv.toIso (overEquivPresheafCostructuredArrow A).fullyFaithfulFunctor.homEquiv ≪≫
                    Equiv.toIso
                      (Iso.homCongr ((toOverCompOverEquivPresheafCostructuredArrow A).app (unop X))
                        (Iso.refl ((overEquivPresheafCostructuredArrow A).functor.obj Y))))
                ⋯)
            X) ≫
        (Functor.op yoneda ⋙
              coyoneda ⋙
                Functor.obj (Functor.whiskeringLeft (Over A) ((CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v) (Type (max u v)))
                  (overEquivPresheafCostructuredArrow A).functor).map
          f)
⊢ ∀ {X Y : (CostructuredArrow yoneda A)ᵒᵖ} (f : X ⟶ Y),
    Eq (α :=
      Functor.obj (Functor.op (toOver yoneda A) ⋙ coyoneda) X ⟶
        (Functor.op yoneda ⋙
              coyoneda ⋙
                Functor.obj (Functor.whiskeringLeft (Over A) ((CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v) (Type (max u v)))
                  (overEquivPresheafCostructuredArrow A).functor).obj
          Y)
      (Functor.map (Functor.op (toOver yoneda A) ⋙ coyoneda) f ≫
        Iso.hom
          ((fun (X : (CostructuredArrow yoneda A)ᵒᵖ) ↦
              NatIso.ofComponents
                (fun (Y : Over A) ↦
                  Equiv.toIso (overEquivPresheafCostructuredArrow A).fullyFaithfulFunctor.homEquiv ≪≫
                    Equiv.toIso
                      (Iso.homCongr ((toOverCompOverEquivPresheafCostructuredArrow A).app (unop X))
                        (Iso.refl ((overEquivPresheafCostructuredArrow A).functor.obj Y))))
                ⋯)
            Y))
      (Iso.hom
          ((fun (X : (CostructuredArrow yoneda A)ᵒᵖ) ↦
              NatIso.ofComponents
                (fun (Y : Over A) ↦
                  Equiv.toIso (overEquivPresheafCostructuredArrow A).fullyFaithfulFunctor.homEquiv ≪≫
                    Equiv.toIso
                      (Iso.homCongr ((toOverCompOverEquivPresheafCostructuredArrow A).app (unop X))
                        (Iso.refl ((overEquivPresheafCostructuredArrow A).functor.obj Y))))
                ⋯)
            X) ≫
        (Functor.op yoneda ⋙
              coyoneda ⋙
                Functor.obj (Functor.whiskeringLeft (Over A) ((CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v) (Type (max u v)))
                  (overEquivPresheafCostructuredArrow A).functor).map
          f)

Tactic:
cat_disch