-- 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)))
refine_2 :
  ∀ (x_1 : Discrete α) (s : α),
    Eq (α :=
      (fun (X : Type u) ↦ X) (Functor.obj (Discrete.functor fun (s : α) ↦ colimit (F s)) { as := s : Discrete α }))
      ((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 }))
          ((hom (FC := TypeCat.Fun) (colimitPointwiseProductToProductColimit (I := I) F) :
              (a : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F))) →
                (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
            ((hom (FC := TypeCat.Fun) (colimit.ι (pointwiseProduct (I := I) F) k) :
                  (a : (fun (X : Type u) ↦ X) ((pointwiseProduct F).obj k)) →
                    (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F)))
                ((hom (FC := TypeCat.Fun) (productIso ((Functor.pi (C := I) (D := fun (i : α) ↦ Type u) F).obj k)).inv :
                      (a : (fun (X : Type u) ↦ X) ((j : α) → (Functor.pi F).obj k j)) →
                        (fun (X : Type u) ↦ X) (∏ᶜ (Functor.pi F).obj k))
                    p :
                  (fun (X : Type u) ↦ X) (∏ᶜ (Functor.pi (C := I) (D := fun (i : α) ↦ Type u) F).obj k)) :
              (fun (X : Type u) ↦ X) (colimit (pointwiseProduct (I := I) F)))) :
        (fun (X : Type u) ↦ X) (Functor.obj (Discrete.functor fun (s : α) ↦ colimit (F s)) { as := s : Discrete α }))
      ((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 α }))
⊢ (hom (FC := TypeCat.Fun) (colimitPointwiseProductToProductColimit (I := I) F) :
        (a : (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F))) →
          (fun (X : Type u) ↦ X) (∏ᶜ fun (s : α) ↦ colimit (F s)))
      ((hom (FC := TypeCat.Fun) (colimit.ι (pointwiseProduct (I := I) F) k) :
            (a : (fun (X : Type u) ↦ X) ((pointwiseProduct F).obj k)) →
              (fun (X : Type u) ↦ X) (colimit (pointwiseProduct F)))
          ((hom (FC := TypeCat.Fun) (productIso ((Functor.pi (C := I) (D := fun (i : α) ↦ Type u) F).obj k)).inv :
                (a : (fun (X : Type u) ↦ X) ((j : α) → (Functor.pi F).obj k j)) →
                  (fun (X : Type u) ↦ X) (∏ᶜ (Functor.pi F).obj k))
              p :
            (fun (X : Type u) ↦ X) (∏ᶜ (Functor.pi (C := I) (D := fun (i : α) ↦ Type u) F).obj k)) :
        (fun (X : Type u) ↦ X) (colimit (pointwiseProduct (I := I) F))) =
    x

Tactic:
refine Types.limit_ext' _ _ _ (fun ⟨s⟩ => ?_)

Premises used: CategoryTheory.Limits.Types.limit_ext'