-- 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 A B : C
f : A ⟶ X
g : B ⟶ X
a : (F.obj A).obj
b : (F.obj B).obj
h :
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
    ((@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 A)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        a :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
    ((@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 B)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        b :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
erw :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾fun (p : Types.PullbackObj (FintypeCat.incl.map (F.map f)) (FintypeCat.incl.map (F.map g))) ↦
            (↑p : (F ⋙ FintypeCat.incl).obj A × (F.obj B).obj).1) :
        (a :
            (fun (X : Type w) ↦ X)
              (Types.PullbackObj (FintypeCat.incl.map (F.map f)) (FintypeCat.incl.map (F.map g)))) →
          (fun (X : Type w) ↦ X) ((F ⋙ FintypeCat.incl).obj A))
      (Subtype.mk (p := fun (p : (F.obj A).obj × (F.obj B).obj) ↦
        Eq (α := (F.obj X).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 A).obj) → (F.obj X).obj)
              p.1 :
            (F.obj X).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 B).obj) → (F.obj X).obj)
              p.2 :
            (F.obj X).obj))
        (a, b) h) =
    a
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((Types.pullbackIsoPullback (FintypeCat.incl.map (F.map f)) (FintypeCat.incl.map (F.map g))).inv ≫
            CategoryStruct.comp (Y := (F ⋙ FintypeCat.incl).obj (pullback f g))
              (Iso.inv (PreservesPullback.iso (F ⋙ FintypeCat.incl) f g))
              ((F ⋙ FintypeCat.incl).map (pullback.fst f g))) :
        (a :
            (fun (X : Type w) ↦ X)
              (Types.PullbackObj (FintypeCat.incl.map (F.map f)) (FintypeCat.incl.map (F.map g)))) →
          (fun (X : Type w) ↦ X) ((F ⋙ FintypeCat.incl).obj A))
      (Subtype.mk (p := fun (p : (F.obj A).obj × (F.obj B).obj) ↦
        Eq (α := (F.obj X).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 A).obj) → (F.obj X).obj)
              p.1 :
            (F.obj X).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 B).obj) → (F.obj X).obj)
              p.2 :
            (F.obj X).obj))
        (a, b) h) =
    a

Tactic:
erw [PreservesPullback.iso_inv_fst, Types.pullbackIsoPullback_inv_fst]

Premises used: CategoryTheory.Limits.PreservesPullback.iso_inv_fst, CategoryTheory.Limits.Types.pullbackIsoPullback_inv_fst