-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
X_1 Y_1 : PullbackCone f g
f_1 : X_1 ⟶ Y_1
w :
  Eq (α :=
    (Functor.obj (𝟭 (PullbackCone f g)) X_1).pt ⟶
      Cone.pt.{0, v, 0, u} (J := WalkingCospan) (F := cospan f g)
        (Functor.obj
          (Functor.comp (D := BinaryFan (Over.mk f) (Over.mk 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 := ⋯ }, map_id := ⋯,
              map_comp := ⋯ }
            {
              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 := ⋯ })
          Y_1))
    (ConeMorphism.hom (Functor.map (𝟭 (PullbackCone f g)) f_1 ≫ Iso.hom ((fun (c : PullbackCone f g) ↦ c.eta) Y_1)))
    (ConeMorphism.hom
      (Iso.hom ((fun (c : PullbackCone f g) ↦ c.eta) X_1) ≫
        Functor.map
          (Functor.comp (D := BinaryFan (Over.mk f) (Over.mk 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) (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) }
            {
              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 })
          f_1))
⊢ Eq (α :=
    Functor.obj (𝟭 (PullbackCone f g)) X_1 ⟶
      Functor.obj
        (Functor.comp (D := BinaryFan (Over.mk f) (Over.mk 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 := ⋯ }, map_id := ⋯,
            map_comp := ⋯ }
          {
            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 := ⋯ })
        Y_1)
    (Functor.map (𝟭 (PullbackCone f g)) f_1 ≫ Iso.hom ((fun (c : PullbackCone f g) ↦ c.eta) Y_1))
    (Iso.hom ((fun (c : PullbackCone f g) ↦ c.eta) X_1) ≫
      Functor.map
        (Functor.comp (D := BinaryFan (Over.mk f) (Over.mk 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) (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) }
          {
            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 })
        f_1)

Tactic:
ext