-- 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
I : Finset (Discrete α)
X Y : Functor.{w, v, w, u} (Discrete α) C
x : X ⟶ Y
⊢ Eq (α :=
    Functor.obj (liftToFinset C α ⋙ Functor.obj (evaluation (Finset (Discrete α))ᵒᵖ C) (op I)) X ⟶
      Functor.obj
        (Functor.comp (D := Functor.{w, v, w, u} (Discrete ↥I) C)
          (Functor.obj (Functor.whiskeringLeft (Discrete ↥I) (Discrete α) C)
            (Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)))
          lim)
        Y)
    (Functor.map (liftToFinset C α ⋙ Functor.obj (evaluation (Finset (Discrete α))ᵒᵖ C) (op I)) x ≫
      Iso.hom
        ((fun (x : Functor.{w, v, w, u} (Discrete α) C) ↦
            (HasLimit.isoOfNatIso
                (Discrete.natIso fun (x_1 : Discrete ↥(unop (op I))) ↦
                  Iso.refl
                    (Functor.obj.{w, v, w, u} (Discrete.functor fun (x_2 : ↥(unop (op I))) ↦ x.obj (↑x_2 : Discrete α))
                      x_1)) :
              limit.{w, w, v, u} (J := Discrete ↥(unop (op I)))
                  (Discrete.functor fun (x_1 : ↥(unop (op I))) ↦ x.obj (↑x_1 : Discrete α)) ≅
                limit (J := Discrete ↥(unop (op I)))
                  (Functor.obj
                    (Functor.obj (Functor.whiskeringLeft (Discrete ↥I) (Discrete α) C)
                      (Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)))
                    x)))
          Y))
    (Iso.hom
        ((fun (x : Functor.{w, v, w, u} (Discrete α) C) ↦
            (HasLimit.isoOfNatIso
                (Discrete.natIso fun (x_1 : Discrete ↥(unop (op I))) ↦
                  Iso.refl
                    (Functor.obj.{w, v, w, u} (Discrete.functor fun (x_2 : ↥(unop (op I))) ↦ x.obj (↑x_2 : Discrete α))
                      x_1)) :
              limit.{w, w, v, u} (J := Discrete ↥(unop (op I)))
                  (Discrete.functor fun (x_1 : ↥(unop (op I))) ↦ x.obj (↑x_1 : Discrete α)) ≅
                limit (J := Discrete ↥(unop (op I)))
                  (Functor.obj
                    (Functor.obj (Functor.whiskeringLeft (Discrete ↥I) (Discrete α) C)
                      (Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)))
                    x)))
          X) ≫
      Functor.map
        (Functor.comp (D := Functor.{w, v, w, u} (Discrete ↥I) C)
          (Functor.obj (Functor.whiskeringLeft (Discrete ↥I) (Discrete α) C)
            (Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)))
          lim)
        x)
have dsimp : Eq (α :=
  (piObj.{w, v, u} fun (x : ↥I) ↦ X.obj (↑x : Discrete α)) ⟶
    limit (J := Discrete ↥I) ((Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)) ⋙ Y))
  (CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ↥I) ↦ Y.obj (↑x : Discrete α))
    (Pi.map fun (x_1 : ↥I) ↦ x.app (↑x_1 : Discrete α))
    (Iso.hom (HasLimit.isoOfNatIso (Discrete.natIso fun (x : Discrete ↥I) ↦ Iso.refl (Y.obj (↑x.as : Discrete α))))))
  (CategoryStruct.comp (Y := limit (J := Discrete ↥I) ((Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)) ⋙ X))
    (Iso.hom (HasLimit.isoOfNatIso (Discrete.natIso fun (x : Discrete ↥I) ↦ Iso.refl (X.obj (↑x.as : Discrete α)))))
    (limMap (Functor.whiskerLeft (Discrete.functor fun (x : ↥I) ↦ (↑x : Discrete α)) x)))
Tactic: dsimp