-- Lean 4 proof step from Mathlib.CategoryTheory.FintypeCat (goal)
Goal:
X : FintypeCat
⊢ 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)
have 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))
Tactic: ext x