-- Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
α : Type w
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasColimitsOfShape.{w, w, v, u} (Finset (Discrete α)) C
F : Functor.{w, v, w, u} (Discrete α) C
s : Cocone F
m :
  Cocone.pt.{w, v, w, u} (J := Discrete α) (F := F)
      { pt := colimit (liftToFinsetObj F),
        ι :=
          Discrete.natTrans fun (j : Discrete α) ↦
            CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : ↥{j}) ↦ F.obj (↑x : Discrete α))
              (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥{j}) ↦ F.obj (↑x : Discrete α))
                (Subtype.mk (p := fun (x : Discrete α) ↦ Membership.mem (γ := Finset (Discrete α)) {j} x) j ⋯))
              (colimit.ι (liftToFinsetObj F) {j}) :
        Cocone F } ⟶
    s.pt
h :
  ∀ (j : Discrete α),
    NatTrans.app
          (Cocone.ι
            { pt := colimit (liftToFinsetObj F),
              ι :=
                Discrete.natTrans fun (j : Discrete α) ↦
                  CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : ↥{j}) ↦ F.obj (↑x : Discrete α))
                    (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥{j}) ↦ F.obj (↑x : Discrete α))
                      (Subtype.mk (p := fun (x : Discrete α) ↦ Membership.mem (γ := Finset (Discrete α)) {j} x) j ⋯))
                    (colimit.ι (liftToFinsetObj F) {j}) })
          j ≫
        m =
      s.ι.app j
t : Finset (Discrete α)
w :
  ∀ (j : Discrete ↥t),
    colimit.ι (Discrete.functor fun (x : ↥t) ↦ F.obj (↑x : Discrete α)) j ≫
        colimit.ι
            { obj := fun (s : Finset (Discrete α)) ↦ sigmaObj.{w, v, u} fun (x : ↥s) ↦ F.obj (↑x : Discrete α),
              map := fun {x Y : Finset (Discrete α)} (h : x ⟶ Y) ↦
                Sigma.desc fun (y : ↥x) ↦
                  Sigma.ι.{w, v, u} (C := C) (fun (x : ↥Y) ↦ F.obj (↑x : Discrete α))
                    (Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ Y) (↑y : Discrete α) ⋯),
              map_id := ⋯, map_comp := ⋯ : Functor.{w, v, w, u} (Finset (Discrete α)) C }
            t ≫
          m =
      CategoryStruct.comp (Y :=
        colimit.{w, w, v, u} (J := Discrete ↥t) (Discrete.functor fun (x : ↥t) ↦ F.obj (↑x : Discrete α)))
        (colimit.ι (Discrete.functor fun (x : ↥t) ↦ F.obj (↑x : Discrete α)) j)
        (CategoryStruct.comp (Y :=
          colimit.{w, w, v, u} (J := Finset (Discrete α))
            { obj := fun (s : Finset (Discrete α)) ↦ sigmaObj.{w, v, u} fun (x : ↥s) ↦ F.obj (↑x : Discrete α),
              map := fun {x Y : Finset (Discrete α)} (h : x ⟶ Y) ↦
                Sigma.desc fun (y : ↥x) ↦
                  Sigma.ι.{w, v, u} (C := C) (fun (x : ↥Y) ↦ F.obj (↑x : Discrete α))
                    (Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ Y) (↑y : Discrete α) ⋯),
              map_id := ⋯, map_comp := ⋯ })
          (colimit.ι
            { obj := fun (s : Finset (Discrete α)) ↦ sigmaObj.{w, v, u} fun (x : ↥s) ↦ F.obj (↑x : Discrete α),
              map := fun {x Y : Finset (Discrete α)} (h : x ⟶ Y) ↦
                Sigma.desc fun (y : ↥x) ↦
                  Sigma.ι.{w, v, u} (C := C) (fun (x : ↥Y) ↦ F.obj (↑x : Discrete α))
                    (Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ Y) (↑y : Discrete α) ⋯),
              map_id := ⋯, map_comp := ⋯ }
            t)
          (colimit.desc
            { obj := fun (s : Finset (Discrete α)) ↦ sigmaObj.{w, v, u} fun (x : ↥s) ↦ F.obj (↑x : Discrete α),
              map := fun {x Y : Finset (Discrete α)} (h : x ⟶ Y) ↦
                Sigma.desc fun (y : ↥x) ↦
                  Sigma.ι.{w, v, u} (C := C) (fun (x : ↥Y) ↦ F.obj (↑x : Discrete α))
                    (Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ Y) (↑y : Discrete α) ⋯),
              map_id := ⋯, map_comp := ⋯ }
            { pt := s.pt,
              ι :=
                { app := fun (x : Finset (Discrete α)) ↦ Sigma.desc fun (x_1 : ↥x) ↦ s.ι.app (↑x_1 : Discrete α),
                  naturality := ⋯ } }))
⊢ colimit.ι
        { obj := fun (s : Finset (Discrete α)) ↦ sigmaObj.{w, v, u} fun (x : ↥s) ↦ F.obj (↑x : Discrete α),
          map := fun {x Y : Finset (Discrete α)} (h : x ⟶ Y) ↦
            Sigma.desc fun (y : ↥x) ↦
              Sigma.ι.{w, v, u} (C := C) (fun (x : ↥Y) ↦ F.obj (↑x : Discrete α))
                (Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ Y) (↑y : Discrete α) ⋯),
          map_id := ⋯, map_comp := ⋯ : Functor.{w, v, w, u} (Finset (Discrete α)) C }
        t ≫
      m =
    CategoryStruct.comp (Y :=
      colimit.{w, w, v, u} (J := Finset (Discrete α))
        { obj := fun (s : Finset (Discrete α)) ↦ sigmaObj.{w, v, u} fun (x : ↥s) ↦ F.obj (↑x : Discrete α),
          map := fun {x Y : Finset (Discrete α)} (h : x ⟶ Y) ↦
            Sigma.desc fun (y : ↥x) ↦
              Sigma.ι.{w, v, u} (C := C) (fun (x : ↥Y) ↦ F.obj (↑x : Discrete α))
                (Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ Y) (↑y : Discrete α) ⋯),
          map_id := ⋯, map_comp := ⋯ })
      (colimit.ι
        { obj := fun (s : Finset (Discrete α)) ↦ sigmaObj.{w, v, u} fun (x : ↥s) ↦ F.obj (↑x : Discrete α),
          map := fun {x Y : Finset (Discrete α)} (h : x ⟶ Y) ↦
            Sigma.desc fun (y : ↥x) ↦
              Sigma.ι.{w, v, u} (C := C) (fun (x : ↥Y) ↦ F.obj (↑x : Discrete α))
                (Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ Y) (↑y : Discrete α) ⋯),
          map_id := ⋯, map_comp := ⋯ }
        t)
      (colimit.desc
        { obj := fun (s : Finset (Discrete α)) ↦ sigmaObj.{w, v, u} fun (x : ↥s) ↦ F.obj (↑x : Discrete α),
          map := fun {x Y : Finset (Discrete α)} (h : x ⟶ Y) ↦
            Sigma.desc fun (y : ↥x) ↦
              Sigma.ι.{w, v, u} (C := C) (fun (x : ↥Y) ↦ F.obj (↑x : Discrete α))
                (Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ Y) (↑y : Discrete α) ⋯),
          map_id := ⋯, map_comp := ⋯ }
        { pt := s.pt,
          ι :=
            { app := fun (x : Finset (Discrete α)) ↦ Sigma.desc fun (x_1 : ↥x) ↦ s.ι.app (↑x_1 : Discrete α),
              naturality := ⋯ } })

Tactic:
apply colimit.hom_ext

Premises used: CategoryTheory.Limits.colimit.hom_ext