-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct (goal)
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)))
⊢ (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
have 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 α }))
Tactic: refine Types.limit_ext' _ _ _ (fun ⟨s⟩ => ?_)