feat: match_scalars and module tactics (#16593)

This PR contributes two new tactics `match_scalars` and `module`.

Given a goal which is an equality in a type `M` (with `M` an `AddCommMonoid`), the `match_scalars` tactic parses the LHS and RHS of the goal as linear combinations of `M`-atoms over some semiring `R`, and reduces 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`:
```lean
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):
```lean
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
```

The `module` tactic runs the `match_scalars` tactic and then runs the `ring` tactic on each of the coefficient-wise equalities which are created, failing if this does not resolve them.  For example, it solves the following goals:
```lean
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
```
The scalar type `R` in these tactics is not pre-determined: instead it starts as `ℕ` (when each atom is initially given a scalar `(1:ℕ)`) and gets bumped up into bigger semirings when such semirings are encountered.  However, to permit this, it is assumed that there is a "linear order" on all the semirings which appear in the expression: for any two semirings `R` and `S` which occur, we have either `Algebra R S` or `Algebra S R`).



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Patrick Massot <patrickmassot@free.fr>

Author: 3 people

Mathlib.lean

@@ -4288,6 +4288,7 @@ import Mathlib.Tactic.Measurability.Init
 import Mathlib.Tactic.MinImports
 import Mathlib.Tactic.MkIffOfInductiveProp
 import Mathlib.Tactic.ModCases
+import Mathlib.Tactic.Module
 import Mathlib.Tactic.Monotonicity
 import Mathlib.Tactic.Monotonicity.Attr
 import Mathlib.Tactic.Monotonicity.Basic

Mathlib/Tactic.lean

@@ -150,6 +150,7 @@ import Mathlib.Tactic.Measurability.Init
 import Mathlib.Tactic.MinImports
 import Mathlib.Tactic.MkIffOfInductiveProp
 import Mathlib.Tactic.ModCases
+import Mathlib.Tactic.Module
 import Mathlib.Tactic.Monotonicity
 import Mathlib.Tactic.Monotonicity.Attr
 import Mathlib.Tactic.Monotonicity.Basic