-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
X Y : Action FintypeCat G
f : X ⟶ Y
g : G
y : (FintypeCat.imageComplement f.hom).obj
x : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V
h :
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.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 :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (InducedCategory.Hom.hom (F := ObjectProperty.FullSubcategory.obj) ((Y.ρ : (a : G) → End Y.V) g)) :
          (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) :
      (fun (X : Type u_1) ↦ X) Y.V.obj)
h₁ :
  (@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)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (InducedCategory.Hom.hom (F := ObjectProperty.FullSubcategory.obj) ((X.ρ : (a : G) → End X.V) g⁻¹)) :
            (a : (fun (X : Type u_1) ↦ X) X.V.obj) → (fun (X : Type u_1) ↦ X) X.V.obj)
          x :
        (fun (X : Type u_1) ↦ X) X.V.obj) =
    (↑y : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V)
⊢ 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))
    (↑y : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V)

Tactic:
use (X.ρ g⁻¹).hom x

Premises used: CategoryTheory.ConcreteCategory.hom, Action.ρ, Inv.inv, CategoryTheory.InducedCategory.Hom.hom, DFunLike.coe