-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Examples (goal)
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)
⊢ (@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)
have 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)
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]