Where to rewrite

Stream: new members

[Benjamin]

I'm sure this is basic, but I can't figure this out from the documentation. How do I decide where to rewrite at a hypothesis? For example, if I want to rewrite the third instance of n to be n+0 in hypothesis h, what would I type?

[Benjamin]

What I've tried is rw \l add_zero(n) at h, but this replaces all instances.

[Johan Commelin]

rw [lemma1, lemma2] at hyp { occs := occurences.pos [3, 5] }

[Johan Commelin]

@Benjamin :up:

[Benjamin]

Thanks! Also, while I'm here, I know rw isn't supposed to be used for one way implications. Is there a function to use for that instead besides have, which requires creating another hypothesis?