Lean4
/-- Given a goal which is an equality in a type `M` (with `M` an `AddCommMonoid`), parse the LHS and
RHS of the goal as linear combinations of `M`-atoms over some semiring `R`, and reduce the goal to
the respective equalities of the `R`-coefficients of each atom.
For example, this produces the goal `⊢ a * 1 + b * 1 = (b + a) * 1`:
```
example [AddCommMonoid M] [Semiring R] [Module R M] (a b : R) (x : M) :
a • x + b • x = (b + a) • x := by
match_scalars
```
This produces the two goals `⊢ a * (a * 1) + b * (b * 1) = 1` (from the `x` atom) and
`⊢ a * -(b * 1) + b * (a * 1) = 0` (from the `y` atom):
```
example [AddCommGroup M] [Ring R] [Module R M] (a b : R) (x : M) :
a • (a • x - b • y) + (b • a • y + b • b • x) = x := by
match_scalars
```
This produces the goal `⊢ -2 * (a * 1) = a * (-2 * 1)`:
```
example [AddCommGroup M] [Ring R] [Module R M] (a : R) (x : M) :
-(2:R) • a • x = a • (-2:ℤ) • x := by
match_scalars
```
The scalar type for the goals produced by the `match_scalars` tactic is the largest scalar type
encountered; for example, if `ℕ`, `ℚ` and a characteristic-zero field `K` all occur as scalars, then
the goals produced are equalities in `K`. A variant of `push_cast` is used internally in
`match_scalars` to interpret scalars from the other types in this largest type.
If the set of scalar types encountered is not totally ordered (in the sense that for all rings `R`,
`S` encountered, it holds that either `Algebra R S` or `Algebra S R`), then the `match_scalars`
tactic fails.
-/
@[tactic_parser 1000]
public meta def tacticMatch_scalars : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.Module.tacticMatch_scalars 1024
(ParserDescr.nonReservedSymbol✝ "match_scalars" false✝)
