-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
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
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 ⋯) (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))
    (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 ⋯) (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))
⊢ 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)

Tactic:
ext