-- 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 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))
⊢ (@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 (pullback.fst f g) : F.obj (pullback f g) ⟶ F.obj A) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (pullback f g))) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
      (((Equiv.symm (fiberPullbackEquiv F f g) :
              { p : (F.obj A).obj × (F.obj B).obj //
                  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))
                        p.1 :
                      (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))
                        p.2 :
                      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) } ≃
                (F.obj (pullback f g)).obj) :
            (a :
                { p : (F.obj A).obj × (F.obj B).obj //
                  (ConcreteCategory.hom (F.map f) :
                        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
                          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
                      p.1 =
                    (ConcreteCategory.hom (F.map g) :
                        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B)) →
                          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
                      p.2 }) →
              (F.obj (pullback f g)).obj)
          (Subtype.mk (p := fun (p : (F.obj A).obj × (F.obj B).obj) ↦
            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))
                  p.1 :
                (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))
                  p.2 :
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)))
            (a, b) h) :
        (F.obj (pullback f g)).obj) =
    a
have simp : (@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 (pullback.fst f g) : F.obj (pullback f g) ⟶ F.obj A) :
      (a : (F.obj (pullback f g)).obj) → (F.obj A).obj)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (PreservesPullback.iso (F ⋙ FintypeCat.incl) f g)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Types.pullbackIsoPullback ((F.map f).hom (F := ObjectProperty.FullSubcategory.obj))
                ((F.map g).hom (F := ObjectProperty.FullSubcategory.obj))).inv).toFun
        (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: simp only [fiberPullbackEquiv, comp_obj, FintypeCat.incl_obj, Functor.comp_map, Iso.toEquiv_comp,
    Equiv.symm_trans_apply, Iso.toEquiv_symm_fun]