-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Filtered (goal)
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 α))ᵒᵖ
j : Discrete α
hj : j ∈ unop t
e_1 :
  (s.pt ⟶
      Functor.obj.{w, v, w, u} (Discrete.functor fun (x : ↥(unop t)) ↦ F.obj (↑x : Discrete α))
        { as := Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ unop t) j hj : Discrete ↥(unop t) }) =
    (s.pt ⟶ F.obj 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) ≫
      limit.π (Discrete.functor fun (x : ↥(unop t)) ↦ F.obj (↑x : Discrete α))
        { as := Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ unop t) j hj : Discrete ↥(unop t) } =
    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
have h₁ : Eq (α := s.pt ⟶ F.obj 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 α) sorry),
            map_id := sorry, map_comp := sorry : Functor.{w, v, w, u} (Finset (Discrete α))ᵒᵖ C }
          t ≫
        limit.π (Discrete.functor fun (x : ↥(unop t)) ↦ F.obj (↑x : Discrete α))
          { as := Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ unop t) j hj } :
    s.pt ⟶ F.obj j)
  (m ≫
      limit.π (liftToFinsetObj F) t ≫
        Pi.π (fun (x : ↥(unop t)) ↦ F.obj (↑x : Discrete α)) (Subtype.mk (p := fun (x : Discrete α) ↦ x ∈ unop t) j sorry) :
    s.pt ⟶ F.obj j)
Tactic: simp [← limit.w (liftToFinsetObj F) ⟨⟨⟨Finset.singleton_subset_iff.2 hj⟩⟩⟩]