-- 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)
calc :
  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))
            _ _ _ ((X.ρ : (a : G) → End X.V) g⁻¹ ≫ f.hom : X.V ⟶ Y.V) :
          (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)
            ((HMul.hMul (α := End Y.V) (β := End Y.V) ((Y.ρ : (a : G) → End Y.V) g⁻¹ : End Y.V)
                  ((Y.ρ : (a : G) → End Y.V) g : End Y.V)).hom
              (F := ObjectProperty.FullSubcategory.obj)) :
          (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)
calc₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((HMul.hMul (α := End Y.V) (β := End Y.V) ((Y.ρ : (a : G) → End Y.V) g⁻¹ : End Y.V)
                ((Y.ρ : (a : G) → End Y.V) g : End Y.V)).hom
            (F := ObjectProperty.FullSubcategory.obj)) :
        (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) =
    (↑y : (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)
      ((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)

Tactic:
calc (X.ρ g⁻¹ ≫ f.hom) x
          = ((Y.ρ g⁻¹ * Y.ρ g)).hom y.val := by rw [f.comm, FintypeCat.comp_apply, h]; rfl
        _ = y.val := by
          simp [← map_mul, inv_mul_cancel, Action.ρ_one, FintypeCat.id_hom]

Premises used: HMul.hMul, CategoryTheory.ConcreteCategory.hom, Action.ρ, Inv.inv, CategoryTheory.CategoryStruct.comp, Action.Hom.hom, CategoryTheory.InducedCategory.Hom.hom, Subtype.val, DFunLike.coe