-- Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
F G : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
f : F ⟶ G
inst_3 : PreservesFiniteProducts F
inst_4 : PreservesFiniteProducts G
U : C
y : ToType (FC := TypeCat.Fun) (G.obj (op U))
α : Type
w : Finite α
Z : α → C
π : (a : α) → Z a ⟶ U
h : EffectiveEpiFamily Z π
h' : ∀ (a : α), (Presheaf.imageSieve (FA := TypeCat.Fun) f y).arrows (π a)
x : (a : α) → F.obj (op (Z a)) :=
  fun (a : α) ↦
    Exists.choose (p := fun (t : ToType (FC := TypeCat.Fun) (F.obj (op (Z a)))) ↦
      Eq (α := (fun (X : Type w) ↦ X) (G.obj (op (Z a))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op (Z a))) :
              (a_1 : (fun (X : Type w) ↦ X) (F.obj (op (Z a)))) → (fun (X : Type w) ↦ X) (G.obj (op (Z a))))
            t :
          (fun (X : Type w) ↦ X) (G.obj (op (Z a))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (π a).op) :
              (a_1 : (fun (X : Type w) ↦ X) (G.obj (op U))) → (fun (X : Type w) ↦ X) (G.obj (op (Z a))))
            y :
          (fun (X : Type w) ↦ X) (G.obj (op (Z a)))))
      ⋯
x_1 : Fintype α := Fintype.ofFinite α
i' : ((a : α) → F.obj (op (Z a))) ≅ F.obj (op (sigmaObj.{0, v_1, u_1} Z)) :=
  Iso.symm (Types.productIso fun (a : α) ↦ F.obj (op (Z a))) ≪≫
    Iso.symm (PreservesProduct.iso F fun (a : α) ↦ op (Z a)) ≪≫ F.mapIso (Iso.symm (opCoproductIsoProduct Z))
this : PreservesLimitsOfShape (Discrete α)ᵒᵖ G
a : α
a₁ :
  Eq (α := G.obj (op (Z a)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op (Z a))) : (a_1 : F.obj (op (Z a))) → G.obj (op (Z a)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (Sigma.ι Z a))) :
              (a_1 : F.obj (op (∐ Z))) → F.obj (op (Z a)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Iso.inv (opCoproductIsoProduct Z))) :
                  (a : F.obj (∏ᶜ fun (a : α) ↦ op (Z a))) → F.obj (op (∐ Z)))
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (PreservesProduct.iso F fun (a : α) ↦ op (Z a))) :
                      (a : ∏ᶜ fun (a : α) ↦ F.obj (op (Z a))) → F.obj (∏ᶜ fun (a : α) ↦ op (Z a)))
                    ((ConcreteCategory.hom (FC := TypeCat.Fun)
                            (Iso.inv (Types.productIso fun (a : α) ↦ F.obj (op (Z a)))) :
                          (a : (a : α) → F.obj (op (Z a))) → ∏ᶜ fun (a : α) ↦ F.obj (op (Z a)))
                        x :
                      ∏ᶜ fun (a : α) ↦ F.obj (op (Z a))) :
                  F.obj (piObj.{0, v_1, u_1} fun (a : α) ↦ op (Z a))) :
              F.obj (op (sigmaObj.{0, v_1, u_1} Z))) :
          F.obj (op (Z a))) :
      G.obj (op (Z a)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (Quiver.Hom.op (Sigma.ι Z a))) :
          (a_1 : G.obj (op (∐ Z))) → G.obj (op (Z a)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (Quiver.Hom.op (Sigma.desc π))) :
              (a : G.obj (op U)) → G.obj (op (∐ Z)))
            y :
          G.obj (op (sigmaObj.{0, v_1, u_1} Z))) :
      G.obj (op (Z a)))
⊢ Eq (α := (Functor.op (Discrete.functor Z) ⋙ G).obj (op { as := a }))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((G.mapCone (Cocone.op (Cofan.mk (sigmaObj.{0, v_1, u_1} Z) (Sigma.ι Z)))).π.app
              (op { as := a : Discrete α })) :
          (a_1 :
              ((Functor.const (Discrete α)ᵒᵖ).obj (G.mapCone (Cocone.op (Cofan.mk (∐ Z) (Sigma.ι Z)))).pt).obj
                (op { as := a })) →
            ((Discrete.functor Z).op ⋙ G).obj (op { as := a }))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op (sigmaObj.{0, v_1, u_1} Z))) :
              (a : (fun (X : Type w) ↦ X) (F.obj (op (∐ Z)))) → (fun (X : Type w) ↦ X) (G.obj (op (∐ Z))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) i'.hom :
                  (a : (fun (X : Type w) ↦ X) ((a : α) → F.obj (op (Z a)))) → (fun (X : Type w) ↦ X) (F.obj (op (∐ Z))))
                x :
              (fun (X : Type w) ↦ X) (F.obj (op (sigmaObj.{0, v_1, u_1} Z)))) :
          (fun (X : Type w) ↦ X) (G.obj (op (sigmaObj.{0, v_1, u_1} Z)))) :
      (Functor.op (Discrete.functor Z) ⋙ G).obj (op { as := a }))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((G.mapCone (Cocone.op (Cofan.mk (sigmaObj.{0, v_1, u_1} Z) (Sigma.ι Z)))).π.app
              (op { as := a : Discrete α })) :
          (a_1 :
              ((Functor.const (Discrete α)ᵒᵖ).obj (G.mapCone (Cocone.op (Cofan.mk (∐ Z) (Sigma.ι Z)))).pt).obj
                (op { as := a })) →
            ((Discrete.functor Z).op ⋙ G).obj (op { as := a }))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (Quiver.Hom.op (Sigma.desc π))) :
              (a : (fun (X : Type w) ↦ X) (G.obj (op U))) → (fun (X : Type w) ↦ X) (G.obj (op (∐ Z))))
            y :
          (fun (X : Type w) ↦ X) (G.obj (op (sigmaObj.{0, v_1, u_1} Z)))) :
      (Functor.op (Discrete.functor Z) ⋙ G).obj (op { as := a }))

Tactic:
simp only [Functor.comp_obj, Functor.op_obj, Discrete.functor_obj_eq_as, Functor.mapCone_pt,
      Cocone.op_pt, Cofan.mk_pt, Functor.const_obj_obj, Functor.mapCone_π_app, Cocone.op_π,
      NatTrans.op_app, Cofan.mk_ι_app, Functor.mapIso_symm, Iso.trans_hom, Iso.symm_hom,
      Functor.mapIso_inv, comp_apply, ← f.naturality_apply (Sigma.ι Z a).op, i']

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.NatTrans.naturality_apply, Quiver.Hom.op, CategoryTheory.Limits.Cocone.op_pt, CategoryTheory.Iso.symm_hom, CategoryTheory.Limits.Sigma.ι, CategoryTheory.Limits.Cofan.mk_ι_app, CategoryTheory.Limits.Cofan.mk_pt, CategoryTheory.Discrete.functor_obj_eq_as, CategoryTheory.NatTrans.op_app, CategoryTheory.Functor.mapCone_pt, CategoryTheory.Functor.mapCone_π_app, CategoryTheory.comp_apply, CategoryTheory.Iso.trans_hom, CategoryTheory.Functor.mapIso_symm, CategoryTheory.Functor.mapIso_inv, CategoryTheory.Limits.Cocone.op_π, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Functor.op_obj