Lean has like super-hyper-turbo uniform function call syntax where the "receiver" doesn't have to actually be the first argument to the function, which is extremely sickos.png and a lot of fun, but also very confusing when you're learning since `x.map y` might desugar to either `map x y` or `map y x` depending how the types line up