-- Module: Mathlib.CategoryTheory.Sites.Point.Conservative
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₁ F₂ : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
f : F₁ ⟶ F₂
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 F₂))
      (⇑(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 F₂))
this_1 :
  ∀ {F₁ F₂ : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)} (f : F₁ ⟶ F₂) [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 F₂))
          (⇑(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 F₂)))
    (hF₂ : ∃ (U : C), F₂ = Functor.obj shrinkYoneda.{w, v, u} U), Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) f
hF₂ : ¬∃ (U : C), F₂ = Functor.obj shrinkYoneda.{w, v, u} U
U : C
s : ToType (FC := TypeCat.Fun) (F₂.obj (op U))
f' : pullback (Y := Functor.obj shrinkYoneda.{w, v, u} U) f
    ((Equiv.symm shrinkYonedaEquiv : (a : F₂.obj (op U)) → shrinkYoneda.{w, v, u}.obj U ⟶ F₂) s) ⟶
  Functor.obj shrinkYoneda.{w, v, u} U :=
  pullback.snd f ((Equiv.symm shrinkYonedaEquiv : (a : F₂.obj (op U)) → shrinkYoneda.{w, v, u}.obj U ⟶ F₂) s)
hf' :
  ∀ (Φ : P.FullSubcategory),
    Function.Surjective (α :=
      (fun (X : Type w) ↦ X)
        (Functor.obj Φ.obj (P := P).presheafFiber
          (pullback (Y := Functor.obj shrinkYoneda.{w, v, u} U) f
            ((Equiv.symm shrinkYonedaEquiv : (a : F₂.obj (op U)) → shrinkYoneda.{w, v, u}.obj U ⟶ F₂) s))))
      (β := (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
                (pullback f ((shrinkYonedaEquiv.symm : (a : F₂.obj (op U)) → shrinkYoneda.{w, v, u}.obj U ⟶ F₂) s)))) →
          (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj U)))
this : Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) f'
V : C
g : V ⟶ U
v :
  ToType (FC := TypeCat.Fun)
    ((pullback (Y := Functor.obj shrinkYoneda.{w, v, u} U) f
          ((Equiv.symm shrinkYonedaEquiv : (a : F₂.obj (op U)) → shrinkYoneda.{w, v, u}.obj U ⟶ F₂) s)).obj
      (op V))
hv :
  Eq (α := (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} U) (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f'.app (op V)) :
          (a :
              (fun (X : Type w) ↦ X)
                ((pullback f ((shrinkYonedaEquiv.symm : (a : F₂.obj (op U)) → shrinkYoneda.{w, v, u}.obj U ⟶ F₂) s)).obj
                  (op V))) →
            (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj U).obj (op V)))
        v :
      (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} U) (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj shrinkYoneda.{w, v, u} U) g.op) :
          (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj U).obj (op (unop (op U))))) →
            (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj U).obj (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)) :
      (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} U) (op V)))
inr :
  Eq (α := F₂.obj (op V))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app
              (pullback.snd f
                  ((Equiv.symm shrinkYonedaEquiv : (a : F₂.obj (op U)) → shrinkYoneda.{w, v, u}.obj U ⟶ F₂) s) ≫
                (Equiv.symm shrinkYonedaEquiv : (a : F₂.obj (op U)) → shrinkYoneda.{w, v, u}.obj U ⟶ F₂) s)
              (op V)) :
          (a :
              (pullback f ((shrinkYonedaEquiv.symm : (a : F₂.obj (op U)) → shrinkYoneda.{w, v, u}.obj U ⟶ F₂) s)).obj
                (op V)) →
            F₂.obj (op V))
        v :
      F₂.obj (op V))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F₂.map g.op) :
          (a : (fun (X : Type w) ↦ X) (F₂.obj (op U))) → (fun (X : Type w) ↦ X) (F₂.obj (op V)))
        s :
      (fun (X : Type w) ↦ X) (F₂.obj (op V)))
⊢ Eq (α := (fun (X : Type w) ↦ X) (F₂.obj (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op V)) :
          (a : (fun (X : Type w) ↦ X) (F₁.obj (op V))) → (fun (X : Type w) ↦ X) (F₂.obj (op V)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app
                  (pullback.fst f
                    ((Equiv.symm shrinkYonedaEquiv : (a : F₂.obj (op U)) → shrinkYoneda.{w, v, u}.obj U ⟶ F₂) s))
                  (op V)) :
              (a :
                  (fun (X : Type w) ↦ X)
                    ((pullback f
                          ((shrinkYonedaEquiv.symm : (a : F₂.obj (op U)) → shrinkYoneda.{w, v, u}.obj U ⟶ F₂) s)).obj
                      (op V))) →
                (fun (X : Type w) ↦ X) (F₁.obj (op V)))
            v :
          (fun (X : Type w) ↦ X) (F₁.obj (op V))) :
      (fun (X : Type w) ↦ X) (F₂.obj (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F₂.map g.op) :
          (a : (fun (X : Type w) ↦ X) (F₂.obj (op U))) → (fun (X : Type w) ↦ X) (F₂.obj (op V)))
        s :
      (fun (X : Type w) ↦ X) (F₂.obj (op V)))

Tactic:
refine (ConcreteCategory.congr_hom (NatTrans.congr_app
      (pullback.condition (f := f)) (op V)) _).trans ?_

Premises used: CategoryTheory.NatTrans.congr_app, Opposite.op, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Limits.pullback.condition, Eq.trans