-- 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 : BinaryFan (Over.mk f) (Over.mk g)
f_1 : X_1 ⟶ Y_1
w :
  Eq (α :=
    Over.left.{v, u} (X := X)
        (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 := ⋯ },
                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_1)) ⟶
      (Functor.obj (𝟭 (BinaryFan (Over.mk f) (Over.mk g))) Y_1).pt.left)
    (Over.Hom.left
      (ConeMorphism.hom
        (Functor.map
            (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) (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) })
            f_1 ≫
          Iso.hom
            ((fun (X_2 : BinaryFan (Over.mk f) (Over.mk g)) ↦
                (BinaryFan.ext
                    (Over.isoMk
                      (Iso.refl
                        (Over.left.{v, u} (X := X)
                          (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 := ⋯ },
                                  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_2))))
                      ⋯)
                    ⋯ ⋯ :
                  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_2 ≅
                    Functor.obj (𝟭 (BinaryFan (Over.mk f) (Over.mk g))) X_2))
              Y_1))))
    (Over.Hom.left
      (ConeMorphism.hom
        (Iso.hom
            ((fun (X_2 : BinaryFan (Over.mk f) (Over.mk g)) ↦
                (BinaryFan.ext
                    (Over.isoMk
                      (Iso.refl
                        (Over.left.{v, u} (X := X)
                          (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 := ⋯ },
                                  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_2))))
                      ⋯)
                    ⋯ ⋯ :
                  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_2 ≅
                    Functor.obj (𝟭 (BinaryFan (Over.mk f) (Over.mk g))) X_2))
              X_1) ≫
          Functor.map (𝟭 (BinaryFan (Over.mk f) (Over.mk g))) f_1)))
⊢ Eq (α :=
    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_1 ⟶
      Functor.obj (𝟭 (BinaryFan (Over.mk f) (Over.mk g))) Y_1)
    (Functor.map
        (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) (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) })
        f_1 ≫
      Iso.hom
        ((fun (X_2 : BinaryFan (Over.mk f) (Over.mk g)) ↦
            (BinaryFan.ext
                (Over.isoMk
                  (Iso.refl
                    (Over.left.{v, u} (X := X)
                      (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 := ⋯ },
                              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_2))))
                  ⋯)
                ⋯ ⋯ :
              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_2 ≅
                Functor.obj (𝟭 (BinaryFan (Over.mk f) (Over.mk g))) X_2))
          Y_1))
    (Iso.hom
        ((fun (X_2 : BinaryFan (Over.mk f) (Over.mk g)) ↦
            (BinaryFan.ext
                (Over.isoMk
                  (Iso.refl
                    (Over.left.{v, u} (X := X)
                      (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 := ⋯ },
                              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_2))))
                  ⋯)
                ⋯ ⋯ :
              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_2 ≅
                Functor.obj (𝟭 (BinaryFan (Over.mk f) (Over.mk g))) X_2))
          X_1) ≫
      Functor.map (𝟭 (BinaryFan (Over.mk f) (Over.mk g))) f_1)

Tactic:
ext