-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
w :
  Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C)
      (Under.right.{v, u} (X := X)
        (Cocone.pt (J := Discrete WalkingPair) (F := pair (Under.mk f) (Under.mk g))
          (Functor.obj
            {
              obj := fun (c : PushoutCocone f g) ↦
                BinaryCofan.mk (P := Under.mk (f ≫ c.inl)) (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
              map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ },
              map_id := ⋯, map_comp := ⋯ }
            c)))
      (Under.right.{v, u} (X := X)
        (Cocone.pt (J := Discrete WalkingPair) (F := pair (Under.mk f) (Under.mk g))
          (Functor.obj
            {
              obj := fun (c : PushoutCocone f g) ↦
                BinaryCofan.mk (P := Under.mk (f ≫ c.inl)) (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
              map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ },
              map_id := ⋯, map_comp := ⋯ }
            c))))
    (Under.Hom.right
        (CoconeMorphism.hom
          (Functor.map
              {
                obj := fun (c : PushoutCocone f g) ↦
                  BinaryCofan.mk (P := Under.mk (f ≫ c.inl)) (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ },
                map_id := ⋯, map_comp := ⋯ }
              (NatTrans.app (Iso.hom (NatIso.ofComponents (fun (c : PushoutCocone f g) ↦ c.eta) ⋯)) c) ≫
            NatTrans.app
              (Iso.hom
                (NatIso.ofComponents
                  (fun (X_1 : BinaryCofan (Under.mk f) (Under.mk g)) ↦
                    BinaryCofan.ext
                      (Under.isoMk
                        (Iso.refl
                          (Under.right.{v, u} (X := X)
                            (Cocone.pt (J := Discrete WalkingPair) (F := pair (Under.mk f) (Under.mk g))
                              (Functor.obj
                                (Functor.comp (D := PushoutCocone f g)
                                  {
                                    obj := fun (c : BinaryCofan (Under.mk f) (Under.mk g)) ↦
                                      PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                                    map := fun {c₁ c₂ : BinaryCofan (Under.mk f) (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) (Under.mk g) ⥤ PushoutCocone f g }
                                  {
                                    obj := fun (c : PushoutCocone f g) ↦
                                      BinaryCofan.mk (P := Under.mk (f ≫ c.inl)) (Under.homMk c.inl ⋯)
                                        (Under.homMk c.inr ⋯),
                                    map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) ↦
                                      { hom := Under.homMk a.hom ⋯, w := ⋯ :
                                        CoconeMorphism (C := Under.{v, u} X) (F := pair (Under.mk f) (Under.mk g))
                                          (BinaryCofan.mk (P := Under.mk (f ≫ c₁.inl)) (Under.homMk c₁.inl ⋯)
                                            (Under.homMk c₁.inr ⋯))
                                          (BinaryCofan.mk (P := Under.mk (f ≫ c₂.inl)) (Under.homMk c₂.inl ⋯)
                                            (Under.homMk c₂.inr ⋯)) },
                                    map_id := ⋯, map_comp := ⋯ :
                                    PushoutCocone f g ⥤ BinaryCofan (Under.mk f) (Under.mk g) })
                                X_1))))
                        ⋯)
                      ⋯ ⋯)
                  ⋯))
              (Functor.obj
                {
                  obj := fun (c : PushoutCocone f g) ↦
                    BinaryCofan.mk (P := Under.mk (f ≫ c.inl)) (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                  map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) ↦
                    { hom := Under.homMk a.hom ⋯, w := ⋯ :
                      CoconeMorphism (C := Under.{v, u} X) (F := pair (Under.mk f) (Under.mk g))
                        (BinaryCofan.mk (P := Under.mk (f ≫ c₁.inl)) (Under.homMk c₁.inl ⋯) (Under.homMk c₁.inr ⋯))
                        (BinaryCofan.mk (P := Under.mk (f ≫ c₂.inl)) (Under.homMk c₂.inl ⋯) (Under.homMk c₂.inr ⋯)) },
                  map_id := ⋯, map_comp := ⋯ : PushoutCocone f g ⥤ BinaryCofan (Under.mk f) (Under.mk g) }
                c))) :
      Quiver.Hom.{v, u} (V := C)
        (Under.right.{v, u} (X := X)
          (Cocone.pt (J := Discrete WalkingPair) (F := pair (Under.mk f) (Under.mk g))
            (Functor.obj
              {
                obj := fun (c : PushoutCocone f g) ↦
                  BinaryCofan.mk (P := Under.mk (f ≫ c.inl)) (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ },
                map_id := ⋯, map_comp := ⋯ }
              c)))
        (Under.right.{v, u} (X := X)
          (Cocone.pt (J := Discrete WalkingPair) (F := pair (Under.mk f) (Under.mk g))
            (Functor.obj
              {
                obj := fun (c : PushoutCocone f g) ↦
                  BinaryCofan.mk (P := Under.mk (f ≫ c.inl)) (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ },
                map_id := ⋯, map_comp := ⋯ }
              c))))
    (Under.Hom.right
        (CoconeMorphism.hom
          (𝟙
            (Functor.obj
              {
                obj := fun (c : PushoutCocone f g) ↦
                  BinaryCofan.mk (P := Under.mk (f ≫ c.inl)) (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ },
                map_id := ⋯, map_comp := ⋯ }
              c))) :
      Quiver.Hom.{v, u} (V := C)
        (Under.right.{v, u} (X := X)
          (Cocone.pt (J := Discrete WalkingPair) (F := pair (Under.mk f) (Under.mk g))
            (Functor.obj
              {
                obj := fun (c : PushoutCocone f g) ↦
                  BinaryCofan.mk (P := Under.mk (f ≫ c.inl)) (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ },
                map_id := ⋯, map_comp := ⋯ }
              c)))
        (Under.right.{v, u} (X := X)
          (Cocone.pt (J := Discrete WalkingPair) (F := pair (Under.mk f) (Under.mk g))
            (Functor.obj
              {
                obj := fun (c : PushoutCocone f g) ↦
                  BinaryCofan.mk (P := Under.mk (f ≫ c.inl)) (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ },
                map_id := ⋯, map_comp := ⋯ }
              c))))
⊢ Eq.{v + 1} (α :=
    Quiver.Hom (V := BinaryCofan (Under.mk f) (Under.mk g))
      (Functor.obj
        {
          obj := fun (c : PushoutCocone f g) ↦
            BinaryCofan.mk (P := Under.mk (f ≫ c.inl)) (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
          map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
          map_comp := ⋯ }
        c)
      (Functor.obj
        {
          obj := fun (c : PushoutCocone f g) ↦
            BinaryCofan.mk (P := Under.mk (f ≫ c.inl)) (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
          map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
          map_comp := ⋯ }
        c))
    (Functor.map
          {
            obj := fun (c : PushoutCocone f g) ↦
              BinaryCofan.mk (P := Under.mk (f ≫ c.inl)) (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
            map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
            map_comp := ⋯ }
          (NatTrans.app (Iso.hom (NatIso.ofComponents (fun (c : PushoutCocone f g) ↦ c.eta) ⋯)) c) ≫
        NatTrans.app
          (Iso.hom
            (NatIso.ofComponents
              (fun (X_1 : BinaryCofan (Under.mk f) (Under.mk g)) ↦
                BinaryCofan.ext
                  (Under.isoMk
                    (Iso.refl
                      (Under.right.{v, u} (X := X)
                        (Cocone.pt (J := Discrete WalkingPair) (F := pair (Under.mk f) (Under.mk g))
                          (Functor.obj
                            (Functor.comp (D := PushoutCocone f g)
                              {
                                obj := fun (c : BinaryCofan (Under.mk f) (Under.mk g)) ↦
                                  PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                                map := fun {c₁ c₂ : BinaryCofan (Under.mk f) (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) (Under.mk g) ⥤ PushoutCocone f g }
                              {
                                obj := fun (c : PushoutCocone f g) ↦
                                  BinaryCofan.mk (P := Under.mk (f ≫ c.inl)) (Under.homMk c.inl ⋯)
                                    (Under.homMk c.inr ⋯),
                                map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) ↦
                                  { hom := Under.homMk a.hom ⋯, w := ⋯ :
                                    CoconeMorphism (C := Under.{v, u} X) (F := pair (Under.mk f) (Under.mk g))
                                      (BinaryCofan.mk (P := Under.mk (f ≫ c₁.inl)) (Under.homMk c₁.inl ⋯)
                                        (Under.homMk c₁.inr ⋯))
                                      (BinaryCofan.mk (P := Under.mk (f ≫ c₂.inl)) (Under.homMk c₂.inl ⋯)
                                        (Under.homMk c₂.inr ⋯)) },
                                map_id := ⋯, map_comp := ⋯ :
                                PushoutCocone f g ⥤ BinaryCofan (Under.mk f) (Under.mk g) })
                            X_1))))
                    ⋯)
                  ⋯ ⋯)
              ⋯))
          (Functor.obj
            {
              obj := fun (c : PushoutCocone f g) ↦
                BinaryCofan.mk (P := Under.mk (f ≫ c.inl)) (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
              map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) ↦
                { hom := Under.homMk a.hom ⋯, w := ⋯ :
                  CoconeMorphism (C := Under.{v, u} X) (F := pair (Under.mk f) (Under.mk g))
                    (BinaryCofan.mk (P := Under.mk (f ≫ c₁.inl)) (Under.homMk c₁.inl ⋯) (Under.homMk c₁.inr ⋯))
                    (BinaryCofan.mk (P := Under.mk (f ≫ c₂.inl)) (Under.homMk c₂.inl ⋯) (Under.homMk c₂.inr ⋯)) },
              map_id := ⋯, map_comp := ⋯ : PushoutCocone f g ⥤ BinaryCofan (Under.mk f) (Under.mk g) }
            c) :
      Quiver.Hom (V := BinaryCofan (Under.mk f) (Under.mk g))
        (Functor.obj
          {
            obj := fun (c : PushoutCocone f g) ↦
              BinaryCofan.mk (P := Under.mk (f ≫ c.inl)) (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
            map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
            map_comp := ⋯ }
          c)
        (Functor.obj
          {
            obj := fun (c : PushoutCocone f g) ↦
              BinaryCofan.mk (P := Under.mk (f ≫ c.inl)) (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
            map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
            map_comp := ⋯ }
          c))
    (𝟙
        (Functor.obj
          {
            obj := fun (c : PushoutCocone f g) ↦
              BinaryCofan.mk (P := Under.mk (f ≫ c.inl)) (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
            map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
            map_comp := ⋯ }
          c) :
      Quiver.Hom (V := BinaryCofan (Under.mk f) (Under.mk g))
        (Functor.obj
          {
            obj := fun (c : PushoutCocone f g) ↦
              BinaryCofan.mk (P := Under.mk (f ≫ c.inl)) (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
            map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
            map_comp := ⋯ }
          c)
        (Functor.obj
          {
            obj := fun (c : PushoutCocone f g) ↦
              BinaryCofan.mk (P := Under.mk (f ≫ c.inl)) (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
            map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
            map_comp := ⋯ }
          c))

Tactic:
ext