That's interesting, coming from the Lean language the analogous function - rw, or rewrite - is a real workhorse. It's often very useful to manipulate expression

That's interesting, coming from the Lean language the analogous function - rw, or rewrite - is a real workhorse. It's often very useful to manipulate expressions when proving things. Why do you think it's a code smell?