-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X Y : FintypeCat
f : X ⟶ Y
x : X.obj
rw :
  Eq.{u + 1} (α := Y.obj)
    ((Y.uSwitchEquiv : (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (uSwitch.obj Y)) → 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.uSwitchEquiv.symm : (a : X.obj) → (uSwitch.obj X).obj) x : (uSwitch.obj X).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))
            _ _ _ f :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y)
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y)
rw₁ :
  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 : (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.uSwitchEquiv.symm : (a : X.obj) → (uSwitch.obj X).obj) x) :
          X.obj) :
      (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 :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y)
rw₂ rw₃ :
  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 : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y)
        x :
      (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 :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y)
⊢ Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (uSwitch.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))
            _ _ _ (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.uSwitchEquiv.symm : (a : X.obj) → (uSwitch.obj X).obj) x : (uSwitch.obj X).obj) :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (uSwitch.obj Y))
    ((Y.uSwitchEquiv.symm : (a : Y.obj) → (uSwitch.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))
              _ _ _ f :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y)
          x) :
      (uSwitch.obj Y).obj)

Tactic:
rw [← Equiv.apply_eq_iff_eq_symm_apply, ← uSwitchEquiv_naturality f,
    Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, FintypeCat.uSwitchEquiv_naturality, Equiv.apply_eq_iff_eq_symm_apply