-- 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 : X ⟶ Y
g : X ⟶ Z
X_1 Y_1 : BinaryCofan (Under.mk f) (Under.mk g)
f_1 : X_1 ⟶ Y_1
⊢ Eq (α :=
    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)
    (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))
    (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)
have w : 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) sorry,
              map := fun {c₁ c₂ : BinaryCofan (Under.mk f) (Under.mk g)} (a : c₁ ⟶ c₂) ↦
                { hom := Under.Hom.right a.hom, w := sorry },
              map_id := sorry, map_comp := sorry }
            {
              obj := fun (c : PushoutCocone f g) ↦
                BinaryCofan.mk (P := Under.mk (f ≫ c.inl)) (Under.homMk c.inl sorry) (Under.homMk c.inr sorry),
              map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) ↦ { hom := Under.homMk a.hom sorry, w := sorry },
              map_id := sorry, map_comp := sorry })
          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) sorry,
              map := fun {c₁ c₂ : BinaryCofan (Under.mk f) (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) (Under.mk g) ⥤ PushoutCocone f g }
            {
              obj := fun (c : PushoutCocone f g) ↦
                BinaryCofan.mk (P := Under.mk (f ≫ c.inl)) (Under.homMk c.inl sorry) (Under.homMk c.inr sorry),
              map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) ↦
                { hom := Under.homMk a.hom sorry, w := sorry :
                  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 sorry) (Under.homMk c₁.inr sorry))
                    (BinaryCofan.mk (P := Under.mk (f ≫ c₂.inl)) (Under.homMk c₂.inl sorry) (Under.homMk c₂.inr sorry)) },
              map_id := sorry, map_comp := sorry : 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) sorry,
                                map := fun {c₁ c₂ : BinaryCofan (Under.mk f) (Under.mk g)} (a : c₁ ⟶ c₂) ↦
                                  { hom := Under.Hom.right a.hom, w := sorry },
                                map_id := sorry, map_comp := sorry }
                              {
                                obj := fun (c : PushoutCocone f g) ↦
                                  BinaryCofan.mk (P := Under.mk (f ≫ c.inl)) (Under.homMk c.inl sorry)
                                    (Under.homMk c.inr sorry),
                                map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) ↦
                                  { hom := Under.homMk a.hom sorry, w := sorry },
                                map_id := sorry, map_comp := sorry })
                            X_2))))
                    sorry)
                  sorry sorry :
                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) sorry,
                        map := fun {c₁ c₂ : BinaryCofan (Under.mk f) (Under.mk g)} (a : c₁ ⟶ c₂) ↦
                          { hom := Under.Hom.right a.hom, w := sorry },
                        map_id := sorry, map_comp := sorry }
                      {
                        obj := fun (c : PushoutCocone f g) ↦
                          BinaryCofan.mk (P := Under.mk (f ≫ c.inl)) (Under.homMk c.inl sorry) (Under.homMk c.inr sorry),
                        map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) ↦ { hom := Under.homMk a.hom sorry, w := sorry },
                        map_id := sorry, map_comp := sorry })
                    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) sorry,
                                map := fun {c₁ c₂ : BinaryCofan (Under.mk f) (Under.mk g)} (a : c₁ ⟶ c₂) ↦
                                  { hom := Under.Hom.right a.hom, w := sorry },
                                map_id := sorry, map_comp := sorry }
                              {
                                obj := fun (c : PushoutCocone f g) ↦
                                  BinaryCofan.mk (P := Under.mk (f ≫ c.inl)) (Under.homMk c.inl sorry)
                                    (Under.homMk c.inr sorry),
                                map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) ↦
                                  { hom := Under.homMk a.hom sorry, w := sorry },
                                map_id := sorry, map_comp := sorry })
                            X_2))))
                    sorry)
                  sorry sorry :
                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) sorry,
                        map := fun {c₁ c₂ : BinaryCofan (Under.mk f) (Under.mk g)} (a : c₁ ⟶ c₂) ↦
                          { hom := Under.Hom.right a.hom, w := sorry },
                        map_id := sorry, map_comp := sorry }
                      {
                        obj := fun (c : PushoutCocone f g) ↦
                          BinaryCofan.mk (P := Under.mk (f ≫ c.inl)) (Under.homMk c.inl sorry) (Under.homMk c.inr sorry),
                        map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) ↦ { hom := Under.homMk a.hom sorry, w := sorry },
                        map_id := sorry, map_comp := sorry })
                    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: ext