-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
X A : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h :
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (selfProd F 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 u) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (selfProd F X)))
        a :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (selfProd F X)))
    (mkSelfProdFib F X : (F.obj (selfProd F X)).obj)
inst_3 : IsConnected.{u₁, u₂} A
b : (F.obj A).obj
t : (F.obj X).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 (selfProdProj u t)) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
            (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))
              _ _ _
              (CategoryStruct.comp (Y := F.obj (piObj.{w, u₂, u₁} fun (x : (F.obj X).obj) ↦ X))
                  (F.map
                    (Pi.map' (⇑(fiberPerm h b) : (a : (F.obj X).obj) → (F.obj X).obj) fun (x : (F.obj X).obj) ↦ 𝟙 X))
                  (F.map (Pi.π (fun (x : (F.obj X).obj) ↦ X) t)) :
                F.obj (piObj.{w, u₂, u₁} fun (x : (F.obj X).obj) ↦ X) ⟶ F.obj X) :
            TypeCat.Fun (F.obj (piObj.{w, u₂, u₁} fun (x : (F.obj X).obj) ↦ X)).obj (F.obj X).obj) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (∏ᶜ fun (x : (F.obj X).obj) ↦ X))) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        (mkSelfProdFib F X : (F.obj (selfProd F X)).obj) :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
⊢ 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 (selfProdProj u t)) :
          (a : (F.obj A).obj) → (F.obj X).obj)
        b :
      (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 (Pi.π (fun (x : (F.obj X).obj) ↦ X) t) :
              F.obj (piObj.{w, u₂, u₁} fun (x : (F.obj X).obj) ↦ X) ⟶ F.obj X) :
          (a : (F.obj (∏ᶜ fun (x : (F.obj X).obj) ↦ X)).obj) → (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
                    (Pi.map' (⇑(fiberPerm h b) : (a : (F.obj X).obj) → (F.obj X).obj) fun (j : (F.obj X).obj) ↦
                      Iso.hom (Iso.refl X)) :
                  F.obj (selfProd F X) ⟶ F.obj (selfProd F X)) :
              (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (selfProd F X))) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (selfProd F X)))
            (mkSelfProdFib F X) :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (selfProd F X))) :
      (F.obj X).obj)

Tactic:
convert_to F.map (selfProdProj u t) b =
      (F.map (Pi.map' (fiberPerm h b) fun _ ↦ 𝟙 X) ≫
      F.map (Pi.π (fun _ ↦ X) t)) (mkSelfProdFib F X)

Premises used: CategoryTheory.ConcreteCategory.hom, _private.0.CategoryTheory.PreGaloisCategory.fiberPerm, CategoryTheory.Limits.Pi.map', CategoryTheory.Limits.Pi.π, _private.0.CategoryTheory.PreGaloisCategory.mkSelfProdFib, CategoryTheory.Functor.map, _private.0.CategoryTheory.PreGaloisCategory.selfProdProj, CategoryTheory.CategoryStruct.comp, DFunLike.coe