refactor(tactic/wlog): simplify and speed up `wlog` (#16495)
Benefits:
- The tactic is faster
- The tactic is easier to port to Lean 4
Downside:
- The tactic doesn't do any heavy-lifting for the user
Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/wlog/near/296996966
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
