-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Products (goal)
Goal:
J_1 : Type w
C : Type u
inst : Category.{v, u} C
X_1 Y_1 Z B : C
J : Type w
F : Discrete J ⥤ Over.{v, u} B
c : Cone (widePullbackDiagramOfDiagramOver B F)
x x_1 : Discrete J
X Y : J
x_2 : { as := X : Discrete J } ⟶ { as := Y }
f : { as := X : Discrete J }.as = { as := Y }.as
⊢ Eq (α :=
    Functor.obj
        (Functor.obj (Functor.const (Discrete J))
          (mk (Y :=
            Functor.obj.{w, v, w, u} (C := WidePullbackShape J) (Functor.obj (Functor.const (WidePullbackShape J)) c.pt)
              none)
            (c.π.app none)))
        { as := X : Discrete J } ⟶
      F.obj { as := Y : Discrete J })
    (CategoryStruct.comp (Y :=
        Functor.obj
          (Functor.obj (Functor.const (Discrete J))
            (mk (Y :=
              Functor.obj.{w, v, w, u} (C := WidePullbackShape J)
                (Functor.obj (Functor.const (WidePullbackShape J)) c.pt) none)
              (c.π.app none)))
          { as := Y : Discrete J })
        (Functor.map
          (Functor.obj (Functor.const (Discrete J))
            (mk (Y :=
              Functor.obj.{w, v, w, u} (C := WidePullbackShape J)
                (Functor.obj (Functor.const (WidePullbackShape J)) c.pt) none)
              (c.π.app none)))
          { down := { down := f } })
        (match (motive :=
          (x : Discrete J) →
            Functor.obj
                (Functor.obj (Functor.const (Discrete J))
                  (mk (Y :=
                    Functor.obj.{w, v, w, u} (C := WidePullbackShape J)
                      (Functor.obj (Functor.const (WidePullbackShape J)) c.pt) none)
                    (c.π.app none)))
                x ⟶
              F.obj x)
          { as := Y : Discrete J } with
        | { as := j } => homMk (c.π.app (some j)) ⋯) :
      Functor.obj
          (Functor.obj (Functor.const (Discrete J))
            (mk (Y :=
              Functor.obj.{w, v, w, u} (C := WidePullbackShape J)
                (Functor.obj (Functor.const (WidePullbackShape J)) c.pt) none)
              (c.π.app none)))
          { as := X : Discrete J } ⟶
        F.obj { as := Y : Discrete J })
    ((match (motive :=
          (x : Discrete J) →
            Functor.obj
                (Functor.obj (Functor.const (Discrete J))
                  (mk (Y :=
                    Functor.obj.{w, v, w, u} (C := WidePullbackShape J)
                      (Functor.obj (Functor.const (WidePullbackShape J)) c.pt) none)
                    (c.π.app none)))
                x ⟶
              F.obj x)
          { as := X : Discrete J } with
        | { as := j } => homMk (c.π.app (some j)) ⋯) ≫
        F.map
          { down := { down := f : PLift ({ as := X : Discrete J }.as = { as := Y : Discrete J }.as) } :
            ULift.{w, 0} (PLift ({ as := X : Discrete J }.as = { as := Y : Discrete J }.as)) } :
      Functor.obj
          (Functor.obj (Functor.const (Discrete J))
            (mk (Y :=
              Functor.obj.{w, v, w, u} (C := WidePullbackShape J)
                (Functor.obj (Functor.const (WidePullbackShape J)) c.pt) none)
              (c.π.app none)))
          { as := X : Discrete J } ⟶
        F.obj { as := Y : Discrete J })
have dsimp : Eq (α := mk (Y := c.pt) (c.π.app none) ⟶ F.obj { as := Y : Discrete J })
  (CategoryStruct.comp (Y := mk (Y := c.pt) (c.π.app none)) (𝟙 (mk (Y := c.pt) (c.π.app none)))
      (homMk (c.π.app (some Y)) sorry) :
    mk (Y := c.pt) (c.π.app none) ⟶ F.obj { as := Y : Discrete J })
  (homMk (c.π.app (some X)) sorry ≫ F.map { down := { down := f : PLift (X = Y) } : ULift.{w, 0} (PLift (X = Y)) } :
    mk (Y := c.pt) (c.π.app none) ⟶ F.obj { as := Y : Discrete J })
Tactic: dsimp at f ⊢