-- 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 F
X Y : WidePullbackShape J
f : X ⟶ Y
⊢ Eq.{v + 1} (α :=
    Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape J)) c.pt.left) X ⟶
      (widePullbackDiagramOfDiagramOver B F).obj Y)
    (Functor.map (Functor.obj (Functor.const (WidePullbackShape J)) c.pt.left) f ≫
      Option.casesOn (motive := fun (x : WidePullbackShape J) ↦
        Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape J)) c.pt.left) x ⟶
          (widePullbackDiagramOfDiagramOver B F).obj x)
        Y c.pt.hom fun (j : J) ↦ Hom.left (c.π.app { as := j }))
    ((Option.casesOn (motive := fun (x : WidePullbackShape J) ↦
        Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape J)) c.pt.left) x ⟶
          (widePullbackDiagramOfDiagramOver B F).obj x)
        X c.pt.hom fun (j : J) ↦ Hom.left (c.π.app { as := j })) ≫
      (widePullbackDiagramOfDiagramOver B F).map f)
have dsimp : Eq.{v + 1} (α :=
  c.pt.left ⟶
    Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left)
      Y)
  (𝟙 c.pt.left ≫
    Option.rec (motive := fun (x : WidePullbackShape J) ↦
      c.pt.left ⟶
        Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
          (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) x)
      c.pt.hom (fun (val : J) ↦ Hom.left (c.π.app { as := val })) Y)
  (CategoryStruct.comp (Y :=
    Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left)
      X)
    (Option.rec (motive := fun (x : WidePullbackShape J) ↦
      c.pt.left ⟶
        Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
          (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) x)
      c.pt.hom (fun (val : J) ↦ Hom.left (c.π.app { as := val })) X)
    (WidePullbackShape.Hom.rec (motive := fun (a a_1 : WidePullbackShape J) (x : a.Hom a_1) ↦
      (h : X = a) →
        (h : Y = a_1) →
          (h : f ≍ x) →
            Quiver.Hom.{v, u} (V := C)
              (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                  (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) X :
                C)
              (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                  (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) Y :
                C))
      (fun (X_2 : WidePullbackShape J) (h : X = X_2) ↦
        Eq.rec (motive := fun (x : WidePullbackShape J) (x_1 : X = x) ↦
          (h : Y = x) →
            (h : HEq f (β := x.Hom x) (𝟙 x)) →
              Quiver.Hom.{v, u} (V := C)
                (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                    (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) X :
                  C)
                (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                    (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) Y :
                  C))
          (fun (h : Y = X) ↦
            Eq.rec (motive := fun (x : WidePullbackShape J) (x_1 : X = x) ↦
              (f : X ⟶ x) →
                (h : HEq f (β := X.Hom X) (𝟙 X)) →
                  Quiver.Hom.{v, u} (V := C)
                    (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                        (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) X :
                      C)
                    (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                        (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) x :
                      C))
              (fun (f : X ⟶ X) (h : HEq f (β := X.Hom X) (𝟙 X)) ↦
                𝟙
                  (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                    (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) X))
              sorry f)
          h)
      (fun (j : J) (h : X = some j) ↦
        Eq.rec (motive := fun (x : WidePullbackShape J) (x_1 : some j = x) ↦
          (f : x ⟶ Y) →
            (h : Y = none) →
              (h : f ≍ WidePullbackShape.Hom.term j) →
                Quiver.Hom.{v, u} (V := C)
                  (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                      (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) x :
                    C)
                  (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                      (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) Y :
                    C))
          (fun (f : some j ⟶ Y) (h : Y = none) ↦
            Eq.rec (motive := fun (x : WidePullbackShape J) (x_1 : none = x) ↦
              (f : some j ⟶ x) →
                (h : f ≍ WidePullbackShape.Hom.term j) →
                  (F.obj { as := j : Discrete J }).left ⟶
                    Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                      (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) x)
              (fun (f : some j ⟶ none) (h : f ≍ WidePullbackShape.Hom.term j) ↦ (F.obj { as := j }).hom) sorry f)
          sorry f)
      f sorry sorry sorry))
Tactic: dsimp