Using change instead of unfolding

Stream: new members

[Martin Dvořák]

I repeatedly do one thing that I suspect might be an antipattern. I often need to expand a function (replace the name by its definition in the goal and/or local context) in order to make a certain lemma work. However, the command unfold does not succeed, and I use the tactic change instead. This makes my code harder to write. I assume there is no situation where the command change is really needed. Is there a general advice about something that change can be always replaced by?

[Reid Barton]

Lemmas?

[Yaël Dillies]

It feels like you're missing API.

[Filippo A. E. Nuccio]

convert is often nicer than change. It accepts also terms which differ from the goal, trying (and often suceeding) to produce "difference goals". Sometimes you end up with 37 goals, showing that you were probably asking for too much. But if it produces only 2 or 3 difference goals, you might be on a good path.

[Martin Dvořák]

Yaël Dillies said:

It feels like you're missing API.

What do you mean by that? Should I add API to my own functions in order to make unfold work?

[Yaël Dillies]

No, you should API to your own function to not need unfold.

[Martin Dvořák]

Where can I read about adding API to functions in Lean? I don't have any idea what it means.