-- 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) (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)))
⊢ Eq (α := (((Discrete.opposite α).inverse ⋙ Functor.op (Discrete.functor Y)) ⋙ G).obj { as := a })
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((G.mapCone (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π)))).π.app
              { as := a : Discrete α }) :
          (a_1 :
              ((Functor.const (Discrete α)).obj
                    (G.mapCone (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π)))).pt).obj
                { as := a }) →
            (((Discrete.opposite α).inverse ⋙ (Discrete.functor Y).op) ⋙ G).obj { as := a })
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op X)) :
              (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (G.obj (op X)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) i.hom :
                  (a : (fun (X : Type w) ↦ X) ((a : α) → F.obj (op (Y a)))) → (fun (X : Type w) ↦ X) (F.obj (op X)))
                y :
              (fun (X : Type w) ↦ X) (F.obj (op X))) :
          (fun (X : Type w) ↦ X) (G.obj (op X))) :
      (((Discrete.opposite α).inverse ⋙ Functor.op (Discrete.functor Y)) ⋙ G).obj { as := a })
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((G.mapCone (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π)))).π.app
              { as := a : Discrete α }) :
          (a_1 :
              ((Functor.const (Discrete α)).obj
                    (G.mapCone (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π)))).pt).obj
                { as := a }) →
            (((Discrete.opposite α).inverse ⋙ (Discrete.functor Y).op) ⋙ G).obj { as := a })
        x :
      (((Discrete.opposite α).inverse ⋙ Functor.op (Discrete.functor Y)) ⋙ G).obj { as := a })

Tactic:
simp only [Functor.comp_obj, Discrete.opposite_inverse_obj, Functor.op_obj, Discrete.functor_obj,
    Functor.mapCone_pt, Cone.whisker_pt, Cocone.op_pt, Cofan.mk_pt, Functor.const_obj_obj,
    Functor.mapCone_π_app, Cone.whisker_π, Cocone.op_π, Functor.whiskerLeft_app, NatTrans.op_app,
    Cofan.mk_ι_app]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Discrete.functor_obj, CategoryTheory.Limits.Cone.whisker_π, CategoryTheory.Limits.Cocone.op_pt, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.Limits.Cofan.mk_ι_app, CategoryTheory.Limits.Cofan.mk_pt, CategoryTheory.NatTrans.op_app, CategoryTheory.Functor.mapCone_pt, CategoryTheory.Functor.mapCone_π_app, CategoryTheory.Limits.Cone.whisker_pt, CategoryTheory.Limits.Cocone.op_π, CategoryTheory.Discrete.opposite_inverse_obj, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Functor.op_obj