-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective (goal)
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_1 : PreservesLimitsOfShape (Discrete α)ᵒᵖ G
a : α
this_2 :
  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))))
        (x a) :
      (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))))
this :
  Eq.{w + 1} (α := ((j : α) → F.obj (op (Z j))) ⟶ F.obj (op (Z a))) (↾fun (f : (j : α) → F.obj (op (Z j))) ↦ f a)
    (Iso.inv (Types.productIso fun (a : α) ↦ F.obj (op (Z a))) ≫ Pi.π (fun (a : α) ↦ F.obj (op (Z a))) a)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := ∏ᶜ fun (j : α) ↦ F.obj (op (Z j)))
            (Iso.hom (PreservesProduct.iso F fun (x : α) ↦ op (Z x))) (Pi.π (fun (b : α) ↦ F.obj (op (Z b))) a)) :
        (a_1 : (fun (X : Type w) ↦ X) (F.obj (∏ᶜ fun (x : α) ↦ op (Z x)))) → (fun (X : Type w) ↦ X) (F.obj (op (Z a))))
      ((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))) =
    x a
have h₁ : (ConcreteCategory.hom (FC := TypeCat.Fun) (Pi.π (fun (b : α) ↦ F.obj (op (Z b))) a) :
      (a_1 : ∏ᶜ fun (j : α) ↦ F.obj (op (Z j))) → F.obj (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))) =
  x a
Tactic: simp only [types_comp_apply, Iso.inv_hom_id_apply]