And in "Lean style", refl proofs are a bit distasteful from a software engineering point of view because they pierce through the API of a mathematical object. (In the language of OOP, it can break encapsulation.)

It tends to be a good idea to give some definition, then prove a bunch of lemmas that characterize the object, and finally forget the definition.