-- Lean 4 proof step from Mathlib.CategoryTheory.FintypeCat (goal)
Goal:
X Y : FintypeCat
f : X ⟶ Y
x : (uSwitch.obj X).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)
have 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)
Tactic: simp only [uSwitch, uSwitchEquiv, Equiv.trans_apply, Equiv.ulift_apply]