-- 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
inst_2 : HasSheafify J (Type w)
inst_3 : J.WEqualsLocallyBijective (Type w) (FA := TypeCat.Fun)
hP : P.IsConservativeFamilyOfPoints
X : C
ι : Type u_1
inst_4 : Small.{w, u_1} ι
U : ι → C
f : (i : ι) → U i ⟶ X
hf :
  ∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
    ∃ (i : ι) (y : Φ.obj (P := P).fiber.obj (U i)),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map (f i)) :
            (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj (U i))) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
          y =
        x
Φ : P.FullSubcategory
i : ι
y : Φ.obj (P := P).fiber.obj (U i)
this :
  Eq (α := Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Iso.inv Φ.obj (P := P).shrinkYonedaCompPresheafFiberIso) X) :
          (a : Φ.obj.fiber.obj X) → Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map (f i)) :
              (a : Φ.obj.fiber.obj (U i)) → Φ.obj.fiber.obj X)
            y :
          Φ.obj (P := P).fiber.obj X) :
      Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Functor.map Φ.obj (P := P).presheafFiber (Functor.map shrinkYoneda.{w, v, u} (f i))) :
          (a : Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj (U i))) →
            Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app (Iso.inv Φ.obj (P := P).shrinkYonedaCompPresheafFiberIso) (U i)) :
              (a : Φ.obj.fiber.obj (U i)) → Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj (U i)))
            y :
          Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} (U i))) :
      Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} X))
refine_2 :
  Eq (α := Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Functor.map Φ.obj (P := P).presheafFiber
              (Sigma.desc fun (i : ι) ↦ Functor.map shrinkYoneda.{w, v, u} (f i))) :
          (a : Φ.obj.presheafFiber.obj (∐ fun (i : ι) ↦ shrinkYoneda.{w, v, u}.obj (U i))) →
            Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj X))
        (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                  (Functor.map Φ.obj (P := P).presheafFiber
                    (Sigma.ι (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w))
                      (fun (i : ι) ↦ Functor.obj shrinkYoneda.{w, v, u} (U i)) i)) :
                TypeCat.Fun (Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} (U i)))
                  (Functor.obj (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) Φ.obj (P := P).presheafFiber
                    (∐ fun (i : ι) ↦ Functor.obj shrinkYoneda.{w, v, u} (U i)))) :
              (a : Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj (U i))) →
                Φ.obj.presheafFiber.obj (∐ fun (i : ι) ↦ shrinkYoneda.{w, v, u}.obj (U i)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (NatTrans.app (Iso.inv Φ.obj (P := P).shrinkYonedaCompPresheafFiberIso) (U i)) :
                  (a : Φ.obj.fiber.obj (U i)) → Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj (U i)))
                y :
              Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} (U i))) :
          Functor.obj (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) Φ.obj (P := P).presheafFiber
            (∐ fun (i : ι) ↦ Functor.obj shrinkYoneda.{w, v, u} (U i))) :
      Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} X))
    (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (CategoryStruct.comp (Y :=
                Functor.obj (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) Φ.obj (P := P).presheafFiber
                  (∐ fun (i : ι) ↦ Functor.obj shrinkYoneda.{w, v, u} (U i)))
                (Functor.map Φ.obj (P := P).presheafFiber
                  (Sigma.ι (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w))
                    (fun (i : ι) ↦ Functor.obj shrinkYoneda.{w, v, u} (U i)) i))
                (Functor.map Φ.obj (P := P).presheafFiber
                  (Sigma.desc fun (i : ι) ↦ Functor.map shrinkYoneda.{w, v, u} (f i)))) :
            TypeCat.Fun (Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} (U i)))
              (Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} X))) :
          (a : Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj (U i))) →
            Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app (Iso.inv Φ.obj (P := P).shrinkYonedaCompPresheafFiberIso) (U i)) :
              (a : Φ.obj.fiber.obj (U i)) → Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj (U i)))
            y :
          Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} (U i))) :
      Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} X))
⊢ Eq (α := Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Functor.map Φ.obj (P := P).presheafFiber
              (Sigma.desc fun (i : ι) ↦ Functor.map shrinkYoneda.{w, v, u} (f i))) :
          (a : Φ.obj.presheafFiber.obj (∐ fun (i : ι) ↦ shrinkYoneda.{w, v, u}.obj (U i))) →
            Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj X))
        (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                  (Functor.map Φ.obj (P := P).presheafFiber
                    (Sigma.ι (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w))
                      (fun (i : ι) ↦ Functor.obj shrinkYoneda.{w, v, u} (U i)) i)) :
                TypeCat.Fun (Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} (U i)))
                  (Functor.obj (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) Φ.obj (P := P).presheafFiber
                    (∐ fun (i : ι) ↦ Functor.obj shrinkYoneda.{w, v, u} (U i)))) :
              (a : Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj (U i))) →
                Φ.obj.presheafFiber.obj (∐ fun (i : ι) ↦ shrinkYoneda.{w, v, u}.obj (U i)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (NatTrans.app (Iso.inv Φ.obj (P := P).shrinkYonedaCompPresheafFiberIso) (U i)) :
                  (a : Φ.obj.fiber.obj (U i)) → Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj (U i)))
                y :
              Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} (U i))) :
          Functor.obj (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) Φ.obj (P := P).presheafFiber
            (∐ fun (i : ι) ↦ Functor.obj shrinkYoneda.{w, v, u} (U i))) :
      Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Iso.inv Φ.obj (P := P).shrinkYonedaCompPresheafFiberIso) X) :
          (a : Φ.obj.fiber.obj X) → Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map (f i)) :
              (a : Φ.obj.fiber.obj (U i)) → Φ.obj.fiber.obj X)
            y :
          Φ.obj (P := P).fiber.obj X) :
      Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} X))

Tactic:
rw [this, ← Sigma.ι_desc (fun i ↦ shrinkYoneda.{w}.map (f i)) i, Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp