import the necessary context for challenge 8

[Ezra]

On challenge 8, Lean complains that it doesn't know the word "group", so (poking through mathlib docs) we'd better import algebra.group.basic. This also puts mul_inv_rev into our list of completions, as the hints file assumes.

If we then also imported tactic, we'd recover the tactic of group, which might otherwise be nice - but here it would trivialize this challenge, so we don't.