-- Module: Mathlib.CategoryTheory.Sites.Point.Map
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
F : Functor.{v, v', u, u'} C D
K : GrothendieckTopology.{v', u'} D
inst_2 : F.IsCocontinuous J K
X : D
R : Sieve.{v', u'} X
hR : R ∈ (K : (a : D) → Set (Sieve a)) X
U : C
f : F.obj U ⟶ X
V : C
g : V ⟶ U
hg : (Sieve.functorPullback F (Sieve.pullback f R)).arrows g
v : Φ.fiber.obj V
⊢ 𝟙 (F.obj ((Φ.fiber.elementsMk V v).fst (β := fun (c : C) ↦ Φ.fiber.obj c))) ≫ F.map g ≫ f =
    F.map
        (↑(Subtype.mk (p :=
              fun
                (f :
                  (Φ.fiber.elementsMk V v).fst (β := fun (c : C) ↦ Φ.fiber.obj c) ⟶
                    Sigma.fst (β := fun (c : C) ↦ Φ.fiber.obj c)
                      (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) U
                        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map g) :
                            (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj V)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj U))
                          v))) ↦
              Eq (α :=
                (fun (X : Type w) ↦ X)
                  (Φ.fiber.obj
                    (Sigma.fst (β := fun (c : C) ↦ Φ.fiber.obj c)
                      (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) U
                        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map g) :
                            (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj V)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj U))
                          v)))))
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
                      (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj (Φ.fiber.elementsMk V v).fst)) →
                        (fun (X : Type w) ↦ X)
                          (Φ.fiber.obj
                            ⟨U,
                                (ConcreteCategory.hom (Φ.fiber.map g) :
                                    (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj V)) →
                                      (fun (X : Type w) ↦ X) (Φ.fiber.obj U))
                                  v⟩.fst))
                    ((Φ.fiber.elementsMk V v).snd (β := fun (c : C) ↦ Φ.fiber.obj c)) :
                  (fun (X : Type w) ↦ X)
                    (Φ.fiber.obj
                      (Sigma.fst (β := fun (c : C) ↦ Φ.fiber.obj c)
                        (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) U
                          ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map g) :
                              (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj V)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj U))
                            v)))))
                (Sigma.snd (β := fun (c : C) ↦ Φ.fiber.obj c)
                    (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) U
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map g) :
                          (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj V)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj U))
                        v)) :
                  Φ.fiber.obj
                    (Sigma.fst (β := fun (c : C) ↦ Φ.fiber.obj c)
                      (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) U
                        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map g) :
                            (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj V)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj U))
                          v)))))
              g ⋯) :
          (Φ.fiber.elementsMk V v).fst ⟶ U) ≫
      f

Tactic:
simp