-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
inst_1 : LocallySmall.{w, v, u} C
X Y : C
f : X ⟶ Y
x : Φ.fiber.obj X
rw :
  Eq (α := (fun (X : Type w) ↦ X) (Functor.obj Φ.presheafFiber (Functor.obj shrinkYoneda.{w, v, u} Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map Φ.presheafFiber (Functor.map shrinkYoneda.{w, v, u} f)) :
          (a : (fun (X : Type w) ↦ X) (Φ.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj X))) →
            (fun (X : Type w) ↦ X) (Φ.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.toPresheafFiber X x (Functor.obj shrinkYoneda.{w, v, u} X)) :
              (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj X).obj (op X))) →
                (fun (X : Type w) ↦ X) (Φ.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj X)))
            ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op X))
                (𝟙 X) :
              Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X)) :
          (fun (X : Type w) ↦ X) (Functor.obj Φ.presheafFiber (Functor.obj shrinkYoneda.{w, v, u} X))) :
      (fun (X : Type w) ↦ X) (Functor.obj Φ.presheafFiber (Functor.obj shrinkYoneda.{w, v, u} Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.toPresheafFiber X x (Functor.obj shrinkYoneda.{w, v, u} Y)) :
          (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj Y).obj (op X))) →
            (fun (X : Type w) ↦ X) (Φ.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj Y)))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ Y) → (shrinkYoneda.{w, v, u}.obj Y).obj (op X)) f :
          Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} Y) (op X)) :
      (fun (X : Type w) ↦ X) (Functor.obj Φ.presheafFiber (Functor.obj shrinkYoneda.{w, v, u} Y)))
⊢ Eq (α := (fun (X : Type w) ↦ X) (Functor.obj Φ.presheafFiber (Functor.obj shrinkYoneda.{w, v, u} Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map Φ.presheafFiber (Functor.map shrinkYoneda.{w, v, u} f)) :
          (a : (fun (X : Type w) ↦ X) (Φ.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj X))) →
            (fun (X : Type w) ↦ X) (Φ.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (Iso.inv Φ.shrinkYonedaCompPresheafFiberIso) X) :
              (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj X)) →
                (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u} ⋙ Φ.presheafFiber).obj X))
            x :
          (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u} ⋙ Φ.presheafFiber).obj X)) :
      (fun (X : Type w) ↦ X) (Functor.obj Φ.presheafFiber (Functor.obj shrinkYoneda.{w, v, u} Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.toPresheafFiber X x (Functor.obj shrinkYoneda.{w, v, u} Y)) :
          (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj Y).obj (op X))) →
            (fun (X : Type w) ↦ X) (Φ.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj Y)))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ Y) → (shrinkYoneda.{w, v, u}.obj Y).obj (op X)) f :
          Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} Y) (op X)) :
      (fun (X : Type w) ↦ X) (Functor.obj Φ.presheafFiber (Functor.obj shrinkYoneda.{w, v, u} Y)))

Tactic:
rw [shrinkYonedaCompPresheafFiberIso_inv_app_toPresheafFiber]

Premises used: CategoryTheory.GrothendieckTopology.Point.shrinkYonedaCompPresheafFiberIso_inv_app_toPresheafFiber