There was already a question here of this type but I would like to ask more generally:
If I see some strange unicode symbols being used in Lean, is there a recommended way to find out how to type them, and finding out what they mean, other than asking here at Proof Assistants or at the Zulip chat?
Unicode character input is an editor feature, so this answer is specific to VSCode.
If you have a Lean file open in VSCode, you can hover over a unicode symbol to see what input commands are available. E.g., if you paste the character • and put your cursor over it, you get the tooltip Type • using \smul or \bub or \bu. This works whether or not the character is used in syntactically correct form.
You can see a list of all the supported input abbreviations in the VSCode plugin.
If you are using Emacs, then the corresponding command is C-u C-x =. This displays a buffer with lots of information about the character under point, including its Unicode name and to input: which shows you how to type it in the current input-mode.