chore(Data/Seq/Parallel): remove an erw (#38681)

- unfolds `rmap` before rewriting by the split equation, avoiding the `erw` in `terminates_parallel.aux`

Extracted from #38415

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

Author: yuanyi-350

Mathlib/Data/Seq/Parallel.lean

@@ -102,7 +102,7 @@ theorem terminates_parallel.aux :
             match o with
             | Sum.inl a => Sum.inl a
             | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
-          (Sum.inr List.nil) l with a' | ls <;> erw [e] at e'
+          (Sum.inr List.nil) l with a' | ls <;> simp only [rmap] at e <;> rw [e] at e'
         · contradiction
         have := IH' m _ e
         grind