-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.TypeValuedFlat (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
inst_1 : HasFiniteLimits.{v, u} C
inst_2 : PreservesFiniteLimits F
X : C
x : F.obj X
Y : C
y : F.obj Y
f : X ⟶ Y
hf_1 : (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj X) → F.obj Y) x = y
g : X ⟶ Y
hf :
  Eq (α := F.obj Y) ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj X) → F.obj Y) x : F.obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) : (a : F.obj X) → F.obj Y) x : F.obj Y)
hg : (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) : (a : F.obj X) → F.obj Y) x = y
h : IsLimit (Fork.ofι (P := F.obj (equalizer f g)) (F.map (equalizer.ι f g)) ⋯) :=
  isLimitForkMapOfIsLimit F ⋯ (equalizerIsEqualizer f g)
h' : IsLimit (F := parallelPair (F.map f) (F.map g)) (LimitCone.cone Types.equalizerLimit) :=
  LimitCone.isLimit Types.equalizerLimit
⊢ Eq.{v + 1} (α :=
    Sigma.mk (β := fun (c : C) ↦ F.obj c) (equalizer f g)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (h'.conePointUniqueUpToIso h).hom :
            (a : (fun (X : Type w) ↦ X) Types.equalizerLimit.cone.pt) →
              (fun (X : Type w) ↦ X) (Fork.ofι (F.map (equalizer.ι f g)) ⋯).pt)
          (Subtype.mk (p := fun (x : F.obj X) ↦
            Eq (α := (fun (X : Type w) ↦ X) (F.obj Y))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                    (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Y))
                  x :
                (fun (X : Type w) ↦ X) (F.obj Y))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
                    (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Y))
                  x :
                (fun (X : Type w) ↦ X) (F.obj Y)))
            x hf)) ⟶
      Sigma.mk (β := fun (c : C) ↦ F.obj c) Y y)
    (CategoryStruct.comp (Y := Sigma.mk (β := fun (c : C) ↦ F.obj c) X x)
      (Subtype.mk (p :=
        fun
          (f_1 :
            Sigma.fst (β := fun (c : C) ↦ F.obj c)
                (Sigma.mk (β := fun (c : C) ↦ F.obj c) (equalizer f g)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (h'.conePointUniqueUpToIso h).hom :
                      (a : (fun (X : Type w) ↦ X) Types.equalizerLimit.cone.pt) →
                        (fun (X : Type w) ↦ X) (Fork.ofι (F.map (equalizer.ι f g)) ⋯).pt)
                    (Subtype.mk (p := fun (x : F.obj X) ↦
                      Eq (α := (fun (X : Type w) ↦ X) (F.obj Y))
                        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                              (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Y))
                            x :
                          (fun (X : Type w) ↦ X) (F.obj Y))
                        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
                              (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Y))
                            x :
                          (fun (X : Type w) ↦ X) (F.obj Y)))
                      x hf))) ⟶
              (Sigma.mk (β := fun (c : C) ↦ F.obj c) X x).fst (β := fun (c : C) ↦ F.obj c)) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f_1) :
              (a :
                  (fun (X : Type w) ↦ X)
                    (F.obj
                      ⟨equalizer f g,
                          (ConcreteCategory.hom (h'.conePointUniqueUpToIso h).hom :
                              (a : (fun (X : Type w) ↦ X) Types.equalizerLimit.cone.pt) →
                                (fun (X : Type w) ↦ X) (Fork.ofι (F.map (equalizer.ι f g)) ⋯).pt)
                            ⟨x, hf⟩⟩.fst)) →
                (fun (X : Type w) ↦ X) (F.obj ⟨X, x⟩.fst))
            (Sigma.snd (β := fun (c : C) ↦ F.obj c)
              (Sigma.mk (β := fun (c : C) ↦ F.obj c) (equalizer f g)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (h'.conePointUniqueUpToIso h).hom :
                    (a : (fun (X : Type w) ↦ X) Types.equalizerLimit.cone.pt) →
                      (fun (X : Type w) ↦ X) (Fork.ofι (F.map (equalizer.ι f g)) ⋯).pt)
                  (Subtype.mk (p := fun (x : F.obj X) ↦
                    Eq (α := (fun (X : Type w) ↦ X) (F.obj Y))
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                            (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Y))
                          x :
                        (fun (X : Type w) ↦ X) (F.obj Y))
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
                            (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Y))
                          x :
                        (fun (X : Type w) ↦ X) (F.obj Y)))
                    x hf)))) =
          (Sigma.mk (β := fun (c : C) ↦ F.obj c) X x).snd (β := fun (c : C) ↦ F.obj c))
        (equalizer.ι f g) ⋯)
      (Subtype.mk (p :=
        fun
          (f :
            (Sigma.mk (β := fun (c : C) ↦ F.obj c) X x).fst (β := fun (c : C) ↦ F.obj c) ⟶
              (Sigma.mk (β := fun (c : C) ↦ F.obj c) Y y).fst (β := fun (c : C) ↦ F.obj c)) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type w) ↦ X) (F.obj ⟨X, x⟩.fst)) → (fun (X : Type w) ↦ X) (F.obj ⟨Y, y⟩.fst))
            ((Sigma.mk (β := fun (c : C) ↦ F.obj c) X x).snd (β := fun (c : C) ↦ F.obj c)) =
          (Sigma.mk (β := fun (c : C) ↦ F.obj c) Y y).snd (β := fun (c : C) ↦ F.obj c))
        f hf_1))
    (CategoryStruct.comp (Y := Sigma.mk (β := fun (c : C) ↦ F.obj c) X x)
      (Subtype.mk (p :=
        fun
          (f_1 :
            Sigma.fst (β := fun (c : C) ↦ F.obj c)
                (Sigma.mk (β := fun (c : C) ↦ F.obj c) (equalizer f g)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (h'.conePointUniqueUpToIso h).hom :
                      (a : (fun (X : Type w) ↦ X) Types.equalizerLimit.cone.pt) →
                        (fun (X : Type w) ↦ X) (Fork.ofι (F.map (equalizer.ι f g)) ⋯).pt)
                    (Subtype.mk (p := fun (x : F.obj X) ↦
                      Eq (α := (fun (X : Type w) ↦ X) (F.obj Y))
                        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                              (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Y))
                            x :
                          (fun (X : Type w) ↦ X) (F.obj Y))
                        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
                              (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Y))
                            x :
                          (fun (X : Type w) ↦ X) (F.obj Y)))
                      x hf))) ⟶
              (Sigma.mk (β := fun (c : C) ↦ F.obj c) X x).fst (β := fun (c : C) ↦ F.obj c)) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f_1) :
              (a :
                  (fun (X : Type w) ↦ X)
                    (F.obj
                      ⟨equalizer f g,
                          (ConcreteCategory.hom (h'.conePointUniqueUpToIso h).hom :
                              (a : (fun (X : Type w) ↦ X) Types.equalizerLimit.cone.pt) →
                                (fun (X : Type w) ↦ X) (Fork.ofι (F.map (equalizer.ι f g)) ⋯).pt)
                            ⟨x, hf⟩⟩.fst)) →
                (fun (X : Type w) ↦ X) (F.obj ⟨X, x⟩.fst))
            (Sigma.snd (β := fun (c : C) ↦ F.obj c)
              (Sigma.mk (β := fun (c : C) ↦ F.obj c) (equalizer f g)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (h'.conePointUniqueUpToIso h).hom :
                    (a : (fun (X : Type w) ↦ X) Types.equalizerLimit.cone.pt) →
                      (fun (X : Type w) ↦ X) (Fork.ofι (F.map (equalizer.ι f g)) ⋯).pt)
                  (Subtype.mk (p := fun (x : F.obj X) ↦
                    Eq (α := (fun (X : Type w) ↦ X) (F.obj Y))
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                            (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Y))
                          x :
                        (fun (X : Type w) ↦ X) (F.obj Y))
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
                            (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Y))
                          x :
                        (fun (X : Type w) ↦ X) (F.obj Y)))
                    x hf)))) =
          (Sigma.mk (β := fun (c : C) ↦ F.obj c) X x).snd (β := fun (c : C) ↦ F.obj c))
        (equalizer.ι f g) ⋯)
      (Subtype.mk (p :=
        fun
          (f :
            (Sigma.mk (β := fun (c : C) ↦ F.obj c) X x).fst (β := fun (c : C) ↦ F.obj c) ⟶
              (Sigma.mk (β := fun (c : C) ↦ F.obj c) Y y).fst (β := fun (c : C) ↦ F.obj c)) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type w) ↦ X) (F.obj ⟨X, x⟩.fst)) → (fun (X : Type w) ↦ X) (F.obj ⟨Y, y⟩.fst))
            ((Sigma.mk (β := fun (c : C) ↦ F.obj c) X x).snd (β := fun (c : C) ↦ F.obj c)) =
          (Sigma.mk (β := fun (c : C) ↦ F.obj c) Y y).snd (β := fun (c : C) ↦ F.obj c))
        g hg))
have w : Eq.{v + 1} (α :=
  Sigma.fst (β := fun (c : C) ↦ F.obj c)
      (Sigma.mk (β := fun (c : C) ↦ F.obj c) (equalizer f g)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (h'.conePointUniqueUpToIso h).hom :
            (a : (fun (X : Type w) ↦ X) Types.equalizerLimit.cone.pt) →
              (fun (X : Type w) ↦ X) (Fork.ofι (F.map (equalizer.ι f g)) sorry).pt)
          (Subtype.mk (p := fun (x : F.obj X) ↦
            Eq (α := (fun (X : Type w) ↦ X) (F.obj Y))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                    (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Y))
                  x :
                (fun (X : Type w) ↦ X) (F.obj Y))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
                    (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Y))
                  x :
                (fun (X : Type w) ↦ X) (F.obj Y)))
            x hf))) ⟶
    (Sigma.mk (β := fun (c : C) ↦ F.obj c) Y y).fst (β := fun (c : C) ↦ F.obj c))
  (↑(CategoryStruct.comp (Y := Sigma.mk (β := fun (c : C) ↦ F.obj c) X x)
        (Subtype.mk (p :=
          fun
            (f_1 :
              Sigma.fst (β := fun (c : C) ↦ F.obj c)
                  (Sigma.mk (β := fun (c : C) ↦ F.obj c) (equalizer f g)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (h'.conePointUniqueUpToIso h).hom :
                        (a : (fun (X : Type w) ↦ X) Types.equalizerLimit.cone.pt) →
                          (fun (X : Type w) ↦ X) (Fork.ofι (F.map (equalizer.ι f g)) sorry).pt)
                      (Subtype.mk (p := fun (x : F.obj X) ↦
                        Eq (α := (fun (X : Type w) ↦ X) (F.obj Y))
                          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                                (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Y))
                              x :
                            (fun (X : Type w) ↦ X) (F.obj Y))
                          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
                                (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Y))
                              x :
                            (fun (X : Type w) ↦ X) (F.obj Y)))
                        x hf))) ⟶
                (Sigma.mk (β := fun (c : C) ↦ F.obj c) X x).fst (β := fun (c : C) ↦ F.obj c)) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f_1) :
                (a :
                    (fun (X : Type w) ↦ X)
                      (F.obj
                        ⟨equalizer f g,
                            (ConcreteCategory.hom (h'.conePointUniqueUpToIso h).hom :
                                (a : (fun (X : Type w) ↦ X) Types.equalizerLimit.cone.pt) →
                                  (fun (X : Type w) ↦ X) (Fork.ofι (F.map (equalizer.ι f g)) sorry).pt)
                              ⟨x, hf⟩⟩.fst)) →
                  (fun (X : Type w) ↦ X) (F.obj ⟨X, x⟩.fst))
              (Sigma.snd (β := fun (c : C) ↦ F.obj c)
                (Sigma.mk (β := fun (c : C) ↦ F.obj c) (equalizer f g)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (h'.conePointUniqueUpToIso h).hom :
                      (a : (fun (X : Type w) ↦ X) Types.equalizerLimit.cone.pt) →
                        (fun (X : Type w) ↦ X) (Fork.ofι (F.map (equalizer.ι f g)) sorry).pt)
                    (Subtype.mk (p := fun (x : F.obj X) ↦
                      Eq (α := (fun (X : Type w) ↦ X) (F.obj Y))
                        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                              (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Y))
                            x :
                          (fun (X : Type w) ↦ X) (F.obj Y))
                        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
                              (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Y))
                            x :
                          (fun (X : Type w) ↦ X) (F.obj Y)))
                      x hf)))) =
            (Sigma.mk (β := fun (c : C) ↦ F.obj c) X x).snd (β := fun (c : C) ↦ F.obj c))
          (equalizer.ι f g) sorry)
        (Subtype.mk (p :=
          fun
            (f :
              (Sigma.mk (β := fun (c : C) ↦ F.obj c) X x).fst (β := fun (c : C) ↦ F.obj c) ⟶
                (Sigma.mk (β := fun (c : C) ↦ F.obj c) Y y).fst (β := fun (c : C) ↦ F.obj c)) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                (a : (fun (X : Type w) ↦ X) (F.obj ⟨X, x⟩.fst)) → (fun (X : Type w) ↦ X) (F.obj ⟨Y, y⟩.fst))
              ((Sigma.mk (β := fun (c : C) ↦ F.obj c) X x).snd (β := fun (c : C) ↦ F.obj c)) =
            (Sigma.mk (β := fun (c : C) ↦ F.obj c) Y y).snd (β := fun (c : C) ↦ F.obj c))
          f hf_1)) :
    ⟨equalizer f g,
          (ConcreteCategory.hom (h'.conePointUniqueUpToIso h).hom :
              (a : (fun (X : Type w) ↦ X) Types.equalizerLimit.cone.pt) →
                (fun (X : Type w) ↦ X) (Fork.ofι (F.map (equalizer.ι f g)) sorry).pt)
            ⟨x, hf⟩⟩.fst ⟶
      ⟨Y, y⟩.fst)
  (↑(CategoryStruct.comp (Y := Sigma.mk (β := fun (c : C) ↦ F.obj c) X x)
        (Subtype.mk (p :=
          fun
            (f_1 :
              Sigma.fst (β := fun (c : C) ↦ F.obj c)
                  (Sigma.mk (β := fun (c : C) ↦ F.obj c) (equalizer f g)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (h'.conePointUniqueUpToIso h).hom :
                        (a : (fun (X : Type w) ↦ X) Types.equalizerLimit.cone.pt) →
                          (fun (X : Type w) ↦ X) (Fork.ofι (F.map (equalizer.ι f g)) sorry).pt)
                      (Subtype.mk (p := fun (x : F.obj X) ↦
                        Eq (α := (fun (X : Type w) ↦ X) (F.obj Y))
                          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                                (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Y))
                              x :
                            (fun (X : Type w) ↦ X) (F.obj Y))
                          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
                                (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Y))
                              x :
                            (fun (X : Type w) ↦ X) (F.obj Y)))
                        x hf))) ⟶
                (Sigma.mk (β := fun (c : C) ↦ F.obj c) X x).fst (β := fun (c : C) ↦ F.obj c)) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f_1) :
                (a :
                    (fun (X : Type w) ↦ X)
                      (F.obj
                        ⟨equalizer f g,
                            (ConcreteCategory.hom (h'.conePointUniqueUpToIso h).hom :
                                (a : (fun (X : Type w) ↦ X) Types.equalizerLimit.cone.pt) →
                                  (fun (X : Type w) ↦ X) (Fork.ofι (F.map (equalizer.ι f g)) sorry).pt)
                              ⟨x, hf⟩⟩.fst)) →
                  (fun (X : Type w) ↦ X) (F.obj ⟨X, x⟩.fst))
              (Sigma.snd (β := fun (c : C) ↦ F.obj c)
                (Sigma.mk (β := fun (c : C) ↦ F.obj c) (equalizer f g)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (h'.conePointUniqueUpToIso h).hom :
                      (a : (fun (X : Type w) ↦ X) Types.equalizerLimit.cone.pt) →
                        (fun (X : Type w) ↦ X) (Fork.ofι (F.map (equalizer.ι f g)) sorry).pt)
                    (Subtype.mk (p := fun (x : F.obj X) ↦
                      Eq (α := (fun (X : Type w) ↦ X) (F.obj Y))
                        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                              (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Y))
                            x :
                          (fun (X : Type w) ↦ X) (F.obj Y))
                        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
                              (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Y))
                            x :
                          (fun (X : Type w) ↦ X) (F.obj Y)))
                      x hf)))) =
            (Sigma.mk (β := fun (c : C) ↦ F.obj c) X x).snd (β := fun (c : C) ↦ F.obj c))
          (equalizer.ι f g) sorry)
        (Subtype.mk (p :=
          fun
            (f :
              (Sigma.mk (β := fun (c : C) ↦ F.obj c) X x).fst (β := fun (c : C) ↦ F.obj c) ⟶
                (Sigma.mk (β := fun (c : C) ↦ F.obj c) Y y).fst (β := fun (c : C) ↦ F.obj c)) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                (a : (fun (X : Type w) ↦ X) (F.obj ⟨X, x⟩.fst)) → (fun (X : Type w) ↦ X) (F.obj ⟨Y, y⟩.fst))
              ((Sigma.mk (β := fun (c : C) ↦ F.obj c) X x).snd (β := fun (c : C) ↦ F.obj c)) =
            (Sigma.mk (β := fun (c : C) ↦ F.obj c) Y y).snd (β := fun (c : C) ↦ F.obj c))
          g hg)) :
    ⟨equalizer f g,
          (ConcreteCategory.hom (h'.conePointUniqueUpToIso h).hom :
              (a : (fun (X : Type w) ↦ X) Types.equalizerLimit.cone.pt) →
                (fun (X : Type w) ↦ X) (Fork.ofι (F.map (equalizer.ι f g)) sorry).pt)
            ⟨x, hf⟩⟩.fst ⟶
      ⟨Y, y⟩.fst)
Tactic: ext