-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Products (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : PullbackCone f g
⊢ Eq.{v + 1} (α :=
    Quiver.Hom (V := BinaryFan (Over.mk f) (Over.mk g))
      (Functor.obj
        {
          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 := ⋯ }
        c)
      (Functor.obj
        {
          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 := ⋯ }
        c))
    (Functor.map
          {
            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 := ⋯ }
          (NatTrans.app (Iso.hom (NatIso.ofComponents (fun (c : PullbackCone f g) ↦ c.eta) ⋯)) c) ≫
        NatTrans.app
          (Iso.hom
            (NatIso.ofComponents
              (fun (X_1 : 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 := ⋯ :
                                    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) })
                            X_1))))
                    ⋯)
                  ⋯ ⋯)
              ⋯))
          (Functor.obj
            {
              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) }
            c) :
      Quiver.Hom (V := BinaryFan (Over.mk f) (Over.mk g))
        (Functor.obj
          {
            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 := ⋯ }
          c)
        (Functor.obj
          {
            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 := ⋯ }
          c))
    (𝟙
        (Functor.obj
          {
            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 := ⋯ }
          c) :
      Quiver.Hom (V := BinaryFan (Over.mk f) (Over.mk g))
        (Functor.obj
          {
            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 := ⋯ }
          c)
        (Functor.obj
          {
            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 := ⋯ }
          c))
have w : Eq.{v + 1} (α :=
  Quiver.Hom.{v, u} (V := C)
    (Over.left.{v, u} (X := X)
      (Cone.pt (J := Discrete WalkingPair) (F := pair (Over.mk f) (Over.mk g))
        (Functor.obj
          {
            obj := fun (c : PullbackCone f g) ↦
              BinaryFan.mk (P := Over.mk (c.fst ≫ f)) (Over.homMk c.fst sorry) (Over.homMk c.snd sorry),
            map := fun {c₁ c₂ : PullbackCone f g} (a : c₁ ⟶ c₂) ↦ { hom := Over.homMk a.hom sorry, w := sorry }, map_id := sorry,
            map_comp := sorry }
          c)))
    (Over.left.{v, u} (X := X)
      (Cone.pt (J := Discrete WalkingPair) (F := pair (Over.mk f) (Over.mk g))
        (Functor.obj
          {
            obj := fun (c : PullbackCone f g) ↦
              BinaryFan.mk (P := Over.mk (c.fst ≫ f)) (Over.homMk c.fst sorry) (Over.homMk c.snd sorry),
            map := fun {c₁ c₂ : PullbackCone f g} (a : c₁ ⟶ c₂) ↦ { hom := Over.homMk a.hom sorry, w := sorry }, map_id := sorry,
            map_comp := sorry }
          c))))
  (Over.Hom.left
      (ConeMorphism.hom
        (Functor.map
            {
              obj := fun (c : PullbackCone f g) ↦
                BinaryFan.mk (P := Over.mk (c.fst ≫ f)) (Over.homMk c.fst sorry) (Over.homMk c.snd sorry),
              map := fun {c₁ c₂ : PullbackCone f g} (a : c₁ ⟶ c₂) ↦ { hom := Over.homMk a.hom sorry, w := sorry }, map_id := sorry,
              map_comp := sorry }
            (NatTrans.app (Iso.hom (NatIso.ofComponents (fun (c : PullbackCone f g) ↦ c.eta) sorry)) c) ≫
          NatTrans.app
            (Iso.hom
              (NatIso.ofComponents
                (fun (X_1 : 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) sorry,
                                  map := fun {c₁ c₂ : BinaryFan (Over.mk f) (Over.mk g)} (a : c₁ ⟶ c₂) ↦
                                    { hom := Over.Hom.left a.hom, w := sorry :
                                      ConeMorphism (PullbackCone.mk (Over.Hom.left c₁.fst) (Over.Hom.left c₁.snd) sorry)
                                        (PullbackCone.mk (Over.Hom.left c₂.fst) (Over.Hom.left c₂.snd) sorry) },
                                  map_id := sorry, map_comp := sorry : 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 sorry) (Over.homMk c.snd sorry),
                                  map := fun {c₁ c₂ : PullbackCone f g} (a : c₁ ⟶ c₂) ↦
                                    { hom := Over.homMk a.hom sorry, w := sorry :
                                      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 sorry)
                                          (Over.homMk c₁.snd sorry))
                                        (BinaryFan.mk (P := Over.mk (c₂.fst ≫ f)) (Over.homMk c₂.fst sorry)
                                          (Over.homMk c₂.snd sorry)) },
                                  map_id := sorry, map_comp := sorry : PullbackCone f g ⥤ BinaryFan (Over.mk f) (Over.mk g) })
                              X_1))))
                      sorry)
                    sorry sorry)
                sorry))
            (Functor.obj
              {
                obj := fun (c : PullbackCone f g) ↦
                  BinaryFan.mk (P := Over.mk (c.fst ≫ f)) (Over.homMk c.fst sorry) (Over.homMk c.snd sorry),
                map := fun {c₁ c₂ : PullbackCone f g} (a : c₁ ⟶ c₂) ↦
                  { hom := Over.homMk a.hom sorry, w := sorry :
                    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 sorry) (Over.homMk c₁.snd sorry))
                      (BinaryFan.mk (P := Over.mk (c₂.fst ≫ f)) (Over.homMk c₂.fst sorry) (Over.homMk c₂.snd sorry)) },
                map_id := sorry, map_comp := sorry : PullbackCone f g ⥤ BinaryFan (Over.mk f) (Over.mk g) }
              c))) :
    Quiver.Hom.{v, u} (V := C)
      (Over.left.{v, u} (X := X)
        (Cone.pt (J := Discrete WalkingPair) (F := pair (Over.mk f) (Over.mk g))
          (Functor.obj
            {
              obj := fun (c : PullbackCone f g) ↦
                BinaryFan.mk (P := Over.mk (c.fst ≫ f)) (Over.homMk c.fst sorry) (Over.homMk c.snd sorry),
              map := fun {c₁ c₂ : PullbackCone f g} (a : c₁ ⟶ c₂) ↦ { hom := Over.homMk a.hom sorry, w := sorry }, map_id := sorry,
              map_comp := sorry }
            c)))
      (Over.left.{v, u} (X := X)
        (Cone.pt (J := Discrete WalkingPair) (F := pair (Over.mk f) (Over.mk g))
          (Functor.obj
            {
              obj := fun (c : PullbackCone f g) ↦
                BinaryFan.mk (P := Over.mk (c.fst ≫ f)) (Over.homMk c.fst sorry) (Over.homMk c.snd sorry),
              map := fun {c₁ c₂ : PullbackCone f g} (a : c₁ ⟶ c₂) ↦ { hom := Over.homMk a.hom sorry, w := sorry }, map_id := sorry,
              map_comp := sorry }
            c))))
  (Over.Hom.left
      (ConeMorphism.hom
        (𝟙
          (Functor.obj
            {
              obj := fun (c : PullbackCone f g) ↦
                BinaryFan.mk (P := Over.mk (c.fst ≫ f)) (Over.homMk c.fst sorry) (Over.homMk c.snd sorry),
              map := fun {c₁ c₂ : PullbackCone f g} (a : c₁ ⟶ c₂) ↦ { hom := Over.homMk a.hom sorry, w := sorry }, map_id := sorry,
              map_comp := sorry }
            c))) :
    Quiver.Hom.{v, u} (V := C)
      (Over.left.{v, u} (X := X)
        (Cone.pt (J := Discrete WalkingPair) (F := pair (Over.mk f) (Over.mk g))
          (Functor.obj
            {
              obj := fun (c : PullbackCone f g) ↦
                BinaryFan.mk (P := Over.mk (c.fst ≫ f)) (Over.homMk c.fst sorry) (Over.homMk c.snd sorry),
              map := fun {c₁ c₂ : PullbackCone f g} (a : c₁ ⟶ c₂) ↦ { hom := Over.homMk a.hom sorry, w := sorry }, map_id := sorry,
              map_comp := sorry }
            c)))
      (Over.left.{v, u} (X := X)
        (Cone.pt (J := Discrete WalkingPair) (F := pair (Over.mk f) (Over.mk g))
          (Functor.obj
            {
              obj := fun (c : PullbackCone f g) ↦
                BinaryFan.mk (P := Over.mk (c.fst ≫ f)) (Over.homMk c.fst sorry) (Over.homMk c.snd sorry),
              map := fun {c₁ c₂ : PullbackCone f g} (a : c₁ ⟶ c₂) ↦ { hom := Over.homMk a.hom sorry, w := sorry }, map_id := sorry,
              map_comp := sorry }
            c))))
Tactic: ext