-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X : FintypeCat
h :
  ∀ (x : (uSwitch.obj X).obj),
    Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (uSwitch.obj X))
      (((@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
                      (NatTrans.app
                        (Iso.hom
                          (NatIso.ofComponents
                            (fun (X : FintypeCat.{u}) ↦
                              Iso.symm
                                ((equivEquivIso :
                                    (a : (uSwitch.obj (uSwitch.obj X)).obj ≃ X.obj) → uSwitch.obj (uSwitch.obj X) ≅ X)
                                  (Equiv.trans (uSwitch.obj X).uSwitchEquiv X.uSwitchEquiv)))
                            @uSwitchEquivalence._proof_2))
                        X) ≫
                    (NatIso.ofComponents
                            (fun (X : FintypeCat.{v}) ↦
                              (equivEquivIso :
                                  (a : ((uSwitch ⋙ uSwitch).obj X).obj ≃ ((𝟭 FintypeCat).obj X).obj) →
                                    (uSwitch ⋙ uSwitch).obj X ≅ (𝟭 FintypeCat).obj X)
                                (Equiv.trans (uSwitch.obj X).uSwitchEquiv X.uSwitchEquiv))
                            @uSwitchEquivalence._proof_3).hom.app
                      (uSwitch.obj X) :
                  uSwitch.obj X ⟶ uSwitch.obj X) :
              TypeCat.Fun (uSwitch.obj X).obj (uSwitch.obj X).obj) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (uSwitch.obj X)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (uSwitch.obj X))
          x :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (uSwitch.obj X))
      ((@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.obj X) : uSwitch.obj X ⟶ uSwitch.obj X) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (uSwitch.obj X)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (uSwitch.obj X))
          x :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (uSwitch.obj X))
⊢ Eq (α := uSwitch.obj X ⟶ uSwitch.obj X)
    (uSwitch.map
          (NatTrans.app
            (Iso.hom
              (NatIso.ofComponents
                (fun (X : FintypeCat.{u}) ↦
                  Iso.symm
                    ((equivEquivIso : (a : (uSwitch.obj (uSwitch.obj X)).obj ≃ X.obj) → uSwitch.obj (uSwitch.obj X) ≅ X)
                      (Equiv.trans (uSwitch.obj X).uSwitchEquiv X.uSwitchEquiv)))
                @uSwitchEquivalence._proof_2))
            X) ≫
        (NatIso.ofComponents
                (fun (X : FintypeCat.{v}) ↦
                  (equivEquivIso :
                      (a : ((uSwitch ⋙ uSwitch).obj X).obj ≃ ((𝟭 FintypeCat).obj X).obj) →
                        (uSwitch ⋙ uSwitch).obj X ≅ (𝟭 FintypeCat).obj X)
                    (Equiv.trans (uSwitch.obj X).uSwitchEquiv X.uSwitchEquiv))
                @uSwitchEquivalence._proof_3).hom.app
          (uSwitch.obj X) :
      uSwitch.obj X ⟶ uSwitch.obj X)
    (𝟙 (uSwitch.obj X) : uSwitch.obj X ⟶ uSwitch.obj X)

Tactic:
ext x