-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Presheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X : C
S : Sieve.{v, u} X
hS :
  ∀ (Φ : ObjectProperty.FullSubcategory (C := Point.{w, v, u} (C := C) ⊥) (pointsBot C))
    (x : Φ.obj (P := pointsBot C).fiber.obj X),
    ∃ (Y : C) (g : Y ⟶ X) (_ : S.arrows g) (y : Φ.obj (P := pointsBot C).fiber.obj Y),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := pointsBot C).fiber.map g) :
            (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
          y =
        x
Y : C
a : Y ⟶ X
ha : S.arrows a
b : X ⟶ Y
hb :
  Eq (α := Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (Functor.map shrinkYoneda.{w, v, u} a) (op X)) :
          (a : (shrinkYoneda.{w, v, u}.obj Y).obj (op X)) → (shrinkYoneda.{w, v, u}.obj X).obj (op X))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : X ⟶ Y) → (shrinkYoneda.{w, v, u}.obj Y).obj (op X)) b :
          Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} Y) (op X)) :
      Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X))
    ((Equiv.symm shrinkYonedaObjObjEquiv : (a : 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))
rw :
  Eq.{w + 1} (α := Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X))
    ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op X)) (b ≫ a) :
      Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (Functor.map shrinkYoneda.{w, v, u} a) (op X)) :
          (a : (shrinkYoneda.{w, v, u}.obj Y).obj (op X)) → (shrinkYoneda.{w, v, u}.obj X).obj (op X))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : X ⟶ Y) → (shrinkYoneda.{w, v, u}.obj Y).obj (op X)) b :
          Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} Y) (op X)) :
      Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X))
⊢ Eq.{w + 1} (α := Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X))
    ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op X)) (b ≫ a) :
      Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op 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))
have rw₁ : Eq.{w + 1} (α := Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X))
  ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op X)) (b ≫ a) :
    Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X))
  ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op X)) (b ≫ a) :
    Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X))
Tactic: rw [← hb, shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm]