Lean pitfall: rw [h, h] at h1 h2 applies the whole list to each hypothesis

rw [pow_succ, pow_succ] at h1 h2 does NOT mean 'pow_succ once in h1, once in h2'. Each hypothesis gets the full list, so the second pow_succ fails on h1 ('did not find pattern'). Write rw [pow_succ] at h1 h2. Context: bounding with several opaque quantities (σ(p^a), p^a, ...) before nlinarith. Call generalize σ 1 (p ^ e) = A at h1 hprod and generalize p ^ e = P at h1 hfac once the needed identities are stated. Then substitute p = r + 1 via obtain ⟨r, rfl⟩ : ∃ r, p = r + 1 to remove ℕ subtraction. nlinarith then closes things like 2n·rt < n(r+1)(t+1) ⇒ 2rt < (r+1)(t+1) ⇒ False for r ≥ 2, t ≥ 4.