-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
X Y : C
f g : X ⟶ Y
x : (F.obj X).obj
h :
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
    ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _ (F.map f) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
    ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _ (F.map g) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
⊢ (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _ (F.map (equalizer.ι f g) : F.obj (equalizer f g) ⟶ F.obj X) :
        (a : (F.obj (equalizer f g)).obj) → (F.obj X).obj)
      ((Equiv.symm
              (Equiv.trans (Iso.toEquiv (PreservesEqualizer.iso (F ⋙ FintypeCat.incl) f g))
                (Iso.toEquiv
                  (Types.equalizerIso ((F.map f).hom (F := ObjectProperty.FullSubcategory.obj))
                    ((F.map g).hom (F := ObjectProperty.FullSubcategory.obj))))) :
            (a :
                { x : (F.obj X).obj //
                  (ConcreteCategory.hom (F.map f) : (a : (F.obj X).obj) → (F.obj Y).obj) x =
                    (ConcreteCategory.hom (F.map g) : (a : (F.obj X).obj) → (F.obj Y).obj) x }) →
              (F.obj (equalizer f g)).obj)
          (Subtype.mk (p := fun (x : (F.obj X).obj) ↦
            Eq (α := (F.obj Y).obj)
              ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
                      (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                      (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                        (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
                      _ _ _ (F.map f) :
                    (a : (F.obj X).obj) → (F.obj Y).obj)
                  x :
                (F.obj Y).obj)
              ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
                      (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                      (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                        (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
                      _ _ _ (F.map g) :
                    (a : (F.obj X).obj) → (F.obj Y).obj)
                  x :
                (F.obj Y).obj))
            x h) :
        (F.obj (equalizer f g)).obj) =
    x
have change : (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.inv
            (Types.equalizerIso ((parallelPair f g ⋙ F ⋙ FintypeCat.incl).map WalkingParallelPairHom.left)
              ((parallelPair f g ⋙ F ⋙ FintypeCat.incl).map WalkingParallelPairHom.right)) ≫
          CategoryStruct.comp (Y := (F ⋙ FintypeCat.incl).obj (equalizer f g))
            (ConeMorphism.hom
              ((Cone.postcomposeEquivalence
                        (diagramIsoParallelPair (parallelPair f g ⋙ F ⋙ FintypeCat.incl))).symm.inverse.map
                (IsLimit.liftConeMorphism (isLimitOfPreserves (F ⋙ FintypeCat.incl) (equalizerIsEqualizer f g))
                  ((Cone.postcomposeEquivalence
                            (diagramIsoParallelPair (parallelPair f g ⋙ F ⋙ FintypeCat.incl))).symm.functor.obj
                    (limit.cone (parallelPair ((F ⋙ FintypeCat.incl).map f) ((F ⋙ FintypeCat.incl).map g)))))))
            ((F ⋙ FintypeCat.incl).map (equalizer.ι f g))) :
      (a :
          (fun (X : Type w) ↦ X)
            { x : (parallelPair f g ⋙ F ⋙ FintypeCat.incl).obj WalkingParallelPair.zero //
              (ConcreteCategory.hom ((parallelPair f g ⋙ F ⋙ FintypeCat.incl).map WalkingParallelPairHom.left) :
                    (a :
                        (fun (X : Type w) ↦ X)
                          ((parallelPair f g ⋙ F ⋙ FintypeCat.incl).obj WalkingParallelPair.zero)) →
                      (fun (X : Type w) ↦ X) ((parallelPair f g ⋙ F ⋙ FintypeCat.incl).obj WalkingParallelPair.one))
                  x =
                (ConcreteCategory.hom ((parallelPair f g ⋙ F ⋙ FintypeCat.incl).map WalkingParallelPairHom.right) :
                    (a :
                        (fun (X : Type w) ↦ X)
                          ((parallelPair f g ⋙ F ⋙ FintypeCat.incl).obj WalkingParallelPair.zero)) →
                      (fun (X : Type w) ↦ X) ((parallelPair f g ⋙ F ⋙ FintypeCat.incl).obj WalkingParallelPair.one))
                  x }) →
        (fun (X : Type w) ↦ X) ((F ⋙ FintypeCat.incl).obj X))
    (Subtype.mk (p := fun (x : (F.obj X).obj) ↦
      Eq (α := (F.obj Y).obj)
        ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
                (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                  (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
                _ _ _ (F.map f) :
              (a : (F.obj X).obj) → (F.obj Y).obj)
            x :
          (F.obj Y).obj)
        ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
                (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                  (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
                _ _ _ (F.map g) :
              (a : (F.obj X).obj) → (F.obj Y).obj)
            x :
          (F.obj Y).obj))
      x h) =
  x
Tactic: change ((Types.equalizerIso _ _).inv ≫ _ ≫ (F ⋙ FintypeCat.incl).map (equalizer.ι f g)) _ = _