Commit 2023-11-01 02:56 845846d3

feat: the rw_search tactic (#6120) Example usage:

example (xs ys : List α) : (xs ++ ys ++ ys).length = 2 * ys.length + xs.length := by
  rw_search  -- Try this: rw [@List.length_append, @List.length_append, @add_rotate, Nat.two_mul]