-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Basic (goal)
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
⊢ 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)))
have 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)))
Tactic: rw [shrinkYonedaCompPresheafFiberIso_inv_app_toPresheafFiber]