-- Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
F G : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
f : F ⟶ G
inst_2 : PreservesFiniteProducts F
inst_3 : PreservesFiniteProducts G
X : C
x : G.obj (op X)
α : Type
w : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), (Presheaf.imageSieve (FA := TypeCat.Fun) f x).arrows (π a)
y : (a : α) → F.obj (op (Y a)) :=
  fun (a : α) ↦
    Exists.choose (p := fun (t : ToType (FC := TypeCat.Fun) (F.obj (op (Y a)))) ↦
      Eq (α := (fun (X : Type w) ↦ X) (G.obj (op (Y a))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op (Y a))) :
              (a_1 : (fun (X : Type w) ↦ X) (F.obj (op (Y a)))) → (fun (X : Type w) ↦ X) (G.obj (op (Y a))))
            t :
          (fun (X : Type w) ↦ X) (G.obj (op (Y a))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (π a).op) :
              (a_1 : (fun (X : Type w) ↦ X) (G.obj (op X))) → (fun (X : Type w) ↦ X) (G.obj (op (Y a))))
            x :
          (fun (X : Type w) ↦ X) (G.obj (op (Y a)))))
      ⋯
x_1 : Fintype α := Fintype.ofFinite α
ht : IsLimit (J := Discrete α) (F := Discrete.functor fun (a : α) ↦ F.obj (op (Y a)))
  (LimitCone.cone (Types.productLimitCone fun (a : α) ↦ F.obj (op (Y a)))) :=
  LimitCone.isLimit (Types.productLimitCone fun (a : α) ↦ F.obj (op (Y a)))
ht' : IsLimit (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))) :=
  ((Functor.Initial.isLimitWhiskerEquiv (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))).symm :
      (a : IsLimit (Cocone.op (Cofan.mk X π))) →
        IsLimit (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))))
    h.some.op
i : ((a : α) → F.obj (op (Y a))) ≅ F.obj (op X) :=
  ht.conePointsIsoOfNatIso (isLimitOfPreserves F ht')
    (Discrete.natIso fun (x : Discrete α) ↦ Iso.refl (F.obj (op (Y x.as))))
a : α
a₁ :
  Eq (α := G.obj (op (Y a)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op (Y a))) : (a_1 : F.obj (op (Y a))) → G.obj (op (Y a)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (π a).op) : (a_1 : F.obj (op X)) → F.obj (op (Y a)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) i.hom : (a : (a : α) → F.obj (op (Y a))) → F.obj (op X)) y :
              F.obj (op X)) :
          F.obj (op (Y a))) :
      G.obj (op (Y a)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op (Y a))) :
          (a_1 : (fun (X : Type w) ↦ X) (F.obj (op (Y a)))) → (fun (X : Type w) ↦ X) (G.obj (op (Y a))))
        (Exists.choose (p := fun (t : ToType (FC := TypeCat.Fun) (F.obj (op (Y a)))) ↦
          Eq (α := (fun (X : Type w) ↦ X) (G.obj (op (Y a))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op (Y a))) :
                  (a_1 : (fun (X : Type w) ↦ X) (F.obj (op (Y a)))) → (fun (X : Type w) ↦ X) (G.obj (op (Y a))))
                t :
              (fun (X : Type w) ↦ X) (G.obj (op (Y a))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (π a).op) :
                  (a_1 : (fun (X : Type w) ↦ X) (G.obj (op X))) → (fun (X : Type w) ↦ X) (G.obj (op (Y a))))
                x :
              (fun (X : Type w) ↦ X) (G.obj (op (Y a)))))
          ⋯) :
      (fun (X : Type w) ↦ X) (G.obj (op (Y a))))
⊢ Eq (α := G.obj (op (Y a)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (π a).op) : (a_1 : G.obj (op X)) → G.obj (op (Y a)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op X)) : (a : F.obj (op X)) → G.obj (op X))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) i.hom : (a : (a : α) → F.obj (op (Y a))) → F.obj (op X)) y :
              F.obj (op X)) :
          G.obj (op X)) :
      G.obj (op (Y a)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (π a).op) : (a_1 : G.obj (op X)) → G.obj (op (Y a))) x :
      G.obj (op (Y a)))

Tactic:
rw [← (h' a).choose_spec, ← NatTrans.naturality_apply (φ := f)]

Premises used: CategoryTheory.NatTrans.naturality_apply, Exists.choose_spec