Control the scope of strategy application

Stream: lean4

[lexuan]

In Lean4, it is common to encounter situations where you only want to apply a tactic to a specific part of the goal. For example, with the expression nsmul₁ (h + n2 + 1) m = nsmul₁ (h + 1) m + nsmul₁ n2 m, I might only want to apply the unfold nsmul₁ tactic to nsmul₁ (h + n2 + 1) m and nsmul₁ (h + 1) m. How should one write the code for this situation?

[Kyle Miller]

One solution is conv. Mathlib documentation has an introduction and a guide.

[lexuan]

Okay, I'll study it now.