-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X Y : FintypeCat
f : X ⟶ Y
x : (uSwitch.obj X).obj
simp :
  Eq (α := Y.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 :
          (a : X.obj) → Y.obj)
        ((Equiv.symm (Fintype.equivFin X.obj) : (a : Fin (Fintype.card X.obj)) → X.obj) x.down : X.obj) :
      Y.obj)
    ((Equiv.symm (Fintype.equivFin Y.obj) : (a : Fin (Fintype.card Y.obj)) → Y.obj)
        (ULift.down.{v, 0}
          ((@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))
                _ _ _
                (homMk
                    (ULift.up ∘
                      Function.comp (β := Y.obj) (⇑(Fintype.equivFin Y.obj) : (a : Y.obj) → Fin (Fintype.card Y.obj))
                        (Function.comp (β := X.obj)
                          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                                (f.hom (F := ObjectProperty.FullSubcategory.obj))) :
                            (a : X.obj) → Y.obj)
                          ((⇑(Equiv.symm (Fintype.equivFin X.obj)) : (a : Fin (Fintype.card X.obj)) → X.obj) ∘
                            ULift.down))) :
                  of (ULift.{v, 0} (Fin (Fintype.card.{u} X.obj))) ⟶ of (ULift.{v, 0} (Fin (Fintype.card.{u} Y.obj)))) :
              (a : ULift.{v, 0} (Fin (Fintype.card X.obj))) → ULift.{v, 0} (Fin (Fintype.card Y.obj)))
            x)) :
      Y.obj)
⊢ Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y)
    ((@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 :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y)
        ((X.uSwitchEquiv : (a : (uSwitch.obj X).obj) → X.obj) x : X.obj) :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y)
    ((Y.uSwitchEquiv : (a : (uSwitch.obj Y).obj) → Y.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))
              _ _ _ (uSwitch.map f) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (uSwitch.obj X)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (uSwitch.obj Y))
          x) :
      Y.obj)

Tactic:
simp only [uSwitch, uSwitchEquiv, Equiv.trans_apply, Equiv.ulift_apply]

Premises used: Equiv.ulift_apply, Equiv.trans_apply, FintypeCat.uSwitch, FintypeCat.uSwitchEquiv