-- 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 Y Z : WidePushoutShape J
f : X ⟶ Y
g : Y ⟶ Z
id :
  ∀ (g : X ⟶ Z),
    Eq.{v + 1} (α :=
      Quiver.Hom.{v, u} (V := C) (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)
        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Z B objs : C))
      (@Hom.casesOn _
          (fun (a a_1 : WidePushoutShape J) (x : a.Hom a_1) ↦
            (h : X = a) →
              (h : Z = a_1) →
                (h : HEq (α := X ⟶ Z) (Hom.id X ≫ g) x) →
                  Quiver.Hom.{v, u} (V := C) (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)
                    (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Z B objs : C))
          X _ (Hom.id X ≫ g)
          (fun (X_1 : WidePushoutShape J) (h : X = X_1) ↦
            Eq.ndrec (motive := fun (X_2 : WidePushoutShape J) ↦
              (h : Z = X_2) →
                (h : HEq (α := X ⟶ Z) (Hom.id X ≫ g) (Hom.id X_2)) →
                  Quiver.Hom.{v, u} (V := C) (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)
                    (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Z B objs : C))
              (fun (h : Z = X) ↦
                Eq.ndrec (motive := fun {Y : WidePushoutShape J} ↦
                  (f : X ⟶ Y) →
                    (h : f ≍ Hom.id X) →
                      Quiver.Hom.{v, u} (V := C)
                        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)
                        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Y B objs : C))
                  (fun (f : X ⟶ X) (h : f ≍ Hom.id X) ↦
                    𝟙 (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs))
                  ⋯ (Hom.id X ≫ g))
              h)
          (fun (j : J) (h : X = none) ↦
            Eq.ndrec (motive := fun {X : WidePushoutShape J} ↦
              (f : X ⟶ Z) →
                (h : Z = some j) →
                  (h : f ≍ Hom.init j) →
                    Quiver.Hom.{v, u} (V := C)
                      (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)
                      (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Z B objs : C))
              (fun (f : none ⟶ Z) (h : Z = some j) ↦
                Eq.ndrec (motive := fun {Y : WidePushoutShape J} ↦
                  (f : none ⟶ Y) →
                    (h : f ≍ Hom.init j) →
                      Quiver.Hom.{v, u} (V := C)
                        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) none B objs : C)
                        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Y B objs : C))
                  (fun (f : none ⟶ some j) (h : f ≍ Hom.init j) ↦ arrows j) ⋯ f)
              ⋯ (Hom.id X ≫ g))
          ⋯ ⋯ ⋯ :
        Quiver.Hom.{v, u} (V := C) (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)
          (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Z B objs : C))
      (CategoryStruct.comp (Y := Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs)
          (Hom.casesOn (motive := fun (a a_1 : WidePushoutShape J) (x : a.Hom a_1) ↦
            (h : X = a) →
              (h : X = a_1) →
                (h : Hom.id X ≍ x) →
                  Quiver.Hom.{v, u} (V := C) (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)
                    (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C))
            (Hom.id X)
            (fun (X_1 : WidePushoutShape J) (h : X = X_1) ↦
              Eq.ndrec (motive := fun (X_2 : WidePushoutShape J) ↦
                (h : X = X_2) →
                  (h : Hom.id X ≍ Hom.id X_2) →
                    Quiver.Hom.{v, u} (V := C)
                      (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)
                      (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C))
                (fun (h : X = X) ↦
                  Eq.ndrec (motive := fun {Y : WidePushoutShape J} ↦
                    (f : X ⟶ Y) →
                      (h : f ≍ Hom.id X) →
                        Quiver.Hom.{v, u} (V := C)
                          (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)
                          (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Y B objs : C))
                    (fun (f : X ⟶ X) (h : f ≍ Hom.id X) ↦
                      𝟙 (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs))
                    ⋯ (Hom.id X))
                h)
            (fun (j : J) (h : X = none) ↦
              Eq.ndrec (motive := fun {X_1 : WidePushoutShape J} ↦
                (f : X_1 ⟶ X) →
                  (h : X = some j) →
                    (h : f ≍ Hom.init j) →
                      Quiver.Hom.{v, u} (V := C)
                        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X_1 B objs : C)
                        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C))
                (fun (f : none ⟶ X) (h : X = some j) ↦
                  Eq.ndrec (motive := fun {Y : WidePushoutShape J} ↦
                    (f : none ⟶ Y) →
                      (h : f ≍ Hom.init j) →
                        Quiver.Hom.{v, u} (V := C)
                          (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) none B objs : C)
                          (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Y B objs : C))
                    (fun (f : none ⟶ some j) (h : f ≍ Hom.init j) ↦ arrows j) ⋯ f)
                ⋯ (Hom.id X))
            ⋯ ⋯ ⋯)
          (Hom.casesOn (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.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)
                    (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Z B objs : C))
            g
            (fun (X_1 : WidePushoutShape J) (h : X = X_1) ↦
              Eq.ndrec (motive := fun (X_2 : WidePushoutShape J) ↦
                (h : Z = X_2) →
                  (h : g ≍ Hom.id X_2) →
                    Quiver.Hom.{v, u} (V := C)
                      (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)
                      (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Z B objs : C))
                (fun (h : Z = X) ↦
                  Eq.ndrec (motive := fun {Y : WidePushoutShape J} ↦
                    (f : X ⟶ Y) →
                      (h : f ≍ Hom.id X) →
                        Quiver.Hom.{v, u} (V := C)
                          (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)
                          (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Y B objs : C))
                    (fun (f : X ⟶ X) (h : f ≍ Hom.id X) ↦
                      𝟙 (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs))
                    ⋯ g)
                h)
            (fun (j : J) (h : X = none) ↦
              Eq.ndrec (motive := fun {X : WidePushoutShape J} ↦
                (f : X ⟶ Z) →
                  (h : Z = some j) →
                    (h : f ≍ Hom.init j) →
                      Quiver.Hom.{v, u} (V := C)
                        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)
                        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Z B objs : C))
                (fun (f : none ⟶ Z) (h : Z = some j) ↦
                  Eq.ndrec (motive := fun {Y : WidePushoutShape J} ↦
                    (f : none ⟶ Y) →
                      (h : f ≍ Hom.init j) →
                        Quiver.Hom.{v, u} (V := C)
                          (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) none B objs : C)
                          (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Y B objs : C))
                    (fun (f : none ⟶ some j) (h : f ≍ Hom.init j) ↦ arrows j) ⋯ f)
                ⋯ g)
            ⋯ ⋯ ⋯) :
        Quiver.Hom.{v, u} (V := C) (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)
          (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Z B objs : C))
init :
  ∀ (j : J) (g : some j ⟶ Z),
    Eq.{v + 1} (α :=
      Quiver.Hom.{v, u} (V := C) (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) none B objs : C)
        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Z B objs : C))
      (@Hom.casesOn _
          (fun (a a_1 : WidePushoutShape J) (x : a.Hom a_1) ↦
            (h : none = a) →
              (h : Z = a_1) →
                (h : HEq (α := none ⟶ Z) (Hom.init j ≫ g) x) →
                  Quiver.Hom.{v, u} (V := C)
                    (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) none B objs : C)
                    (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Z B objs : C))
          none _ (Hom.init j ≫ g)
          (fun (X : WidePushoutShape J) (h : none = X) ↦
            Eq.ndrec (motive := fun (X : WidePushoutShape J) ↦
              (h : Z = X) →
                (h : HEq (α := none ⟶ Z) (Hom.init j ≫ g) (Hom.id X)) →
                  Quiver.Hom.{v, u} (V := C)
                    (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) none B objs : C)
                    (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Z B objs : C))
              (fun (h : Z = none) ↦
                Eq.ndrec (motive := fun {Y : WidePushoutShape J} ↦
                  (f : none ⟶ Y) →
                    (h : HEq f (β := Hom (J := J) none none) (Hom.id none)) →
                      Quiver.Hom.{v, u} (V := C)
                        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) none B objs : C)
                        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Y B objs : C))
                  (fun (f : Quiver.Hom (V := WidePushoutShape J) none none)
                      (h : HEq f (β := Hom (J := J) none none) (Hom.id none)) ↦
                    𝟙 (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) none B objs))
                  ⋯ (Hom.init j ≫ g))
              h)
          (fun (j_1 : J) (h : Eq.{w + 1} (α := WidePushoutShape J) none none) ↦
            Eq.ndrec (motive := fun {X : WidePushoutShape J} ↦
              (f : X ⟶ Z) →
                (h : Z = some j_1) →
                  (h : f ≍ Hom.init j_1) →
                    Quiver.Hom.{v, u} (V := C)
                      (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)
                      (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Z B objs : C))
              (fun (f : none ⟶ Z) (h : Z = some j_1) ↦
                Eq.ndrec (motive := fun {Y : WidePushoutShape J} ↦
                  (f : none ⟶ Y) →
                    (h : f ≍ Hom.init j_1) →
                      Quiver.Hom.{v, u} (V := C)
                        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) none B objs : C)
                        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Y B objs : C))
                  (fun (f : none ⟶ some j_1) (h : f ≍ Hom.init j_1) ↦ arrows j_1) ⋯ f)
              ⋯ (Hom.init j ≫ g))
          ⋯ ⋯ ⋯ :
        Quiver.Hom.{v, u} (V := C) (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) none B objs : C)
          (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Z B objs : C))
      (CategoryStruct.comp (Y := Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) (some j) B objs)
          (Hom.casesOn (motive := fun (a a_1 : WidePushoutShape J) (x : a.Hom a_1) ↦
            (h : none = a) →
              (h : some j = a_1) →
                (h : Hom.init j ≍ x) →
                  Quiver.Hom.{v, u} (V := C)
                    (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) none B objs : C)
                    (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) (some j) B objs : C))
            (Hom.init j)
            (fun (X : WidePushoutShape J) (h : none = X) ↦
              Eq.ndrec (motive := fun (X : WidePushoutShape J) ↦
                (h : some j = X) →
                  (h : Hom.init j ≍ Hom.id X) →
                    Quiver.Hom.{v, u} (V := C)
                      (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) none B objs : C)
                      (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) (some j) B objs : C))
                (fun (h : some j = none) ↦
                  Eq.ndrec (motive := fun {Y : WidePushoutShape J} ↦
                    (f : none ⟶ Y) →
                      (h : HEq f (β := Hom (J := J) none none) (Hom.id none)) →
                        Quiver.Hom.{v, u} (V := C)
                          (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) none B objs : C)
                          (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Y B objs : C))
                    (fun (f : Quiver.Hom (V := WidePushoutShape J) none none)
                        (h : HEq f (β := Hom (J := J) none none) (Hom.id none)) ↦
                      𝟙 (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) none B objs))
                    ⋯ (Hom.init j))
                h)
            (fun (j_1 : J) (h : Eq.{w + 1} (α := WidePushoutShape J) none none) ↦
              Eq.ndrec (motive := fun {X : WidePushoutShape J} ↦
                (f : X ⟶ some j) →
                  (h : some j = some j_1) →
                    (h : f ≍ Hom.init j_1) →
                      Quiver.Hom.{v, u} (V := C)
                        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)
                        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) (some j) B objs : C))
                (fun (f : none ⟶ some j) (h : some j = some j_1) ↦
                  Eq.ndrec (motive := fun {Y : WidePushoutShape J} ↦
                    (f : none ⟶ Y) →
                      (h : f ≍ Hom.init j_1) →
                        Quiver.Hom.{v, u} (V := C)
                          (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) none B objs : C)
                          (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Y B objs : C))
                    (fun (f : none ⟶ some j_1) (h : f ≍ Hom.init j_1) ↦ arrows j_1) ⋯ f)
                ⋯ (Hom.init j))
            ⋯ ⋯ ⋯)
          (Hom.casesOn (motive := fun (a a_1 : WidePushoutShape J) (x : a.Hom a_1) ↦
            (h : some j = a) →
              (h : Z = a_1) →
                (h : g ≍ x) →
                  Quiver.Hom.{v, u} (V := C)
                    (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) (some j) B objs : C)
                    (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Z B objs : C))
            g
            (fun (X : WidePushoutShape J) (h : some j = X) ↦
              Eq.ndrec (motive := fun (X : WidePushoutShape J) ↦
                (h : Z = X) →
                  (h : g ≍ Hom.id X) →
                    Quiver.Hom.{v, u} (V := C)
                      (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) (some j) B objs : C)
                      (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Z B objs : C))
                (fun (h : Z = some j) ↦
                  Eq.ndrec (motive := fun {Y : WidePushoutShape J} ↦
                    (f : some j ⟶ Y) →
                      (h : f ≍ Hom.id (some j)) →
                        Quiver.Hom.{v, u} (V := C)
                          (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) (some j) B objs : C)
                          (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Y B objs : C))
                    (fun (f : some j ⟶ some j) (h : f ≍ Hom.id (some j)) ↦
                      𝟙 (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) (some j) B objs))
                    ⋯ g)
                h)
            (fun (j_1 : J) (h : some j = none) ↦
              Eq.ndrec (motive := fun {X : WidePushoutShape J} ↦
                (f : X ⟶ Z) →
                  (h : Z = some j_1) →
                    (h : f ≍ Hom.init j_1) →
                      Quiver.Hom.{v, u} (V := C)
                        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)
                        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Z B objs : C))
                (fun (f : none ⟶ Z) (h : Z = some j_1) ↦
                  Eq.ndrec (motive := fun {Y : WidePushoutShape J} ↦
                    (f : none ⟶ Y) →
                      (h : f ≍ Hom.init j_1) →
                        Quiver.Hom.{v, u} (V := C)
                          (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) none B objs : C)
                          (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Y B objs : C))
                    (fun (f : none ⟶ some j_1) (h : f ≍ Hom.init j_1) ↦ arrows j_1) ⋯ f)
                ⋯ g)
            ⋯ ⋯ ⋯) :
        Quiver.Hom.{v, u} (V := C) (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) none B objs : C)
          (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Z B objs : C))
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C) (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)
      (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Z B objs : C))
    (Hom.casesOn (motive := fun (a a_1 : WidePushoutShape J) (x : a.Hom a_1) ↦
        (h : X = a) →
          (h : Z = a_1) →
            (h : f ≫ g ≍ x) →
              Quiver.Hom.{v, u} (V := C) (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)
                (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Z B objs : C))
        (f ≫ g)
        (fun (X_1 : WidePushoutShape J) (h : X = X_1) ↦
          Eq.ndrec (motive := fun (X_2 : WidePushoutShape J) ↦
            (h : Z = X_2) →
              (h : f ≫ g ≍ Hom.id X_2) →
                Quiver.Hom.{v, u} (V := C) (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)
                  (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Z B objs : C))
            (fun (h : Z = X) ↦
              Eq.ndrec (motive := fun {Y : WidePushoutShape J} ↦
                (f : X ⟶ Y) →
                  (h : f ≍ Hom.id X) →
                    Quiver.Hom.{v, u} (V := C)
                      (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)
                      (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Y B objs : C))
                (fun (f : X ⟶ X) (h : f ≍ Hom.id X) ↦
                  𝟙 (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs))
                ⋯ (f ≫ g))
            h)
        (fun (j : J) (h : X = none) ↦
          Eq.ndrec (motive := fun {X : WidePushoutShape J} ↦
            (f : X ⟶ Z) →
              (h : Z = some j) →
                (h : f ≍ Hom.init j) →
                  Quiver.Hom.{v, u} (V := C) (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)
                    (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Z B objs : C))
            (fun (f : none ⟶ Z) (h : Z = some j) ↦
              Eq.ndrec (motive := fun {Y : WidePushoutShape J} ↦
                (f : none ⟶ Y) →
                  (h : f ≍ Hom.init j) →
                    Quiver.Hom.{v, u} (V := C)
                      (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) none B objs : C)
                      (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Y B objs : C))
                (fun (f : none ⟶ some j) (h : f ≍ Hom.init j) ↦ arrows j) ⋯ f)
            ⋯ (f ≫ g))
        ⋯ ⋯ ⋯ :
      Quiver.Hom.{v, u} (V := C) (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)
        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Z B objs : C))
    (CategoryStruct.comp (Y := Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Y B objs)
        (Hom.casesOn (motive := fun (a a_1 : WidePushoutShape J) (x : a.Hom a_1) ↦
          (h : X = a) →
            (h : Y = a_1) →
              (h : f ≍ x) →
                Quiver.Hom.{v, u} (V := C) (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)
                  (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Y B objs : C))
          f
          (fun (X_1 : WidePushoutShape J) (h : X = X_1) ↦
            Eq.ndrec (motive := fun (X_2 : WidePushoutShape J) ↦
              (h : Y = X_2) →
                (h : f ≍ Hom.id X_2) →
                  Quiver.Hom.{v, u} (V := C) (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)
                    (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Y B objs : C))
              (fun (h : Y = X) ↦
                Eq.ndrec (motive := fun {Y : WidePushoutShape J} ↦
                  (f : X ⟶ Y) →
                    (h : f ≍ Hom.id X) →
                      Quiver.Hom.{v, u} (V := C)
                        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)
                        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Y B objs : C))
                  (fun (f : X ⟶ X) (h : f ≍ Hom.id X) ↦
                    𝟙 (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs))
                  ⋯ f)
              h)
          (fun (j : J) (h : X = none) ↦
            Eq.ndrec (motive := fun {X : WidePushoutShape J} ↦
              (f : X ⟶ Y) →
                (h : Y = some j) →
                  (h : f ≍ Hom.init j) →
                    Quiver.Hom.{v, u} (V := C)
                      (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)
                      (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Y B objs : C))
              (fun (f : none ⟶ Y) (h : Y = some j) ↦
                Eq.ndrec (motive := fun {Y : WidePushoutShape J} ↦
                  (f : none ⟶ Y) →
                    (h : f ≍ Hom.init j) →
                      Quiver.Hom.{v, u} (V := C)
                        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) none B objs : C)
                        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Y B objs : C))
                  (fun (f : none ⟶ some j) (h : f ≍ Hom.init j) ↦ arrows j) ⋯ f)
              ⋯ f)
          ⋯ ⋯ ⋯)
        (Hom.casesOn (motive := fun (a a_1 : WidePushoutShape J) (x : a.Hom a_1) ↦
          (h : Y = a) →
            (h : Z = a_1) →
              (h : g ≍ x) →
                Quiver.Hom.{v, u} (V := C) (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Y B objs : C)
                  (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Z B objs : C))
          g
          (fun (X : WidePushoutShape J) (h : Y = X) ↦
            Eq.ndrec (motive := fun (X : WidePushoutShape J) ↦
              (h : Z = X) →
                (h : g ≍ Hom.id X) →
                  Quiver.Hom.{v, u} (V := C) (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Y B objs : C)
                    (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Z B objs : C))
              (fun (h : Z = Y) ↦
                Eq.ndrec (motive := fun {Y_1 : WidePushoutShape J} ↦
                  (f : Y ⟶ Y_1) →
                    (h : f ≍ Hom.id Y) →
                      Quiver.Hom.{v, u} (V := C)
                        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Y B objs : C)
                        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Y_1 B objs : C))
                  (fun (f : Y ⟶ Y) (h : f ≍ Hom.id Y) ↦
                    𝟙 (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Y B objs))
                  ⋯ g)
              h)
          (fun (j : J) (h : Y = none) ↦
            Eq.ndrec (motive := fun {X : WidePushoutShape J} ↦
              (f : X ⟶ Z) →
                (h : Z = some j) →
                  (h : f ≍ Hom.init j) →
                    Quiver.Hom.{v, u} (V := C)
                      (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)
                      (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Z B objs : C))
              (fun (f : none ⟶ Z) (h : Z = some j) ↦
                Eq.ndrec (motive := fun {Y : WidePushoutShape J} ↦
                  (f : none ⟶ Y) →
                    (h : f ≍ Hom.init j) →
                      Quiver.Hom.{v, u} (V := C)
                        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) none B objs : C)
                        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Y B objs : C))
                  (fun (f : none ⟶ some j) (h : f ≍ Hom.init j) ↦ arrows j) ⋯ f)
              ⋯ g)
          ⋯ ⋯ ⋯) :
      Quiver.Hom.{v, u} (V := C) (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)
        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Z B objs : C))

Tactic:
cases f