-- Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
X Y Z : C
x : X ⟶ Y
x_1 : Y ⟶ Z
h :
  ∀ (val : F.obj X),
    Eq (α := F.obj Z ⊕ G.obj Z)
      (TypeCat.Fun.toFun (X := F.obj X ⊕ G.obj X)
        (hom (FC := TypeCat.Fun)
          (↾Sum.map
              (⇑(hom (FC := TypeCat.Fun) (F.map (x ≫ x_1))) :
                (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Z))
              (⇑(hom (FC := TypeCat.Fun) (G.map (x ≫ x_1))) :
                (a : (fun (X : Type w) ↦ X) (G.obj X)) → (fun (X : Type w) ↦ X) (G.obj Z))))
        (Sum.inl val))
      (TypeCat.Fun.toFun (X := F.obj X ⊕ G.obj X)
        (hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := F.obj Y ⊕ G.obj Y)
            (↾Sum.map
                (⇑(hom (FC := TypeCat.Fun) (F.map x)) :
                  (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Y))
                (⇑(hom (FC := TypeCat.Fun) (G.map x)) :
                  (a : (fun (X : Type w) ↦ X) (G.obj X)) → (fun (X : Type w) ↦ X) (G.obj Y)))
            (↾Sum.map
                (⇑(hom (FC := TypeCat.Fun) (F.map x_1)) :
                  (a : (fun (X : Type w) ↦ X) (F.obj Y)) → (fun (X : Type w) ↦ X) (F.obj Z))
                (⇑(hom (FC := TypeCat.Fun) (G.map x_1)) :
                  (a : (fun (X : Type w) ↦ X) (G.obj Y)) → (fun (X : Type w) ↦ X) (G.obj Z)))))
        (Sum.inl val))
h₁ :
  ∀ (val : G.obj X),
    Eq (α := F.obj Z ⊕ G.obj Z)
      (TypeCat.Fun.toFun (X := F.obj X ⊕ G.obj X)
        (hom (FC := TypeCat.Fun)
          (↾Sum.map
              (⇑(hom (FC := TypeCat.Fun) (F.map (x ≫ x_1))) :
                (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Z))
              (⇑(hom (FC := TypeCat.Fun) (G.map (x ≫ x_1))) :
                (a : (fun (X : Type w) ↦ X) (G.obj X)) → (fun (X : Type w) ↦ X) (G.obj Z))))
        (Sum.inr val))
      (TypeCat.Fun.toFun (X := F.obj X ⊕ G.obj X)
        (hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := F.obj Y ⊕ G.obj Y)
            (↾Sum.map
                (⇑(hom (FC := TypeCat.Fun) (F.map x)) :
                  (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Y))
                (⇑(hom (FC := TypeCat.Fun) (G.map x)) :
                  (a : (fun (X : Type w) ↦ X) (G.obj X)) → (fun (X : Type w) ↦ X) (G.obj Y)))
            (↾Sum.map
                (⇑(hom (FC := TypeCat.Fun) (F.map x_1)) :
                  (a : (fun (X : Type w) ↦ X) (F.obj Y)) → (fun (X : Type w) ↦ X) (F.obj Z))
                (⇑(hom (FC := TypeCat.Fun) (G.map x_1)) :
                  (a : (fun (X : Type w) ↦ X) (G.obj Y)) → (fun (X : Type w) ↦ X) (G.obj Z)))))
        (Sum.inr val))
⊢ Eq (α := F.obj X ⊕ G.obj X ⟶ F.obj Z ⊕ G.obj Z)
    (↾Sum.map
        (⇑(hom (FC := TypeCat.Fun) (F.map (x ≫ x_1))) :
          (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Z))
        (⇑(hom (FC := TypeCat.Fun) (G.map (x ≫ x_1))) :
          (a : (fun (X : Type w) ↦ X) (G.obj X)) → (fun (X : Type w) ↦ X) (G.obj Z)))
    (CategoryStruct.comp (Y := F.obj Y ⊕ G.obj Y)
      (↾Sum.map
          (⇑(hom (FC := TypeCat.Fun) (F.map x)) :
            (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Y))
          (⇑(hom (FC := TypeCat.Fun) (G.map x)) :
            (a : (fun (X : Type w) ↦ X) (G.obj X)) → (fun (X : Type w) ↦ X) (G.obj Y)))
      (↾Sum.map
          (⇑(hom (FC := TypeCat.Fun) (F.map x_1)) :
            (a : (fun (X : Type w) ↦ X) (F.obj Y)) → (fun (X : Type w) ↦ X) (F.obj Z))
          (⇑(hom (FC := TypeCat.Fun) (G.map x_1)) :
            (a : (fun (X : Type w) ↦ X) (G.obj Y)) → (fun (X : Type w) ↦ X) (G.obj Z))))

Tactic:
ext ⟨⟩