-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Products (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f_1 : X ⟶ Y
g : X ⟶ Z
X_1 Y_1 : PushoutCocone f_1 g
f : X_1 ⟶ Y_1
⊢ Eq (α :=
    Functor.obj (𝟭 (PushoutCocone f_1 g)) X_1 ⟶
      Functor.obj
        (Functor.comp (D := BinaryCofan (Under.mk f_1) (Under.mk g))
          {
            obj := fun (c : PushoutCocone f_1 g) ↦
              BinaryCofan.mk (P := Under.mk (f_1 ≫ c.inl)) (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
            map := fun {c₁ c₂ : PushoutCocone f_1 g} (a : c₁ ⟶ c₂) ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ },
            map_id := ⋯, map_comp := ⋯ }
          {
            obj := fun (c : BinaryCofan (Under.mk f_1) (Under.mk g)) ↦
              PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
            map := fun {c₁ c₂ : BinaryCofan (Under.mk f_1) (Under.mk g)} (a : c₁ ⟶ c₂) ↦
              { hom := Under.Hom.right a.hom, w := ⋯ },
            map_id := ⋯, map_comp := ⋯ })
        Y_1)
    (Functor.map (𝟭 (PushoutCocone f_1 g)) f ≫ Iso.hom ((fun (c : PushoutCocone f_1 g) ↦ c.eta) Y_1))
    (Iso.hom ((fun (c : PushoutCocone f_1 g) ↦ c.eta) X_1) ≫
      Functor.map
        (Functor.comp (D := BinaryCofan (Under.mk f_1) (Under.mk g))
          {
            obj := fun (c : PushoutCocone f_1 g) ↦
              BinaryCofan.mk (P := Under.mk (f_1 ≫ c.inl)) (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
            map := fun {c₁ c₂ : PushoutCocone f_1 g} (a : c₁ ⟶ c₂) ↦
              { hom := Under.homMk a.hom ⋯, w := ⋯ :
                CoconeMorphism (C := Under.{v, u} X) (F := pair (Under.mk f_1) (Under.mk g))
                  (BinaryCofan.mk (P := Under.mk (f_1 ≫ c₁.inl)) (Under.homMk c₁.inl ⋯) (Under.homMk c₁.inr ⋯))
                  (BinaryCofan.mk (P := Under.mk (f_1 ≫ c₂.inl)) (Under.homMk c₂.inl ⋯) (Under.homMk c₂.inr ⋯)) },
            map_id := ⋯, map_comp := ⋯ : PushoutCocone f_1 g ⥤ BinaryCofan (Under.mk f_1) (Under.mk g) }
          {
            obj := fun (c : BinaryCofan (Under.mk f_1) (Under.mk g)) ↦
              PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
            map := fun {c₁ c₂ : BinaryCofan (Under.mk f_1) (Under.mk g)} (a : c₁ ⟶ c₂) ↦
              { hom := Under.Hom.right a.hom, w := ⋯ :
                CoconeMorphism (PushoutCocone.mk (Under.Hom.right c₁.inl) (Under.Hom.right c₁.inr) ⋯)
                  (PushoutCocone.mk (Under.Hom.right c₂.inl) (Under.Hom.right c₂.inr) ⋯) },
            map_id := ⋯, map_comp := ⋯ : BinaryCofan (Under.mk f_1) (Under.mk g) ⥤ PushoutCocone f_1 g })
        f)
have w : Eq (α :=
  (Functor.obj (𝟭 (PushoutCocone f_1 g)) X_1).pt ⟶
    Cocone.pt.{0, v, 0, u} (J := WalkingSpan) (F := span f_1 g)
      (Functor.obj
        (Functor.comp (D := BinaryCofan (Under.mk f_1) (Under.mk g))
          {
            obj := fun (c : PushoutCocone f_1 g) ↦
              BinaryCofan.mk (P := Under.mk (f_1 ≫ c.inl)) (Under.homMk c.inl sorry) (Under.homMk c.inr sorry),
            map := fun {c₁ c₂ : PushoutCocone f_1 g} (a : c₁ ⟶ c₂) ↦ { hom := Under.homMk a.hom sorry, w := sorry },
            map_id := sorry, map_comp := sorry }
          {
            obj := fun (c : BinaryCofan (Under.mk f_1) (Under.mk g)) ↦
              PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) sorry,
            map := fun {c₁ c₂ : BinaryCofan (Under.mk f_1) (Under.mk g)} (a : c₁ ⟶ c₂) ↦
              { hom := Under.Hom.right a.hom, w := sorry },
            map_id := sorry, map_comp := sorry })
        Y_1))
  (CoconeMorphism.hom (Functor.map (𝟭 (PushoutCocone f_1 g)) f ≫ Iso.hom ((fun (c : PushoutCocone f_1 g) ↦ c.eta) Y_1)))
  (CoconeMorphism.hom
    (Iso.hom ((fun (c : PushoutCocone f_1 g) ↦ c.eta) X_1) ≫
      Functor.map
        (Functor.comp (D := BinaryCofan (Under.mk f_1) (Under.mk g))
          {
            obj := fun (c : PushoutCocone f_1 g) ↦
              BinaryCofan.mk (P := Under.mk (f_1 ≫ c.inl)) (Under.homMk c.inl sorry) (Under.homMk c.inr sorry),
            map := fun {c₁ c₂ : PushoutCocone f_1 g} (a : c₁ ⟶ c₂) ↦
              { hom := Under.homMk a.hom sorry, w := sorry :
                CoconeMorphism (C := Under.{v, u} X) (F := pair (Under.mk f_1) (Under.mk g))
                  (BinaryCofan.mk (P := Under.mk (f_1 ≫ c₁.inl)) (Under.homMk c₁.inl sorry) (Under.homMk c₁.inr sorry))
                  (BinaryCofan.mk (P := Under.mk (f_1 ≫ c₂.inl)) (Under.homMk c₂.inl sorry) (Under.homMk c₂.inr sorry)) },
            map_id := sorry, map_comp := sorry : PushoutCocone f_1 g ⥤ BinaryCofan (Under.mk f_1) (Under.mk g) }
          {
            obj := fun (c : BinaryCofan (Under.mk f_1) (Under.mk g)) ↦
              PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) sorry,
            map := fun {c₁ c₂ : BinaryCofan (Under.mk f_1) (Under.mk g)} (a : c₁ ⟶ c₂) ↦
              { hom := Under.Hom.right a.hom, w := sorry :
                CoconeMorphism (PushoutCocone.mk (Under.Hom.right c₁.inl) (Under.Hom.right c₁.inr) sorry)
                  (PushoutCocone.mk (Under.Hom.right c₂.inl) (Under.Hom.right c₂.inr) sorry) },
            map_id := sorry, map_comp := sorry : BinaryCofan (Under.mk f_1) (Under.mk g) ⥤ PushoutCocone f_1 g })
        f))
Tactic: ext