-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
X Y : Action FintypeCat G
f : X ⟶ Y
⊢ ∀ (x y : G),
    (FintypeCat.homMk fun (y_1 : (FintypeCat.imageComplement f.hom).obj) ↦
        Subtype.mk (p := fun (x : Y.V.obj) ↦
          Membership.mem (γ := Set ((fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V))
            (Set.range (ι := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V)
                (⇑(@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.hom) :
                  (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V) →
                    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V))ᶜ
            x)
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (InducedCategory.Hom.hom (F := ObjectProperty.FullSubcategory.obj)
                  ((Y.ρ : (a : G) → End Y.V) (x * y))) :
              (a : (fun (X : Type u_1) ↦ X) Y.V.obj) → (fun (X : Type u_1) ↦ X) Y.V.obj)
            (↑y_1 : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V))
          ⋯) =
      HMul.hMul (α := End (FintypeCat.imageComplement f.hom))
        (FintypeCat.homMk fun (y : (FintypeCat.imageComplement f.hom).obj) ↦
          Subtype.mk (p := fun (x : Y.V.obj) ↦
            Membership.mem (γ := Set ((fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V))
              (Set.range (ι := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V)
                  (⇑(@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.hom) :
                    (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V) →
                      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V))ᶜ
              x)
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (InducedCategory.Hom.hom (F := ObjectProperty.FullSubcategory.obj) ((Y.ρ : (a : G) → End Y.V) x)) :
                (a : (fun (X : Type u_1) ↦ X) Y.V.obj) → (fun (X : Type u_1) ↦ X) Y.V.obj)
              (↑y : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V))
            ⋯)
        (FintypeCat.homMk fun (y_1 : (FintypeCat.imageComplement f.hom).obj) ↦
          Subtype.mk (p := fun (x : Y.V.obj) ↦
            Membership.mem (γ := Set ((fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V))
              (Set.range (ι := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V)
                  (⇑(@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.hom) :
                    (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V) →
                      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V))ᶜ
              x)
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (InducedCategory.Hom.hom (F := ObjectProperty.FullSubcategory.obj) ((Y.ρ : (a : G) → End Y.V) y)) :
                (a : (fun (X : Type u_1) ↦ X) Y.V.obj) → (fun (X : Type u_1) ↦ X) Y.V.obj)
              (↑y_1 : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V))
            ⋯)

Tactic:
aesop