I think this is a worthwhile goal in general, but not an easy one. From the concrete examples you give, I do think isinstance is almost equivalent to:
def isinstance[T](obj: object, type: type[T]) -> TypeNarrower[T]: ...
(Using my suggested name from PEP 724: Stricter Type Guards - #54 by Jelle).
It’s almost equivalent because isinstance also supports nested tuples of types, which you could possibly express with a set of overloads but it certainly wouldn’t look nice.
property is hard to replace fully because the @...setter pattern is difficult to express from a type system perspective. However, PEP 612 ParamSpec is quite possibly enough for type checkers with good descriptor support to avoid special-casing @classmethod and @staticmethod.