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 : Y ⟶ X
g : Z ⟶ X
X✝ Y✝ : BinaryFan (Over.mk f) (Over.mk g)
f✝ : X✝ ⟶ Y✝
⊢ ({ obj := fun c ↦ PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
              map := fun {c₁ c₂} a ↦ { hom := Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
            { obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
              map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).map
        f✝ ≫
      (BinaryFan.ext
          (Over.isoMk
            (Iso.refl
              (({ obj := fun c ↦ PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
                          map := fun {c₁ c₂} a ↦ { hom := Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
                        { obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
                          map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
                          map_comp := ⋯ }).obj
                    Y✝).pt.left)
            ⋯)
          ⋯ ⋯).hom =
    (BinaryFan.ext
          (Over.isoMk
            (Iso.refl
              (({ obj := fun c ↦ PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
                          map := fun {c₁ c₂} a ↦ { hom := Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
                        { obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
                          map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
                          map_comp := ⋯ }).obj
                    X✝).pt.left)
            ⋯)
          ⋯ ⋯).hom ≫
      (𝟭 (BinaryFan (Over.mk f) (Over.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 : Y ⟶ X
g : Z ⟶ X
X✝ Y✝ : BinaryFan (Over.mk f) (Over.mk g)
f✝ : X✝ ⟶ Y✝
⊢ Over.Hom.left
      (({ obj := fun c ↦ PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
                  map := fun {c₁ c₂} a ↦ { hom := Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
                { obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
                  map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).map
            f✝ ≫
          (BinaryFan.ext
              (Over.isoMk
                (Iso.refl
                  (({ obj := fun c ↦ PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
                              map := fun {c₁ c₂} a ↦ { hom := Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯,
                              map_comp := ⋯ } ⋙
                            { obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
                              map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
                              map_comp := ⋯ }).obj
                        Y✝).pt.left)
                ⋯)
              ⋯ ⋯).hom).hom =
    Over.Hom.left
      ((BinaryFan.ext
              (Over.isoMk
                (Iso.refl
                  (({ obj := fun c ↦ PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
                              map := fun {c₁ c₂} a ↦ { hom := Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯,
                              map_comp := ⋯ } ⋙
                            { obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
                              map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
                              map_comp := ⋯ }).obj
                        X✝).pt.left)
                ⋯)
              ⋯ ⋯).hom ≫
          (𝟭 (BinaryFan (Over.mk f) (Over.mk g))).map f✝).hom