-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q U : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X Y_1 : C
S : Sieve.{v₁, u₁} X
R : Presieve.{v₁, u₁} X
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
t : Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v₁, u₁} X) (shrinkFunctor.{w, v₁, u₁} S) ⟶ F
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
hf : S.arrows f
⊢ Eq (α := F.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (t.app (op Z)) :
          (a : (shrinkFunctor.{w, v₁, u₁} S).toFunctor.obj (op Z)) → F.obj (op Z))
        (Subtype.mk (p := fun (x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Z)) ↦
            Membership.mem (γ := Set (Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Z)))
              {f : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Z) |
                S.arrows (Y := Z)
                  ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Z)) → Z ⟶ X) f)}
              x)
            ((Equiv.symm shrinkYonedaObjObjEquiv : (a : Z ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Z)) (g ≫ f))
            ⋯ :
          { x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Z) //
            Membership.mem (γ := Set (Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Z)))
              {f : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Z) |
                S.arrows (Y := Z)
                  ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Z)) → Z ⟶ X) f)}
              x }) :
      F.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (t.app (op Z)) :
          (a : (shrinkFunctor.{w, v₁, u₁} S).toFunctor.obj (op Z)) → F.obj (op Z))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                ((Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v₁, u₁} X) (shrinkFunctor.{w, v₁, u₁} S)).map
                  g.op) :
              (a : (shrinkFunctor.{w, v₁, u₁} S).toFunctor.obj (op Y)) →
                (shrinkFunctor.{w, v₁, u₁} S).toFunctor.obj (op Z))
            (Subtype.mk (p := fun (x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y)) ↦
              Membership.mem (γ := Set (Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y)))
                {f : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y) |
                  S.arrows (Y := Y)
                    ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) → Y ⟶ X) f)}
                x)
              ((Equiv.symm shrinkYonedaObjObjEquiv : (a : Y ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) f) ⋯) :
          (Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v₁, u₁} X) (shrinkFunctor.{w, v₁, u₁} S)).obj
            (op Z)) :
      F.obj (op Z))
have rw! : Eq (α := F.obj (op Z))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (t.app (op Z)) :
        (a : (shrinkFunctor.{w, v₁, u₁} S).toFunctor.obj (op Z)) → F.obj (op Z))
      (Subtype.mk (p := fun (x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Z)) ↦
          Membership.mem (γ := Set (Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Z)))
            {f : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Z) |
              S.arrows (Y := Z)
                ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Z)) → Z ⟶ X) f)}
            x)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj shrinkYoneda.{w, v₁, u₁} X) g.op) :
              (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y))) →
                (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Z)))
            ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op Y) ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y))
                f :
              Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y)))
          sorry :
        { x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Z) //
          Membership.mem (γ := Set (Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Z)))
            {f : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Z) |
              S.arrows (Y := Z)
                ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Z)) → Z ⟶ X) f)}
            x }) :
    F.obj (op Z))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (t.app (op Z)) :
        (a : (shrinkFunctor.{w, v₁, u₁} S).toFunctor.obj (op Z)) → F.obj (op Z))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v₁, u₁} X) (shrinkFunctor.{w, v₁, u₁} S)).map
                g.op) :
            (a : (shrinkFunctor.{w, v₁, u₁} S).toFunctor.obj (op Y)) →
              (shrinkFunctor.{w, v₁, u₁} S).toFunctor.obj (op Z))
          (Subtype.mk (p := fun (x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y)) ↦
            Membership.mem (γ := Set (Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y)))
              {f : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y) |
                S.arrows (Y := Y)
                  ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) → Y ⟶ X) f)}
              x)
            ((Equiv.symm shrinkYonedaObjObjEquiv : (a : Y ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) f) sorry) :
        (Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v₁, u₁} X) (shrinkFunctor.{w, v₁, u₁} S)).obj (op Z)) :
    F.obj (op Z))
Tactic: rw! [shrinkYonedaObjObjEquiv_symm_comp]