-- 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)
T : Over A
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ {X Y : (CostructuredArrow yoneda A)ᵒᵖ} (f : X ⟶ Y),
    Eq (α :=
      Functor.obj (Functor.op (toOver yoneda A) ⋙ Functor.obj yoneda T) X ⟶
        (Functor.op yoneda ⋙ Functor.obj yoneda ((overEquivPresheafCostructuredArrow A).functor.obj T)).obj Y)
      (Functor.map (Functor.op (toOver yoneda A) ⋙ Functor.obj yoneda T) f ≫
        Iso.hom
          ((fun (X : (CostructuredArrow yoneda A)ᵒᵖ) ↦
              (Equiv.toIso (overEquivPresheafCostructuredArrow A).fullyFaithfulFunctor.homEquiv ≪≫
                  Equiv.toIso
                    (Iso.homCongr ((toOverCompOverEquivPresheafCostructuredArrow A).app (unop X))
                      (Iso.refl ((overEquivPresheafCostructuredArrow A).functor.obj T))) :
                Functor.obj (Functor.op (toOver yoneda A) ⋙ Functor.obj yoneda T) X ≅
                  (Functor.op yoneda ⋙ Functor.obj yoneda ((overEquivPresheafCostructuredArrow A).functor.obj T)).obj
                    X))
            Y))
      (Iso.hom
          ((fun (X : (CostructuredArrow yoneda A)ᵒᵖ) ↦
              (Equiv.toIso (overEquivPresheafCostructuredArrow A).fullyFaithfulFunctor.homEquiv ≪≫
                  Equiv.toIso
                    (Iso.homCongr ((toOverCompOverEquivPresheafCostructuredArrow A).app (unop X))
                      (Iso.refl ((overEquivPresheafCostructuredArrow A).functor.obj T))) :
                Functor.obj (Functor.op (toOver yoneda A) ⋙ Functor.obj yoneda T) X ≅
                  (Functor.op yoneda ⋙ Functor.obj yoneda ((overEquivPresheafCostructuredArrow A).functor.obj T)).obj
                    X))
            X) ≫
        (Functor.op yoneda ⋙ Functor.obj yoneda ((overEquivPresheafCostructuredArrow A).functor.obj T)).map f)
⊢ ∀ {X Y : (CostructuredArrow yoneda A)ᵒᵖ} (f : X ⟶ Y),
    Eq (α :=
      Functor.obj (Functor.op (toOver yoneda A) ⋙ Functor.obj yoneda T) X ⟶
        (Functor.op yoneda ⋙ Functor.obj yoneda ((overEquivPresheafCostructuredArrow A).functor.obj T)).obj Y)
      (Functor.map (Functor.op (toOver yoneda A) ⋙ Functor.obj yoneda T) f ≫
        Iso.hom
          ((fun (X : (CostructuredArrow yoneda A)ᵒᵖ) ↦
              (Equiv.toIso (overEquivPresheafCostructuredArrow A).fullyFaithfulFunctor.homEquiv ≪≫
                  Equiv.toIso
                    (Iso.homCongr ((toOverCompOverEquivPresheafCostructuredArrow A).app (unop X))
                      (Iso.refl ((overEquivPresheafCostructuredArrow A).functor.obj T))) :
                Functor.obj (Functor.op (toOver yoneda A) ⋙ Functor.obj yoneda T) X ≅
                  (Functor.op yoneda ⋙ Functor.obj yoneda ((overEquivPresheafCostructuredArrow A).functor.obj T)).obj
                    X))
            Y))
      (Iso.hom
          ((fun (X : (CostructuredArrow yoneda A)ᵒᵖ) ↦
              (Equiv.toIso (overEquivPresheafCostructuredArrow A).fullyFaithfulFunctor.homEquiv ≪≫
                  Equiv.toIso
                    (Iso.homCongr ((toOverCompOverEquivPresheafCostructuredArrow A).app (unop X))
                      (Iso.refl ((overEquivPresheafCostructuredArrow A).functor.obj T))) :
                Functor.obj (Functor.op (toOver yoneda A) ⋙ Functor.obj yoneda T) X ≅
                  (Functor.op yoneda ⋙ Functor.obj yoneda ((overEquivPresheafCostructuredArrow A).functor.obj T)).obj
                    X))
            X) ≫
        (Functor.op yoneda ⋙ Functor.obj yoneda ((overEquivPresheafCostructuredArrow A).functor.obj T)).map f)

Tactic:
cat_disch