Lean4
/-- Tactic for normalizing expressions in multiplicative groups, without assuming
commutativity, using only the group axioms without any information about which group
is manipulated.
(For additive commutative groups, use the `abel` tactic instead.)
Example:
```lean
example {G : Type} [Group G] (a b c d : G) (h : c = (a*b^2)*((b*b)⁻¹*a⁻¹)*d) : a*c*d⁻¹ = a := by
group at h -- normalizes `h` which becomes `h : c = d`
rw [h] -- the goal is now `a*d*d⁻¹ = a`
group -- which then normalized and closed
```
-/
@[tactic_parser 1000]
public meta def group : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.Group.group 1022
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "group" false✝)
(ParserDescr.unary✝ `optional Lean.Parser.Tactic.location))
