-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Conservative (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P : ObjectProperty (GrothendieckTopology.Point.{w, v, u} J)
inst_1 : LocallySmall.{w, v, u} C
hP :
  ∀ ⦃X : C⦄ (S : Sieve.{v, u} X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
        ∃ (Y : C) (g : Y ⟶ X) (_ : S.arrows g) (y : Φ.obj (P := P).fiber.obj Y),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map g) :
                (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
              y =
            x) →
      S ∈ (J : (a : C) → Set (Sieve a)) X
F₁ : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
U : C
f : F₁ ⟶ Functor.obj shrinkYoneda.{w, v, u} U
inst_2 : Mono f
hf :
  ∀ (Φ : P.FullSubcategory),
    Function.Surjective (α := (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber F₁)) (β :=
      (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} U)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map Φ.obj (P := P).presheafFiber f)) :
        (a : (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj F₁)) →
          (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj U)))
V : C
g : unop (op V) ⟶ U
this :
  Membership.mem (γ := Set (Sieve.{v, u} (unop (op V)))) ((J : (a : C) → Set (Sieve a)) (unop (op V)))
    (Presheaf.imageSieve (FA := TypeCat.Fun) f
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj shrinkYoneda.{w, v, u} U) g.op) :
          (a : (shrinkYoneda.{w, v, u}.obj U).obj (op U)) → (shrinkYoneda.{w, v, u}.obj U).obj (op (unop (op V))))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op U) ⟶ U) → (shrinkYoneda.{w, v, u}.obj U).obj (op U))
            (𝟙 U) :
          Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} U) (op U))))
⊢ Presheaf.imageSieve (FA := TypeCat.Fun) f
      ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op V) ⟶ U) → (shrinkYoneda.{w, v, u}.obj U).obj (op V)) g) ∈
    (J : (a : C) → Set (Sieve a)) V
have hg : Eq (α :=
  (fun (X : Type w) ↦ X)
    (Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} (unop (op U))) (op (unop (op V)))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj shrinkYoneda.{w, v, u} (unop (op U))) g.op) :
        (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj (unop (op U))).obj (op U))) →
          (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj (unop (op U))).obj (op (unop (op V)))))
      ((Equiv.symm shrinkYonedaObjObjEquiv :
            (a : unop (op U) ⟶ unop (op U)) → (shrinkYoneda.{w, v, u}.obj (unop (op U))).obj (op U))
          (𝟙 (unop (op U))) :
        Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} (unop (op U))) (op U)) :
    (fun (X : Type w) ↦ X)
      (Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} (unop (op U))) (op (unop (op V)))))
  ((Equiv.symm shrinkYonedaObjObjEquiv :
        (a : unop (op (unop (op V))) ⟶ unop (op U)) → (shrinkYoneda.{w, v, u}.obj (unop (op U))).obj (op (unop (op V))))
      (g.op.unop ≫ 𝟙 (unop (op U))) :
    Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} (unop (op U))) (op (unop (op V))))
Tactic: have hg := shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm g.op (𝟙 _)