-- Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
α : Type w
inst_1 : HasFiniteProducts.{v, u} C
inst_2 : HasLimitsOfShape.{w, w, v, u} (Finset (Discrete α))ᵒᵖ C
F : Functor.{w, v, w, u} (Discrete α) C
s : Cone F
m :
  s.pt ⟶
    Cone.pt.{w, v, w, u} (J := Discrete α) (F := F)
      { pt := limit (liftToFinsetObj F),
        π :=
          Discrete.natTrans fun (j : Discrete α) ↦
            limit.π (liftToFinsetObj F) (op {j}) ≫
              Pi.π (fun (x : ↥(unop (op {j}))) ↦ F.obj (↑x : Discrete α))
                (Subtype.mk (p := fun (x : Discrete α) ↦ Membership.mem (γ := Finset (Discrete α)) {j} x) j ⋯) }
h :
  ∀ (j : Discrete α),
    m ≫
        NatTrans.app
          (Cone.π
            { pt := limit (liftToFinsetObj F),
              π :=
                Discrete.natTrans fun (j : Discrete α) ↦
                  limit.π (liftToFinsetObj F) (op {j}) ≫
                    Pi.π (fun (x : ↥(unop (op {j}))) ↦ F.obj (↑x : Discrete α))
                      (Subtype.mk (p := fun (x : Discrete α) ↦ Membership.mem (γ := Finset (Discrete α)) {j} x) j ⋯) })
          j =
      s.π.app j
t : (Finset (Discrete α))ᵒᵖ
w :
  ∀ (j : Discrete ↥(unop t)),
    (m ≫
          limit.π
            { obj := fun (s : (Finset (Discrete α))ᵒᵖ) ↦ piObj.{w, v, u} fun (x : ↥(unop s)) ↦ F.obj (↑x : Discrete α),
              map := fun {Y x : (Finset (Discrete α))ᵒᵖ} (h : Y ⟶ x) ↦
                Pi.lift fun (y : ↥(unop x)) ↦
                  Pi.π (fun (x : ↥(unop Y)) ↦ F.obj (↑x : Discrete α))
                    (Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ unop Y) (↑y : Discrete α) ⋯),
              map_id := ⋯, map_comp := ⋯ : Functor.{w, v, w, u} (Finset (Discrete α))ᵒᵖ C }
            t) ≫
        limit.π (Discrete.functor fun (x : ↥(unop t)) ↦ F.obj (↑x : Discrete α)) j =
      CategoryStruct.comp (Y :=
        limit.{w, w, v, u} (J := Discrete ↥(unop t)) (Discrete.functor fun (x : ↥(unop t)) ↦ F.obj (↑x : Discrete α)))
        (CategoryStruct.comp (Y :=
          limit.{w, w, v, u} (J := (Finset (Discrete α))ᵒᵖ)
            { obj := fun (s : (Finset (Discrete α))ᵒᵖ) ↦ piObj.{w, v, u} fun (x : ↥(unop s)) ↦ F.obj (↑x : Discrete α),
              map := fun {Y x : (Finset (Discrete α))ᵒᵖ} (h : Y ⟶ x) ↦
                Pi.lift fun (y : ↥(unop x)) ↦
                  Pi.π (fun (x : ↥(unop Y)) ↦ F.obj (↑x : Discrete α))
                    (Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ unop Y) (↑y : Discrete α) ⋯),
              map_id := ⋯, map_comp := ⋯ })
          (limit.lift
              {
                obj := fun (s : (Finset (Discrete α))ᵒᵖ) ↦
                  piObj.{w, v, u} fun (x : ↥(unop s)) ↦ F.obj (↑x : Discrete α),
                map := fun {Y x : (Finset (Discrete α))ᵒᵖ} (h : Y ⟶ x) ↦
                  Pi.lift fun (y : ↥(unop x)) ↦
                    Pi.π (fun (x : ↥(unop Y)) ↦ F.obj (↑x : Discrete α))
                      (Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ unop Y) (↑y : Discrete α) ⋯),
                map_id := ⋯, map_comp := ⋯ }
              { pt := s.pt,
                π :=
                  {
                    app := fun (x : (Finset (Discrete α))ᵒᵖ) ↦
                      Pi.lift fun (x_1 : ↥(unop x)) ↦ s.π.app (↑x_1 : Discrete α),
                    naturality := ⋯ } } :
            Cone.pt.{w, v, w, u} (J := (Finset (Discrete α))ᵒᵖ) (F :=
                {
                  obj := fun (s : (Finset (Discrete α))ᵒᵖ) ↦
                    piObj.{w, v, u} fun (x : ↥(unop s)) ↦ F.obj (↑x : Discrete α),
                  map := fun {Y x : (Finset (Discrete α))ᵒᵖ} (h : Y ⟶ x) ↦
                    Pi.lift fun (y : ↥(unop x)) ↦
                      Pi.π (fun (x : ↥(unop Y)) ↦ F.obj (↑x : Discrete α))
                        (Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ unop Y) (↑y : Discrete α) ⋯),
                  map_id := ⋯, map_comp := ⋯ : Functor.{w, v, w, u} (Finset (Discrete α))ᵒᵖ C })
                { pt := s.pt,
                  π :=
                    {
                      app := fun (x : (Finset (Discrete α))ᵒᵖ) ↦
                        Pi.lift fun (x_1 : ↥(unop x)) ↦ s.π.app (↑x_1 : Discrete α),
                      naturality := ⋯ :
                      NatTrans.{w, v, w, u} (C := (Finset (Discrete α))ᵒᵖ)
                        (Functor.obj (Functor.const (Finset (Discrete α))ᵒᵖ) s.pt)
                        {
                          obj := fun (s : (Finset (Discrete α))ᵒᵖ) ↦
                            piObj.{w, v, u} fun (x : ↥(unop s)) ↦ F.obj (↑x : Discrete α),
                          map := fun {Y x : (Finset (Discrete α))ᵒᵖ} (h : Y ⟶ x) ↦
                            Pi.lift fun (y : ↥(unop x)) ↦
                              Pi.π (fun (x : ↥(unop Y)) ↦ F.obj (↑x : Discrete α))
                                (Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ unop Y) (↑y : Discrete α) ⋯),
                          map_id := ⋯, map_comp := ⋯ : Functor.{w, v, w, u} (Finset (Discrete α))ᵒᵖ C } } :
                  Cone.{w, v, w, u} (J := (Finset (Discrete α))ᵒᵖ) (C := C)
                    {
                      obj := fun (s : (Finset (Discrete α))ᵒᵖ) ↦
                        piObj.{w, v, u} fun (x : ↥(unop s)) ↦ F.obj (↑x : Discrete α),
                      map := fun {Y x : (Finset (Discrete α))ᵒᵖ} (h : Y ⟶ x) ↦
                        Pi.lift fun (y : ↥(unop x)) ↦
                          Pi.π (fun (x : ↥(unop Y)) ↦ F.obj (↑x : Discrete α))
                            (Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ unop Y) (↑y : Discrete α) ⋯),
                      map_id := ⋯, map_comp := ⋯ : Functor.{w, v, w, u} (Finset (Discrete α))ᵒᵖ C } } ⟶
              limit.{w, w, v, u} (J := (Finset (Discrete α))ᵒᵖ)
                {
                  obj := fun (s : (Finset (Discrete α))ᵒᵖ) ↦
                    piObj.{w, v, u} fun (x : ↥(unop s)) ↦ F.obj (↑x : Discrete α),
                  map := fun {Y x : (Finset (Discrete α))ᵒᵖ} (h : Y ⟶ x) ↦
                    Pi.lift fun (y : ↥(unop x)) ↦
                      Pi.π (fun (x : ↥(unop Y)) ↦ F.obj (↑x : Discrete α))
                        (Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ unop Y) (↑y : Discrete α) ⋯),
                  map_id := ⋯, map_comp := ⋯ })
          (limit.π
              {
                obj := fun (s : (Finset (Discrete α))ᵒᵖ) ↦
                  piObj.{w, v, u} fun (x : ↥(unop s)) ↦ F.obj (↑x : Discrete α),
                map := fun {Y x : (Finset (Discrete α))ᵒᵖ} (h : Y ⟶ x) ↦
                  Pi.lift fun (y : ↥(unop x)) ↦
                    Pi.π (fun (x : ↥(unop Y)) ↦ F.obj (↑x : Discrete α))
                      (Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ unop Y) (↑y : Discrete α) ⋯),
                map_id := ⋯, map_comp := ⋯ }
              t :
            Quiver.Hom.{v, u} (V := C)
              (limit.{w, w, v, u} (J := (Finset (Discrete α))ᵒᵖ)
                {
                  obj := fun (s : (Finset (Discrete α))ᵒᵖ) ↦
                    piObj.{w, v, u} fun (x : ↥(unop s)) ↦ F.obj (↑x : Discrete α),
                  map := fun {Y x : (Finset (Discrete α))ᵒᵖ} (h : Y ⟶ x) ↦
                    Pi.lift fun (y : ↥(unop x)) ↦
                      Pi.π (fun (x : ↥(unop Y)) ↦ F.obj (↑x : Discrete α))
                        (Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ unop Y) (↑y : Discrete α) ⋯),
                  map_id := ⋯, map_comp := ⋯ })
              (Functor.obj.{w, v, w, u}
                {
                  obj := fun (s : (Finset (Discrete α))ᵒᵖ) ↦
                    piObj.{w, v, u} fun (x : ↥(unop s)) ↦ F.obj (↑x : Discrete α),
                  map := fun {Y x : (Finset (Discrete α))ᵒᵖ} (h : Y ⟶ x) ↦
                    Pi.lift fun (y : ↥(unop x)) ↦
                      Pi.π (fun (x : ↥(unop Y)) ↦ F.obj (↑x : Discrete α))
                        (Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ unop Y) (↑y : Discrete α) ⋯),
                  map_id := ⋯, map_comp := ⋯ }
                t)))
        (limit.π (Discrete.functor fun (x : ↥(unop t)) ↦ F.obj (↑x : Discrete α)) j)
⊢ m ≫
      limit.π
        { obj := fun (s : (Finset (Discrete α))ᵒᵖ) ↦ piObj.{w, v, u} fun (x : ↥(unop s)) ↦ F.obj (↑x : Discrete α),
          map := fun {Y x : (Finset (Discrete α))ᵒᵖ} (h : Y ⟶ x) ↦
            Pi.lift fun (y : ↥(unop x)) ↦
              Pi.π (fun (x : ↥(unop Y)) ↦ F.obj (↑x : Discrete α))
                (Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ unop Y) (↑y : Discrete α) ⋯),
          map_id := ⋯, map_comp := ⋯ : Functor.{w, v, w, u} (Finset (Discrete α))ᵒᵖ C }
        t =
    CategoryStruct.comp (Y :=
      limit.{w, w, v, u} (J := (Finset (Discrete α))ᵒᵖ)
        { obj := fun (s : (Finset (Discrete α))ᵒᵖ) ↦ piObj.{w, v, u} fun (x : ↥(unop s)) ↦ F.obj (↑x : Discrete α),
          map := fun {Y x : (Finset (Discrete α))ᵒᵖ} (h : Y ⟶ x) ↦
            Pi.lift fun (y : ↥(unop x)) ↦
              Pi.π (fun (x : ↥(unop Y)) ↦ F.obj (↑x : Discrete α))
                (Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ unop Y) (↑y : Discrete α) ⋯),
          map_id := ⋯, map_comp := ⋯ })
      (limit.lift
          { obj := fun (s : (Finset (Discrete α))ᵒᵖ) ↦ piObj.{w, v, u} fun (x : ↥(unop s)) ↦ F.obj (↑x : Discrete α),
            map := fun {Y x : (Finset (Discrete α))ᵒᵖ} (h : Y ⟶ x) ↦
              Pi.lift fun (y : ↥(unop x)) ↦
                Pi.π (fun (x : ↥(unop Y)) ↦ F.obj (↑x : Discrete α))
                  (Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ unop Y) (↑y : Discrete α) ⋯),
            map_id := ⋯, map_comp := ⋯ }
          { pt := s.pt,
            π :=
              { app := fun (x : (Finset (Discrete α))ᵒᵖ) ↦ Pi.lift fun (x_1 : ↥(unop x)) ↦ s.π.app (↑x_1 : Discrete α),
                naturality := ⋯ } } :
        Cone.pt.{w, v, w, u} (J := (Finset (Discrete α))ᵒᵖ) (F :=
            { obj := fun (s : (Finset (Discrete α))ᵒᵖ) ↦ piObj.{w, v, u} fun (x : ↥(unop s)) ↦ F.obj (↑x : Discrete α),
              map := fun {Y x : (Finset (Discrete α))ᵒᵖ} (h : Y ⟶ x) ↦
                Pi.lift fun (y : ↥(unop x)) ↦
                  Pi.π (fun (x : ↥(unop Y)) ↦ F.obj (↑x : Discrete α))
                    (Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ unop Y) (↑y : Discrete α) ⋯),
              map_id := ⋯, map_comp := ⋯ : Functor.{w, v, w, u} (Finset (Discrete α))ᵒᵖ C })
            { pt := s.pt,
              π :=
                {
                  app := fun (x : (Finset (Discrete α))ᵒᵖ) ↦
                    Pi.lift fun (x_1 : ↥(unop x)) ↦ s.π.app (↑x_1 : Discrete α),
                  naturality := ⋯ :
                  NatTrans.{w, v, w, u} (C := (Finset (Discrete α))ᵒᵖ)
                    (Functor.obj (Functor.const (Finset (Discrete α))ᵒᵖ) s.pt)
                    {
                      obj := fun (s : (Finset (Discrete α))ᵒᵖ) ↦
                        piObj.{w, v, u} fun (x : ↥(unop s)) ↦ F.obj (↑x : Discrete α),
                      map := fun {Y x : (Finset (Discrete α))ᵒᵖ} (h : Y ⟶ x) ↦
                        Pi.lift fun (y : ↥(unop x)) ↦
                          Pi.π (fun (x : ↥(unop Y)) ↦ F.obj (↑x : Discrete α))
                            (Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ unop Y) (↑y : Discrete α) ⋯),
                      map_id := ⋯, map_comp := ⋯ : Functor.{w, v, w, u} (Finset (Discrete α))ᵒᵖ C } } :
              Cone.{w, v, w, u} (J := (Finset (Discrete α))ᵒᵖ) (C := C)
                {
                  obj := fun (s : (Finset (Discrete α))ᵒᵖ) ↦
                    piObj.{w, v, u} fun (x : ↥(unop s)) ↦ F.obj (↑x : Discrete α),
                  map := fun {Y x : (Finset (Discrete α))ᵒᵖ} (h : Y ⟶ x) ↦
                    Pi.lift fun (y : ↥(unop x)) ↦
                      Pi.π (fun (x : ↥(unop Y)) ↦ F.obj (↑x : Discrete α))
                        (Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ unop Y) (↑y : Discrete α) ⋯),
                  map_id := ⋯, map_comp := ⋯ : Functor.{w, v, w, u} (Finset (Discrete α))ᵒᵖ C } } ⟶
          limit.{w, w, v, u} (J := (Finset (Discrete α))ᵒᵖ)
            { obj := fun (s : (Finset (Discrete α))ᵒᵖ) ↦ piObj.{w, v, u} fun (x : ↥(unop s)) ↦ F.obj (↑x : Discrete α),
              map := fun {Y x : (Finset (Discrete α))ᵒᵖ} (h : Y ⟶ x) ↦
                Pi.lift fun (y : ↥(unop x)) ↦
                  Pi.π (fun (x : ↥(unop Y)) ↦ F.obj (↑x : Discrete α))
                    (Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ unop Y) (↑y : Discrete α) ⋯),
              map_id := ⋯, map_comp := ⋯ })
      (limit.π
          { obj := fun (s : (Finset (Discrete α))ᵒᵖ) ↦ piObj.{w, v, u} fun (x : ↥(unop s)) ↦ F.obj (↑x : Discrete α),
            map := fun {Y x : (Finset (Discrete α))ᵒᵖ} (h : Y ⟶ x) ↦
              Pi.lift fun (y : ↥(unop x)) ↦
                Pi.π (fun (x : ↥(unop Y)) ↦ F.obj (↑x : Discrete α))
                  (Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ unop Y) (↑y : Discrete α) ⋯),
            map_id := ⋯, map_comp := ⋯ }
          t :
        Quiver.Hom.{v, u} (V := C)
          (limit.{w, w, v, u} (J := (Finset (Discrete α))ᵒᵖ)
            { obj := fun (s : (Finset (Discrete α))ᵒᵖ) ↦ piObj.{w, v, u} fun (x : ↥(unop s)) ↦ F.obj (↑x : Discrete α),
              map := fun {Y x : (Finset (Discrete α))ᵒᵖ} (h : Y ⟶ x) ↦
                Pi.lift fun (y : ↥(unop x)) ↦
                  Pi.π (fun (x : ↥(unop Y)) ↦ F.obj (↑x : Discrete α))
                    (Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ unop Y) (↑y : Discrete α) ⋯),
              map_id := ⋯, map_comp := ⋯ })
          (Functor.obj.{w, v, w, u}
            { obj := fun (s : (Finset (Discrete α))ᵒᵖ) ↦ piObj.{w, v, u} fun (x : ↥(unop s)) ↦ F.obj (↑x : Discrete α),
              map := fun {Y x : (Finset (Discrete α))ᵒᵖ} (h : Y ⟶ x) ↦
                Pi.lift fun (y : ↥(unop x)) ↦
                  Pi.π (fun (x : ↥(unop Y)) ↦ F.obj (↑x : Discrete α))
                    (Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ unop Y) (↑y : Discrete α) ⋯),
              map_id := ⋯, map_comp := ⋯ }
            t))

Tactic:
apply limit.hom_ext

Premises used: CategoryTheory.Limits.limit.hom_ext