-- 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
⊢ 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)

Tactic:
equalizer.condition f g

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.equalizer.condition, CategoryTheory.Limits.limit