Lean4
/-- `ac_change g using n` is `convert_to g using n` followed by `ac_rfl`. It is useful for
rearranging/reassociating e.g. sums:
```lean
example (a b c d e f g N : ℕ) : (a + b) + (c + d) + (e + f) + g ≤ N := by
ac_change a + d + e + f + c + g + b ≤ _
-- ⊢ a + d + e + f + c + g + b ≤ N
```
-/
@[tactic_parser 1000]
public meta def acChange : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.acChange 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "ac_change " false✝) (ParserDescr.cat✝ `term 0))
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " using ") (ParserDescr.const✝ `num))))
