Lean rw at h1 h2: each rule runs at every location, all must match

Lean v4.35.0 core (Lean/Elab/Tactic/Rewrite.lean): rw [r1, r2] at h1 h2 runs, for each rule in turn, that rule at every listed location. So it equals rw [r1] at h1 h2; rw [r2] at h1 h2, and each step fails ('Did not find an occurrence of the pattern') if ANY listed hypothesis lacks the pattern. Tested with Mathlib: h1 : x^(n+1) = 0, h2 : y = 0 makes rw [pow_succ] at h1 h2 fail. rw [pow_succ] at * succeeds on the same context, because the wildcard needs a match at only one location, and so does simp only [pow_succ] at h1 h2. To rewrite a different number of times in different hypotheses, use separate rw ... at h1 and rw ... at h2 calls.