-- 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 : Y ⟶ X_1
g : Z ⟶ X_1
X : BinaryFan (Over.mk f) (Over.mk g)
h :
  Over.Hom.left
      (BinaryFan.snd
        (Functor.obj
          (Functor.comp (D := PullbackCone f g)
            {
              obj := fun (c : BinaryFan (Over.mk f) (Over.mk g)) ↦
                PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
              map := fun {c₁ c₂ : BinaryFan (Over.mk f) (Over.mk g)} (a : c₁ ⟶ c₂) ↦
                { hom := Over.Hom.left a.hom, w := ⋯ },
              map_id := ⋯, map_comp := ⋯ }
            {
              obj := fun (c : PullbackCone f g) ↦
                BinaryFan.mk (P := Over.mk (c.fst ≫ f)) (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
              map := fun {c₁ c₂ : PullbackCone f g} (a : c₁ ⟶ c₂) ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
              map_comp := ⋯ })
          X)) =
    Over.Hom.left
      (Iso.hom
          (Over.isoMk
            (Iso.refl
              (Over.left.{v, u} (X := X_1)
                (Cone.pt (J := Discrete WalkingPair) (F := pair (Over.mk f) (Over.mk g))
                  (Functor.obj
                    (Functor.comp (D := PullbackCone f g)
                      {
                        obj := fun (c : BinaryFan (Over.mk f) (Over.mk g)) ↦
                          PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
                        map := fun {c₁ c₂ : BinaryFan (Over.mk f) (Over.mk g)} (a : c₁ ⟶ c₂) ↦
                          { hom := Over.Hom.left a.hom, w := ⋯ :
                            ConeMorphism (PullbackCone.mk (Over.Hom.left c₁.fst) (Over.Hom.left c₁.snd) ⋯)
                              (PullbackCone.mk (Over.Hom.left c₂.fst) (Over.Hom.left c₂.snd) ⋯) },
                        map_id := ⋯, map_comp := ⋯ : BinaryFan (Over.mk f) (Over.mk g) ⥤ PullbackCone f g }
                      {
                        obj := fun (c : PullbackCone f g) ↦
                          BinaryFan.mk (P := Over.mk (c.fst ≫ f)) (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
                        map := fun {c₁ c₂ : PullbackCone f g} (a : c₁ ⟶ c₂) ↦
                          { hom := Over.homMk a.hom ⋯, w := ⋯ :
                            ConeMorphism (C := Over.{v, u} X_1) (F := pair (Over.mk f) (Over.mk g))
                              (BinaryFan.mk (P := Over.mk (c₁.fst ≫ f)) (Over.homMk c₁.fst ⋯) (Over.homMk c₁.snd ⋯))
                              (BinaryFan.mk (P := Over.mk (c₂.fst ≫ f)) (Over.homMk c₂.fst ⋯) (Over.homMk c₂.snd ⋯)) },
                        map_id := ⋯, map_comp := ⋯ : PullbackCone f g ⥤ BinaryFan (Over.mk f) (Over.mk g) })
                    X))))
            ⋯) ≫
        (Functor.obj (𝟭 (BinaryFan (Over.mk f) (Over.mk g))) X).snd)
⊢ BinaryFan.snd
      (Functor.obj
        (Functor.comp (D := PullbackCone f g)
          {
            obj := fun (c : BinaryFan (Over.mk f) (Over.mk g)) ↦
              PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
            map := fun {c₁ c₂ : BinaryFan (Over.mk f) (Over.mk g)} (a : c₁ ⟶ c₂) ↦
              { hom := Over.Hom.left a.hom, w := ⋯ },
            map_id := ⋯, map_comp := ⋯ }
          {
            obj := fun (c : PullbackCone f g) ↦
              BinaryFan.mk (P := Over.mk (c.fst ≫ f)) (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
            map := fun {c₁ c₂ : PullbackCone f g} (a : c₁ ⟶ c₂) ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
            map_comp := ⋯ })
        X) =
    Iso.hom
        (Over.isoMk
          (Iso.refl
            (Over.left.{v, u} (X := X_1)
              (Cone.pt (J := Discrete WalkingPair) (F := pair (Over.mk f) (Over.mk g))
                (Functor.obj
                  (Functor.comp (D := PullbackCone f g)
                    {
                      obj := fun (c : BinaryFan (Over.mk f) (Over.mk g)) ↦
                        PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
                      map := fun {c₁ c₂ : BinaryFan (Over.mk f) (Over.mk g)} (a : c₁ ⟶ c₂) ↦
                        { hom := Over.Hom.left a.hom, w := ⋯ :
                          ConeMorphism (PullbackCone.mk (Over.Hom.left c₁.fst) (Over.Hom.left c₁.snd) ⋯)
                            (PullbackCone.mk (Over.Hom.left c₂.fst) (Over.Hom.left c₂.snd) ⋯) },
                      map_id := ⋯, map_comp := ⋯ : BinaryFan (Over.mk f) (Over.mk g) ⥤ PullbackCone f g }
                    {
                      obj := fun (c : PullbackCone f g) ↦
                        BinaryFan.mk (P := Over.mk (c.fst ≫ f)) (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
                      map := fun {c₁ c₂ : PullbackCone f g} (a : c₁ ⟶ c₂) ↦
                        { hom := Over.homMk a.hom ⋯, w := ⋯ :
                          ConeMorphism (C := Over.{v, u} X_1) (F := pair (Over.mk f) (Over.mk g))
                            (BinaryFan.mk (P := Over.mk (c₁.fst ≫ f)) (Over.homMk c₁.fst ⋯) (Over.homMk c₁.snd ⋯))
                            (BinaryFan.mk (P := Over.mk (c₂.fst ≫ f)) (Over.homMk c₂.fst ⋯) (Over.homMk c₂.snd ⋯)) },
                      map_id := ⋯, map_comp := ⋯ : PullbackCone f g ⥤ BinaryFan (Over.mk f) (Over.mk g) })
                  X))))
          ⋯) ≫
      (Functor.obj (𝟭 (BinaryFan (Over.mk f) (Over.mk g))) X).snd

Tactic:
ext