-- Module: Mathlib.CategoryTheory.Galois.GaloisObjects
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
A B : C
f : A ⟶ B
inst_2 : IsConnected.{u₁, u₂} A
inst_3 : IsGalois.{u₁, u₂} B
σ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).obj
τ : Aut B
hτ : f ≫ τ.hom = σ.hom ≫ f
refine_3 :
  Eq.{u₂ + 1} (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B))
    ((fun (f_1 : Aut B) ↦
        ((@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_1.hom) :
              (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B))
            ((@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 B))
                a :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B)) :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B)))
      τ)
    ((fun (f_1 : Aut B) ↦
        ((@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_1.hom) :
              (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B))
            ((@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 B))
                a :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B)) :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B)))
      (((evaluationEquivOfIsGalois F B
              ((@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 B))
                a)).symm :
          (a : (F.obj B).obj) → Aut B)
        ((@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 (σ.hom ≫ f)) :
              (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B))
            a :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B))))
⊢ τ =
    ((evaluationEquivOfIsGalois F B
            ((@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 B))
              a)).symm :
        (a : (F.obj B).obj) → Aut B)
      ((@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 (σ.hom ≫ f)) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B))
          a :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B))

Tactic:
apply evaluation_aut_injective_of_isConnected F B (F.map f a)

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Functor.map, DFunLike.coe, CategoryTheory.PreGaloisCategory.evaluation_aut_injective_of_isConnected