-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
f : X_1 ⟶ Y
g : X_1 ⟶ Z
X : BinaryCofan (Under.mk f) (Under.mk g)
h :
  Under.Hom.right
      (BinaryCofan.inl
          (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) ≫
        Iso.hom
          (Under.isoMk
            (Iso.refl
              (Under.right.{v, u} (X := X_1)
                (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_1) (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))))
            ⋯)) =
    Under.Hom.right (Functor.obj (𝟭 (BinaryCofan (Under.mk f) (Under.mk g))) X).inl
⊢ BinaryCofan.inl
        (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) ≫
      Iso.hom
        (Under.isoMk
          (Iso.refl
            (Under.right.{v, u} (X := X_1)
              (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_1) (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))))
          ⋯) =
    (Functor.obj (𝟭 (BinaryCofan (Under.mk f) (Under.mk g))) X).inl

Tactic:
ext