invalidInstImplicit.lean:1:9-1:12: error: invalid binder annotation, type is not a class instance Nat Note: Use the command `set_option checkBinderAnnotations false` to disable the check