-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Presheaf.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
this : (CostructuredArrow.mkPrecomp (unop t).hom f.unop.left).op = f ≫ eqToHom ⋯
⊢ Eq (α :=
    (fun (X : Type v) ↦ X)
      (F.obj
        (op
          (CostructuredArrow.mk (Y := unop (op (unop s).left))
            (YonedaCollection.fst
              (OverArrows.val
                (counitForward F (unop s)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                      (a : (fun (X : Type v) ↦ X) (F.obj t)) → (fun (X : Type v) ↦ X) (F.obj s))
                    x))))))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (eqToHom ⋯)) :
          (a :
              (fun (X : Type v) ↦ X)
                (F.obj
                  (op
                    (CostructuredArrow.mk
                      (YonedaCollection.fst ((counitForward F (unop t) x).map₂ f.unop.left ⋯).val))))) →
            (fun (X : Type v) ↦ X)
              (F.obj
                (op
                  (CostructuredArrow.mk
                    (YonedaCollection.fst
                      (counitForward F (unop s)
                          ((ConcreteCategory.hom (F.map f) :
                              (a : (fun (X : Type v) ↦ X) (F.obj t)) → (fun (X : Type v) ↦ X) (F.obj s))
                            x)).val)))))
        (YonedaCollection.snd ((counitForward F (unop t) x).map₂ f.unop.left ⋯).val) :
      (fun (X : Type v) ↦ X)
        (F.obj
          (op
            (CostructuredArrow.mk (Y := unop (op (unop s).left))
              (YonedaCollection.fst
                (OverArrows.val
                  (counitForward F (unop s)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                        (a : (fun (X : Type v) ↦ X) (F.obj t)) → (fun (X : Type v) ↦ X) (F.obj s))
                      x))))))))
    (YonedaCollection.snd
        (OverArrows.val
          (counitForward F (unop s)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                (a : (fun (X : Type v) ↦ X) (F.obj t)) → (fun (X : Type v) ↦ X) (F.obj s))
              x))) :
      F.obj
        (op
          (CostructuredArrow.mk (Y := unop (op (unop s).left))
            (YonedaCollection.fst
              (OverArrows.val
                (counitForward F (unop s)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                      (a : (fun (X : Type v) ↦ X) (F.obj t)) → (fun (X : Type v) ↦ X) (F.obj s))
                    x)))))))
have this₁ : Eq (α :=
  (fun (X : Type v) ↦ X)
    (F.obj
      (op
        (CostructuredArrow.mk
          (Functor.map yoneda f.unop.left ≫ YonedaCollection.fst (counitForward F (unop t) x).val)))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (F.map (CostructuredArrow.mkPrecomp (YonedaCollection.fst (counitForward F (unop t) x).val) f.unop.left).op) :
        (a :
            (fun (X : Type v) ↦ X)
              (F.obj (op (CostructuredArrow.mk (YonedaCollection.fst (counitForward F (unop t) x).val))))) →
          (fun (X : Type v) ↦ X)
            (F.obj
              (op
                (CostructuredArrow.mk
                  (yoneda.map f.unop.left ≫ YonedaCollection.fst (counitForward F (unop t) x).val)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (eqToHom sorry)) :
            (a : (fun (X : Type v) ↦ X) (F.obj t)) →
              (fun (X : Type v) ↦ X)
                (F.obj (op (CostructuredArrow.mk (YonedaCollection.fst (counitForward F (unop t) x).val)))))
          x :
        (fun (X : Type v) ↦ X)
          (F.obj (op (CostructuredArrow.mk (YonedaCollection.fst (counitForward F (unop t) x).val))))) :
    (fun (X : Type v) ↦ X)
      (F.obj
        (op
          (CostructuredArrow.mk
            (Functor.map yoneda f.unop.left ≫ YonedaCollection.fst (counitForward F (unop t) x).val)))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (eqToHom sorry)) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk (yoneda.map f.unop.left ≫ t.1.hom))))) →
          (fun (X : Type v) ↦ X)
            (F.obj
              (op
                (CostructuredArrow.mk
                  (yoneda.map f.unop.left ≫ YonedaCollection.fst (counitForward F (unop t) x).val)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (F.map (Quiver.Hom.op (CostructuredArrow.mkPrecomp (Comma.hom t.1) f.unop.left))) :
            (a : (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk t.1.hom)))) →
              (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk (yoneda.map f.unop.left ≫ t.1.hom)))))
          x :
        (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk (Functor.map yoneda f.unop.left ≫ Comma.hom t.1))))) :
    (fun (X : Type v) ↦ X)
      (F.obj
        (op
          (CostructuredArrow.mk
            (Functor.map yoneda f.unop.left ≫ YonedaCollection.fst (counitForward F (unop t) x).val)))))
Tactic: have : F.map (CostructuredArrow.mkPrecomp
      (YonedaCollection.fst (counitForward F (unop t) x).val) f.unop.left).op
      (F.map (eqToHom (by simp; rfl)) x) = _ :=
    map_mkPrecomp_eqToHom (h := by simp)