Julia Markus Himmel reworks order instances across Lean core types