!= is two bloody characters not one.
And now people are doing it for 3 characters.
With this kind of thing, you get all the text editing idiocy of combining characters (like emojis) for no benefit at all.
See: Text Editing Hates You Too https://lord.io/text-editing-hates-you-too/
Jetbrains, VSCode people, whomever: edit mode and presentation view. There are times when I think for a lot of people the traditional math style makes sense for reading, but when it comes to editing, it bothers the hell out of me too.
In addition to ligatures, you get IMO a better version of the "Mix & Match" idea: doc comments are rendered as normal proportional text.