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 commutative semiring `R`, and prove
the goal by checking that the LHS- and RHS-coefficients of each atom are the same up to
ring-normalization in `R`.
(If the proofs of coefficient-wise equality will require more reasoning than just
ring-normalization, use the tactic `match_scalars` instead, and then prove coefficient-wise equality
by hand.)
Example uses of the `module` tactic:
```
example [AddCommMonoid M] [CommSemiring R] [Module R M] (a b : R) (x : M) :
a • x + b • x = (b + a) • x := by
module
example [AddCommMonoid M] [Field K] [CharZero K] [Module K M] (x : M) :
(2:K)⁻¹ • x + (3:K)⁻¹ • x + (6:K)⁻¹ • x = x := by
module
example [AddCommGroup M] [CommRing R] [Module R M] (a : R) (v w : M) :
(1 + a ^ 2) • (v + w) - a • (a • v - w) = v + (1 + a + a ^ 2) • w := by
module
example [AddCommGroup M] [CommRing R] [Module R M] (a b μ ν : R) (x y : M) :
(μ - ν) • a • x = (a • μ • x + b • ν • y) - ν • (a • x + b • y) := by
module
```
-/
@[tactic_parser 1000]
public meta def tacticModule : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.Module.tacticModule 1024 (ParserDescr.nonReservedSymbol✝ "module" false✝)
