The funny symbol is called sqsubseteq and you can find that out by drawing it here: https://detexify.kirelabs.org/classify.html

But I agree that there needs to be a way to type latex Symbols quicker. The Lean Community did this quite well: hovering over a symbol in the docs gives you the correct ascii name.