Look behind definitions (such that explicit unfolds are not needed) when performing rewrites

[dranov]

This is the behaviour Coq rewrite seems to have.

Currently in Lean, we either:

1. Add a @[simp] attribute to the definition, which means it's always unfolded when simplification is called – which is annoying when a goal has multiple functions, only some of which we want to unfold, or
2. Manually unfold before calling the rewrite, which is verbose

[volodeyka]

Could you check if erw tactic from Lean standard library solves this issue?
If it works, I will make srw call erw internally instead of rw

[volodeyka]

Alright, I just tired, it doesn't work. Will it help if I add unfolding to intro patterns?

[dranov]

@volodeyka yes, it will definitely help to have unfolding via views e.g. /nseq