Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
X✝ Y✝ : BinaryCofan (Under.mk f) (Under.mk g)
f✝ : X✝ ⟶ Y✝
⊢ ({ obj := fun c ↦ PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
              map := fun {c₁ c₂} a ↦ { hom := Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
            { obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
              map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).map
        f✝ ≫
      (BinaryCofan.ext
          (Under.isoMk
            (Iso.refl
              (({ obj := fun c ↦ PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                          map := fun {c₁ c₂} a ↦ { hom := Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯,
                          map_comp := ⋯ } ⋙
                        { obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                          map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
                          map_comp := ⋯ }).obj
                    Y✝).pt.right)
            ⋯)
          ⋯ ⋯).hom =
    (BinaryCofan.ext
          (Under.isoMk
            (Iso.refl
              (({ obj := fun c ↦ PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                          map := fun {c₁ c₂} a ↦ { hom := Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯,
                          map_comp := ⋯ } ⋙
                        { obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                          map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
                          map_comp := ⋯ }).obj
                    X✝).pt.right)
            ⋯)
          ⋯ ⋯).hom ≫
      (𝟭 (BinaryCofan (Under.mk f) (Under.mk g))).map f✝

Tactic:
ext

Goal state after:
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
X✝ Y✝ : BinaryCofan (Under.mk f) (Under.mk g)
f✝ : X✝ ⟶ Y✝
⊢ Under.Hom.right
      (({ obj := fun c ↦ PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                  map := fun {c₁ c₂} a ↦ { hom := Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
                { obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                  map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).map
            f✝ ≫
          (BinaryCofan.ext
              (Under.isoMk
                (Iso.refl
                  (({ obj := fun c ↦ PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                              map := fun {c₁ c₂} a ↦ { hom := Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯,
                              map_comp := ⋯ } ⋙
                            { obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                              map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
                              map_comp := ⋯ }).obj
                        Y✝).pt.right)
                ⋯)
              ⋯ ⋯).hom).hom =
    Under.Hom.right
      ((BinaryCofan.ext
              (Under.isoMk
                (Iso.refl
                  (({ obj := fun c ↦ PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                              map := fun {c₁ c₂} a ↦ { hom := Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯,
                              map_comp := ⋯ } ⋙
                            { obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                              map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
                              map_comp := ⋯ }).obj
                        X✝).pt.right)
                ⋯)
              ⋯ ⋯).hom ≫
          (𝟭 (BinaryCofan (Under.mk f) (Under.mk g))).map f✝).hom