-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
X Z : WidePushoutShape J
g : X ⟶ Z
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C)
      (Option.rec (motive := fun (x : WidePushoutShape J) ↦ C) B (fun (val : J) ↦ objs val) X : C)
      (Option.rec (motive := fun (x : WidePushoutShape J) ↦ C) B (fun (val : J) ↦ objs val) Z : C))
    (Hom.rec (motive := fun (a a_1 : WidePushoutShape J) (x : a.Hom a_1) ↦
        (h : X = a) →
          (h : Z = a_1) →
            (h : 𝟙 X ≫ g ≍ x) →
              Quiver.Hom.{v, u} (V := C)
                (Option.rec (motive := fun (x : WidePushoutShape J) ↦ C) B (fun (val : J) ↦ objs val) X : C)
                (Option.rec (motive := fun (x : WidePushoutShape J) ↦ C) B (fun (val : J) ↦ objs val) Z : C))
        (fun (X_1 : WidePushoutShape J) (h : X = X_1) ↦
          Eq.rec (motive := fun (x : WidePushoutShape J) (x_1 : X = x) ↦
            (h : Z = x) →
              (h : HEq (𝟙 X ≫ g) (β := x.Hom x) (𝟙 x)) →
                Quiver.Hom.{v, u} (V := C)
                  (Option.rec (motive := fun (x : WidePushoutShape J) ↦ C) B (fun (val : J) ↦ objs val) X : C)
                  (Option.rec (motive := fun (x : WidePushoutShape J) ↦ C) B (fun (val : J) ↦ objs val) Z : C))
            (fun (h : Z = X) ↦
              Eq.rec (motive := fun (x : WidePushoutShape 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 : WidePushoutShape J) ↦ C) B (fun (val : J) ↦ objs val) X : C)
                      (Option.rec (motive := fun (x : WidePushoutShape J) ↦ C) B (fun (val : J) ↦ objs val) x : C))
                (fun (f : X ⟶ X) (h : HEq f (β := X.Hom X) (𝟙 X)) ↦
                  𝟙 (Option.rec (motive := fun (x : WidePushoutShape J) ↦ C) B (fun (val : J) ↦ objs val) X))
                ⋯ (𝟙 X ≫ g))
            h)
        (fun (j : J) (h : X = none) ↦
          Eq.rec (motive := fun (x : WidePushoutShape J) (x_1 : none = x) ↦
            (f : x ⟶ Z) →
              (h : Z = some j) →
                (h : f ≍ Hom.init j) →
                  Quiver.Hom.{v, u} (V := C)
                    (Option.rec (motive := fun (x : WidePushoutShape J) ↦ C) B (fun (val : J) ↦ objs val) x : C)
                    (Option.rec (motive := fun (x : WidePushoutShape J) ↦ C) B (fun (val : J) ↦ objs val) Z : C))
            (fun (f : none ⟶ Z) (h : Z = some j) ↦
              Eq.rec (motive := fun (x : WidePushoutShape J) (x_1 : some j = x) ↦
                (f : none ⟶ x) →
                  (h : f ≍ Hom.init j) →
                    B ⟶ Option.rec (motive := fun (x : WidePushoutShape J) ↦ C) B (fun (val : J) ↦ objs val) x)
                (fun (f : none ⟶ some j) (h : f ≍ Hom.init j) ↦ arrows j) ⋯ f)
            ⋯ (𝟙 X ≫ g))
        (𝟙 X ≫ g) ⋯ ⋯ ⋯ :
      Quiver.Hom.{v, u} (V := C)
        (Option.rec (motive := fun (x : WidePushoutShape J) ↦ C) B (fun (val : J) ↦ objs val) X : C)
        (Option.rec (motive := fun (x : WidePushoutShape J) ↦ C) B (fun (val : J) ↦ objs val) Z : C))
    (Hom.rec (motive := fun (a a_1 : WidePushoutShape J) (x : a.Hom a_1) ↦
        (h : X = a) →
          (h : Z = a_1) →
            (h : g ≍ x) →
              Quiver.Hom.{v, u} (V := C)
                (Option.rec (motive := fun (x : WidePushoutShape J) ↦ C) B (fun (val : J) ↦ objs val) X : C)
                (Option.rec (motive := fun (x : WidePushoutShape J) ↦ C) B (fun (val : J) ↦ objs val) Z : C))
        (fun (X_1 : WidePushoutShape J) (h : X = X_1) ↦
          Eq.rec (motive := fun (x : WidePushoutShape J) (x_1 : X = x) ↦
            (h : Z = x) →
              (h : HEq g (β := x.Hom x) (𝟙 x)) →
                Quiver.Hom.{v, u} (V := C)
                  (Option.rec (motive := fun (x : WidePushoutShape J) ↦ C) B (fun (val : J) ↦ objs val) X : C)
                  (Option.rec (motive := fun (x : WidePushoutShape J) ↦ C) B (fun (val : J) ↦ objs val) Z : C))
            (fun (h : Z = X) ↦
              Eq.rec (motive := fun (x : WidePushoutShape 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 : WidePushoutShape J) ↦ C) B (fun (val : J) ↦ objs val) X : C)
                      (Option.rec (motive := fun (x : WidePushoutShape J) ↦ C) B (fun (val : J) ↦ objs val) x : C))
                (fun (f : X ⟶ X) (h : HEq f (β := X.Hom X) (𝟙 X)) ↦
                  𝟙 (Option.rec (motive := fun (x : WidePushoutShape J) ↦ C) B (fun (val : J) ↦ objs val) X))
                ⋯ g)
            h)
        (fun (j : J) (h : X = none) ↦
          Eq.rec (motive := fun (x : WidePushoutShape J) (x_1 : none = x) ↦
            (f : x ⟶ Z) →
              (h : Z = some j) →
                (h : f ≍ Hom.init j) →
                  Quiver.Hom.{v, u} (V := C)
                    (Option.rec (motive := fun (x : WidePushoutShape J) ↦ C) B (fun (val : J) ↦ objs val) x : C)
                    (Option.rec (motive := fun (x : WidePushoutShape J) ↦ C) B (fun (val : J) ↦ objs val) Z : C))
            (fun (f : none ⟶ Z) (h : Z = some j) ↦
              Eq.rec (motive := fun (x : WidePushoutShape J) (x_1 : some j = x) ↦
                (f : none ⟶ x) →
                  (h : f ≍ Hom.init j) →
                    B ⟶ Option.rec (motive := fun (x : WidePushoutShape J) ↦ C) B (fun (val : J) ↦ objs val) x)
                (fun (f : none ⟶ some j) (h : f ≍ Hom.init j) ↦ arrows j) ⋯ f)
            ⋯ g)
        g ⋯ ⋯ ⋯ :
      Quiver.Hom.{v, u} (V := C)
        (Option.rec (motive := fun (x : WidePushoutShape J) ↦ C) B (fun (val : J) ↦ objs val) X : C)
        (Option.rec (motive := fun (x : WidePushoutShape J) ↦ C) B (fun (val : J) ↦ objs val) Z : C))

Tactic:
congr