-- 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
X_1 Y_1 : BinaryCofan (Under.mk f) (Under.mk g)
f_1 : X_1 ⟶ Y_1
⊢ Eq (α :=
    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 := ⋯ },
                map_id := ⋯, map_comp := ⋯ }
              {
                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 := ⋯ })
            X_1)) ⟶
      (Functor.obj (𝟭 (BinaryCofan (Under.mk f) (Under.mk g))) Y_1).pt.right)
    (Under.Hom.right
      (CoconeMorphism.hom
        (Functor.map
            (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) })
            f_1 ≫
          Iso.hom
            ((fun (X_2 : 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 := ⋯ },
                                  map_id := ⋯, map_comp := ⋯ }
                                {
                                  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 := ⋯ })
                              X_2))))
                      ⋯)
                    ⋯ ⋯ :
                  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 := ⋯ },
                          map_id := ⋯, map_comp := ⋯ }
                        {
                          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 := ⋯ })
                      X_2 ≅
                    Functor.obj (𝟭 (BinaryCofan (Under.mk f) (Under.mk g))) X_2))
              Y_1))))
    (Under.Hom.right
      (CoconeMorphism.hom
        (Iso.hom
            ((fun (X_2 : 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 := ⋯ },
                                  map_id := ⋯, map_comp := ⋯ }
                                {
                                  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 := ⋯ })
                              X_2))))
                      ⋯)
                    ⋯ ⋯ :
                  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 := ⋯ },
                          map_id := ⋯, map_comp := ⋯ }
                        {
                          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 := ⋯ })
                      X_2 ≅
                    Functor.obj (𝟭 (BinaryCofan (Under.mk f) (Under.mk g))) X_2))
              X_1) ≫
          Functor.map (𝟭 (BinaryCofan (Under.mk f) (Under.mk g))) f_1)))

Tactic:
simp