-- Module: Mathlib.CategoryTheory.Functor.TypeValuedFlat
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
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)) ⋯).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)) ⋯).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)) :
      ⟨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 ⟶
        ⟨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)) ⋯).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)) :
      ⟨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 ⟶
        ⟨Y, y⟩.fst)
⊢ 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))

Tactic:
ext