-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
α : Type u
I : α → Type u
inst : (i : α) → SmallCategory (I i)
inst_1 : ∀ (i : α), IsFiltered.{u, u} (I i)
F : (i : α) → I i ⥤ Type u
x : (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s))
k : (s : α) → I s
p : (s : α) → (F s).obj (k s)
hk :
  ∀ (s : α),
    Eq (α := (fun (X : Type u) ↦ X) (colimit (F s)))
      ((hom (FC := TypeCat.Fun) (colimit.ι (F s) (k s)) :
            (a : (fun (X : Type u) ↦ X) ((F s).obj (k s))) → (fun (X : Type u) ↦ X) (colimit (F s)))
          (p s) :
        (fun (X : Type u) ↦ X) (colimit (F s)))
      ((hom (FC := TypeCat.Fun) (Pi.π (fun (s : α) ↦ colimit (F s)) s) :
            (a : (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s))) → (fun (X : Type u) ↦ X) (colimit (F s)))
          x :
        (fun (X : Type u) ↦ X) (colimit (F s)))
x_1 : Discrete α
s : α
this :
  Eq (α := colimit (F s))
    ((hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := colimit (pointwiseProduct (I := I) F))
              (colimit.ι (pointwiseProduct (I := I) F) k)
              (colimitPointwiseProductToProductColimit (I := I) F ≫ Pi.π (fun (s : α) ↦ colimit (F s)) s)) :
          (a : (pointwiseProduct F).obj k) → colimit (F s))
        ((hom (FC := TypeCat.Fun) (Iso.inv (productIso fun (j : α) ↦ (F j).obj (k j))) :
              (a : (fun (X : Type u) ↦ X) ((j : α) → (F j).obj (k j))) →
                (fun (X : Type u) ↦ X) (∏ᶜ fun (j : α) ↦ (F j).obj (k j)))
            p :
          (fun (X : Type u) ↦ X) (∏ᶜ fun (j : α) ↦ (F j).obj (k j))) :
      colimit (F s))
    ((hom (FC := TypeCat.Fun)
            (Pi.π ((Functor.pi (C := I) (D := fun (i : α) ↦ Type u) F).obj k) s ≫ colimit.ι (F s) (k s)) :
          (a : (pointwiseProduct F).obj k) → colimit (F s))
        ((hom (FC := TypeCat.Fun) (Iso.inv (productIso fun (j : α) ↦ (F j).obj (k j))) :
              (a : (fun (X : Type u) ↦ X) ((j : α) → (F j).obj (k j))) →
                (fun (X : Type u) ↦ X) (∏ᶜ fun (j : α) ↦ (F j).obj (k j)))
            p :
          (fun (X : Type u) ↦ X) (∏ᶜ fun (j : α) ↦ (F j).obj (k j))) :
      colimit (F s))
⊢ Eq (α := colimit (F s))
    ((hom (FC := TypeCat.Fun)
            (Pi.π ((Functor.pi (C := I) (D := fun (i : α) ↦ Type u) F).obj k) s ≫ colimit.ι (F s) (k s)) :
          (a : (pointwiseProduct F).obj k) → colimit (F s))
        ((hom (FC := TypeCat.Fun) (Iso.inv (productIso fun (j : α) ↦ (F j).obj (k j))) :
              (a : (fun (X : Type u) ↦ X) ((j : α) → (F j).obj (k j))) →
                (fun (X : Type u) ↦ X) (∏ᶜ fun (j : α) ↦ (F j).obj (k j)))
            p :
          (fun (X : Type u) ↦ X) (∏ᶜ fun (j : α) ↦ (F j).obj (k j))) :
      colimit (F s))
    ((hom (FC := TypeCat.Fun) (limit.π (Discrete.functor fun (s : α) ↦ colimit (F s)) { as := s : Discrete α }) :
          (a : (fun (X : Type u) ↦ X) (limit (Discrete.functor fun (s : α) ↦ colimit (F s)))) →
            (fun (X : Type u) ↦ X) ((Discrete.functor fun (s : α) ↦ colimit (F s)).obj { as := s }))
        x :
      (fun (X : Type u) ↦ X) (Functor.obj (Discrete.functor fun (s : α) ↦ colimit (F s)) { as := s : Discrete α }))

Tactic:
simpa [Functor.pi] using hk _

Premises used: CategoryTheory.Functor.pi