fix(tactic/group): bugfix for inverse of 1 (#3117)
The new group tactic made goals like
```lean
example {G : Type*} [group G] (x : G) (h : x = 1) : x = 1 :=
begin
group, -- x * 1 ^(-1) = 1
exact h,
end
```
worse, presumably from trying to move the rhs to the lhs we end up with `x * 1^(-1) = 1`, we add a couple more lemmas to try to fix this.
