-- 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 Y_1 Z B : C
J : Type w
F : Discrete J ⥤ Over.{v, u} B
c : Cone F
Y : WidePullbackShape J
val : J
f : some val ⟶ Y
⊢ 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) (some val))
      (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 })) (some val))
      (WidePullbackShape.Hom.rec (motive := fun (a a_1 : WidePullbackShape J) (x : a.Hom a_1) ↦
        (h : some val = 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) (some val) :
                  C)
                (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                    (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) Y :
                  C))
        (fun (X : WidePullbackShape J) (h : some val = X) ↦
          Eq.rec (motive := fun (x : WidePullbackShape J) (x_1 : some val = 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) (some val) :
                    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 = some val) ↦
              Eq.rec (motive := fun (x : WidePullbackShape J) (x_1 : some val = x) ↦
                (f : some val ⟶ x) →
                  (h : HEq f (β := WidePullbackShape.Hom (some val) (some val)) (𝟙 (some val) : some val ⟶ some val)) →
                    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) (some val) :
                        C)
                      (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                          (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) x :
                        C))
                (fun (f : some val ⟶ some val)
                    (h :
                      HEq f (β := WidePullbackShape.Hom (some val) (some val)) (𝟙 (some val) : some val ⟶ some val)) ↦
                  𝟙
                    (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                      (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) (some val)))
                ⋯ f)
            h)
        (fun (j : J) (h : some val = 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) ⋯ f)
            ⋯ f)
        f ⋯ ⋯ ⋯))
have some : ∀ (f : some val ⟶ none),
  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) none)
    (𝟙 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 })) none)
    (CategoryStruct.comp (Y :=
      Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
        (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) (some val))
      (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 })) (some val))
      (WidePullbackShape.Hom.rec (motive := fun (a a_1 : WidePullbackShape J) (x : a.Hom a_1) ↦
        (h : some val = a) →
          (h : none = 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) (some val) :
                  C)
                (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                    (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) none :
                  C))
        (fun (X : WidePullbackShape J) (h : some val = X) ↦
          Eq.rec (motive := fun (x : WidePullbackShape J) (x_1 : some val = x) ↦
            (h : none = 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) (some val) :
                    C)
                  (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                      (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) none :
                    C))
            (fun (h : none = some val) ↦
              Eq.rec (motive := fun (x : WidePullbackShape J) (x_1 : some val = x) ↦
                (f : some val ⟶ x) →
                  (h : HEq f (β := WidePullbackShape.Hom (some val) (some val)) (𝟙 (some val) : some val ⟶ some val)) →
                    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) (some val) :
                        C)
                      (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                          (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) x :
                        C))
                (fun (f : some val ⟶ some val)
                    (h :
                      HEq f (β := WidePullbackShape.Hom (some val) (some val)) (𝟙 (some val) : some val ⟶ some val)) ↦
                  𝟙
                    (Option.rec (motive := fun (x : WidePullbackShape J) ↦ C) B
                      (fun (val : J) ↦ (F.obj { as := val : Discrete J }).left) (some val)))
                sorry f)
            h)
        (fun (j : J) (h : some val = some j) ↦
          Eq.rec (motive := fun (x : WidePullbackShape J) (x_1 : some j = x) ↦
            (f : x ⟶ none) →
              (h : Eq.{w + 1} (α := WidePullbackShape J) none 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) none :
                      C))
            (fun (f : some j ⟶ none) (h : Eq.{w + 1} (α := WidePullbackShape J) none 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: cases Y
Cleared hypotheses: Y, f