-- Module: Mathlib.CategoryTheory.Galois.Basic
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))
erw :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾Subtype.val (p := fun (x : (F ⋙ FintypeCat.incl).obj X) ↦
              Eq (α := (fun (X : Type w) ↦ X) ((parallelPair f g ⋙ F ⋙ FintypeCat.incl).obj WalkingParallelPair.one))
                ((ConcreteCategory.hom (FC := TypeCat.Fun)
                        ((parallelPair f g ⋙ F ⋙ FintypeCat.incl).map WalkingParallelPairHom.left) :
                      (a : (fun (X : Type w) ↦ X) ((F ⋙ FintypeCat.incl).obj X)) →
                        (fun (X : Type w) ↦ X) ((parallelPair f g ⋙ F ⋙ FintypeCat.incl).obj WalkingParallelPair.one))
                    x :
                  (fun (X : Type w) ↦ X) ((parallelPair f g ⋙ F ⋙ FintypeCat.incl).obj WalkingParallelPair.one))
                ((ConcreteCategory.hom (FC := TypeCat.Fun)
                        ((parallelPair f g ⋙ F ⋙ FintypeCat.incl).map WalkingParallelPairHom.right) :
                      (a : (fun (X : Type w) ↦ X) ((F ⋙ FintypeCat.incl).obj X)) →
                        (fun (X : Type w) ↦ X) ((parallelPair f g ⋙ F ⋙ FintypeCat.incl).obj WalkingParallelPair.one))
                    x :
                  (fun (X : Type w) ↦ X) ((parallelPair f g ⋙ F ⋙ FintypeCat.incl).obj WalkingParallelPair.one)))) :
        (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
⊢ (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:
erw [PreservesEqualizer.iso_inv_ι, Types.equalizerIso_inv_comp_ι]

Premises used: CategoryTheory.Limits.Types.equalizerIso_inv_comp_ι, CategoryTheory.Limits.PreservesEqualizer.iso_inv_ι