Feature request: "module_nf"

Stream: mathlib4

[Mitchell Lee]

Let R be a commutative ring and let M be an R-module. Let us say that an expression of type M is in "normal form" if it is of the form a₁ • v₁ + ⋯ + aₙ • vₙ, where

• each aᵢ : R is a expression in ring normal form
• no aᵢ is syntactically equal to 0
• v₁, ⋯, vₙ : M are atoms; i.e. they are not of the form _ + _, _ - _, -_, or _ • _
• v₁, ⋯, vₙ are distinct and in some consistent sorted order.
  (It is possible that this definition needs to be modified slightly, but I hope it conveys the right idea.)

I think it could be quite useful to have a tactic that puts a module-valued expression in normal form. Here is an example use case:

import Mathlib

example {R : Type} [CommRing R] {V : Type} [AddCommGroup V] [Module R V] (x : R) (v w : V) :
    (1 + x ^ 2) • (v + w) - x • (x • v - w) = v + (1 + x + x ^ 2) • w := by
  sorry

Or, to give a more practical example, I recently finished defining the standard geometric representation of a Coxeter group. There was a step that involved proving a large equation in a vector space, where everything was written in terms of two vectors v and v'. The proof essentially boils down to "write each side of the equation as a • v + b • v', and then compare the coefficients". To actually carry that out, though I ended up having to do this horrible thing:

simp only [smul_sub, smul_add, smul_smul, smul_neg, sub_eq_add_neg, neg_add, ← neg_smul, smul_eq_mul]
have h₁ : ∀ a b : ℝ, a • v + b • v = (a + b) • v :=
  fun _ _ ↦ (add_smul _ _ _).symm
have h₂ : ∀ a b : ℝ, a • v' + b • v' = (a + b) • v' :=
  fun _ _ ↦ (add_smul _ _ _).symm
have h₃ : ∀ a b : ℝ, a • v' + b • v = b • v + a • v' :=
  fun _ _ ↦ add_comm _ _
have h₄ : ∀ a b c : ℝ, a • v + b • v' + c • v = (a + c) • v + b • v' :=
  fun a b c ↦ (add_right_comm _ _ _).trans (congrArg (· + _) (h₁ a c))
have h₅ : ∀ a b c : ℝ, a • v + b • v' + c • v' = a • v + (b + c) • v' :=
  fun a b c ↦ (add_assoc _ _ _).trans (congrArg (_ + ·) (h₂ b c))
simp only [← add_assoc, h₁, h₂, h₃, h₄, h₅]
ring_nf

Would this be a feasible thing to include?

[Ruben Van de Velde]

Does linear_combination work?

[Mitchell Lee]

I don't understand what you mean. Why would linear_combination be useful here?

[Ruben Van de Velde]

I don't actually know how it works, but "write each side of the equation as..." made me think of it

[Patrick Massot]

This has been on the tactic writing TODO list forever, but someone needs to do it, otherwise it will never happen.

[Eric Rodriguez]

from not reading through carefully, can this not be simplified with something like simp only [add_smul, ...]; abel?

[Mitchell Lee]

You can technically do that in the toy example I gave if you expand out the coefficients of v and w and then use ring_nf; abel. This gives an intermediate goal of v + x ^ 2 • v + (w + x ^ 2 • w) - ((x * x) • v - x • w) = v + (w + x • w + x ^ 2 • w).

example {R : Type} [CommRing R] {V : Type} [AddCommGroup V] [Module R V] (x : R) (v w : V) :
    (1 + x ^ 2) • (v + w) - x • (x • v - w) = v + (1 + x + x ^ 2) • w := by
  simp only [smul_add, smul_sub, smul_neg, smul_smul]
  simp only [add_smul, sub_smul, neg_smul, one_smul]
  ring_nf
  abel

However, I want to do it without expanding out the coefficients. So, for example, I want the normal form of (1 + x ^ 2) • (v + w) - x • (x • v - w) to be 1 • v + (1 + x + x ^ 2) • w, not 1 • v + 1 • w + x • w + (x ^ 2) • w. (I should have made that clear in my original post; the v₁, ⋯, vₙ are supposed to be distinct.) It might not always be possible to break down the coefficients into sums and cancel out individual terms.

[Mitchell Lee]

For that particular example, though, I agree that

simp only [smul_add, smul_sub, smul_neg, smul_smul]
simp only [add_smul, sub_smul, neg_smul, one_smul]
ring_nf
abel

is pretty clean.

Still, the one line

module_nf

would be even better.

[Yaël Dillies]

Mitchell Lee said:

I want the normal form of (1 + x ^ 2) • (v + w) - x • (x • v - w) to be 1 • v + (1 + x + x ^ 2) • w, not 1 • v + 1 • w + x • w + (x ^ 2) • w.

Can you un #xy ? What do you need this normal form for?

[Mitchell Lee]

It's very easy to compare two expressions when they're both of the form (something) • v + (something) • w. In informal mathematics, if I wanted to show (1 + x ^ 2) • (v + w) - x • (x • v - w) = v + (1 + x + x ^ 2) • w, I would say "Look at the coefficient of $v$ and of $w$ on both sides; they are equal". I would not say "Write each side using monomials of the form $x^n v$ or $x ^ n w$, and then perform the necessary cancellations." The latter is far less flexible.

[Mitchell Lee]

For a slightly more serious example, consider this. At some point when developing the theory of Coxeter groups (after line 506 here), I needed to show that

$$\frac{\sin ((2 k + 1) \pi / m)}{\sin (\pi / m)} (\alpha_i + 2 \cos(\pi / m) \alpha_{i'}) + \frac{\sin (2 k \pi/ m)}{\sin (\pi / m)} (-\alpha_{i'})$$

is equal to

$$\frac{\sin ((2 k + 1) \pi / m)}{\sin (\pi / m)} \alpha_i + \frac{\sin ((2 k + 2) \pi / m)}{\sin (\pi / m)} \alpha_{i'},$$

where $m$ is a natural number and $\alpha_i, \alpha_{i'}$ are elements of some real vector space. It would not make any sense to try to prove this by breaking $\frac{\sin ((2 k + 2) \pi / m)}{\sin (\pi / m)}$ into its "monomials". The sensible way to approach the problem is to compare the coefficients of $\alpha_i$ and of $\alpha_{i'}$ on both sides, and it would have been useful if there were a tactic that could automatically write each side as some coefficient times $\alpha_i$ plus some coefficient times $\alpha_{i'}$.

[Yaël Dillies]

Okay, but you gave me an example in terms of a polynomial and now you give me your motivation in terms of a power series!

[Mitchell Lee]

Where's the power series? The part I am trying to automate in the above example is not the part where you prove the real number equation
$\frac{\sin((2k + 1) \pi / m)}{\sin(\pi / m)} \cdot (2 \cos (\pi/m)) - \frac{\sin(2k \pi / m)}{\sin(\pi / m)} = \frac{\sin((2k + 2) \pi / m)}{\sin(\pi / m)}.$ I understand that that can't be done using ring_nf and needs to be done using some other method. That's fine. There are many other theorems and tactics in Lean for dealing with equations in rings.

The part I am trying to automate is the part where you collect all the terms containing $\alpha_i$, and you collect all the terms containing $\alpha_{i'}$, and you equate those coefficients on both sides. Whether those coefficients are polynomials in whatever variables happen to appear in the example is immaterial.

[Yaël Dillies]

Yes, so I am claiming this is a rather specialised normal form, because eg you might also also want to group things by scalars

[Mitchell Lee]

Well, then you could use a different method for that.
Also, I'm not entirely sure you would actually ever want to do that.

[Mitchell Lee]

I think essentially what you are saying is "Imagine a problem that could not be solved using the method you describe", and I do not think that is a good reason to claim that the method is not useful.

[Mitchell Lee]

Maybe I am misunderstanding what you are saying, though.

[Yaël Dillies]

What I'm saying is that you should think of your method in a broader context. So maybe you want a tactic which can switch between various normal forms

[Yaël Dillies]

eg "fully expanded", "scalar-collected", "vector-collected"

[Mitchell Lee]

Shouldn't that just be three different tactics, though?

[Yaël Dillies]

Not necessarily!

[Mitchell Lee]

Also, I think that collecting like terms based on the vector is by far the most useful out of those three. What's a reason why I would actually want 1 • v + 1 • w + x • w + (x ^ 2) • w over 1 • v + (1 + x + x ^ 2) • w?

[Yaël Dillies]

For the same reason that you would want a * a + a * b + b * a + b * b rather than (a + b) * a + (a + b) * b?

[Mitchell Lee]

Let's say we have an equation in the commutative ring $\mathbb{Z}[a, b]$, such as $(a + b) ^ 4 + (a - b) ^ 4 = 2 a ^ 4 + 12 a^2 b^2 + 2 b ^ 4$. Sometimes, you need to expand some products in order to prove an equation like this.

If you have any expression built up from the operations of a ring and the variables $a$ and $b$, you can always put it in a normal form by expanding out all the products. This procedure lets you decide whether any two elements of $\mathbb{Z}[a, b]$ are equal. In fact, you can even do the same for $R[a, b]$ for any ring $R$, as long as you know how to work with elements of the ring $R$ already.

That's why we sometimes want a * a + a * b + b * a + b * b rather than (a + b) * a + (a + b) * b. The bad news, however, is that expanding products can make them balloon exponentially in complexity, so we don't always want to do it.

Now, let's say that instead of working in the free (commutative) ring $\mathbb{Z}[a, b]$, we were to work in the free $\mathbb{Z}$-module generated by two vectors $v$ and $w$. This time, it is never necessary to expand anything out. The normal form is $mv + nw$, where $m$ and $n$ are integers. If you have two expressions of this form, it is very easy to add them. It is also very easy to multiply an expression of this form by a scalar. It is also very easy to decide whether two expressions of this form are equal. Those are all the operations of a module, so this is a "complete" normal form for elements of this module.

Of course, in this example, the ring $\mathbb{Z}$ can be replaced by any ring $R$. But we'll have to compare the coefficients of $v$ and of $w$, so it is best if we already have some ways of dealing with elements of $R$ and proving that they are equal.

Note that unlike in the previous example, we do not have to make a compromise. Putting an expression like $(a + b)^6$ into normal form has the potential to make it more complex. But putting an expression like $3(2v - w) - (3w + v) + 5(3(w - 2v) + v)$ into normal form does not.

[Mitchell Lee]

That's why I want everything to be written as (something) • v + (something) • w: it's because that form lets you do anything you want. By "anything", I mean any operation in the language of modules.

Yes, this only works for free modules. But then, ring_nf only works for free rings, and abel_nf only works for free abelian groups. Dealing with relations is harder.

[Yaël Dillies]

Okay, that is a fair argument. Although note that I still don't understand your use case

[Damiano Testa]

I remember that there was some discussion of something like this in lean 3 and I may have even written a metaprogram that "collected terms" at the time. Let me see if I can dig up the Zulip thread.

[Yaël Dillies]

My point is that usually you don't want to put things in normal form but instead let the tactic run terminally by first stating the exact equality you want

[Yaël Dillies]

Have you tried using linear_combination?

[Mitchell Lee]

I do not see how linear_combination does anything here. For one, it only proves equations in commutative semirings.

[Yaël Dillies]

Then it should be extended to work for modules

[Damiano Testa]

I can't find it, but I also tend to agree with Yaël: there are already tools to deal with similar problems and the idea of "collecting terms" is often hard to formalize precisely and tricky to implement.

[Damiano Testa]

If you have a specific example, maybe I can look into how to get the available tools to work towards it.

[Mitchell Lee]

linear_combination always needs a normalization tactic in order to do anything useful. (By default it uses ring_nf.) So if you're saying that linear_combination should work for modules, then you are implicitly agreeing that there should be a module_nf.

[Mitchell Lee]

I already stated an exact specification of what "normal form" could mean, at the beginning of this thread.

[Eric Rodriguez]

I agree with Mitchell here, and I also think that part of the reason we're so resistant to this change here is that our normal form tactics have been mediocre; ring_nf doesn't usually give what I'd call a normal form, it's usually messy.

[Mario Carneiro]

To be clear, there is no fundamental reason we don't have a module tactic, abel is already doing that somewhat (it's a Z-module tactic, and runs ring on the Z part)

[Mario Carneiro]

Eric Rodriguez said:

I agree with Mitchell here, and I also think that part of the reason we're so resistant to this change here is that our normal form tactics have been mediocre; ring_nf doesn't usually give what I'd call a normal form, it's usually messy.

Curious to hear more details about this. ring_nf shows what ring would call its normal form, and it is actually a normal form in the sense that equal expressions map to the same thing

[Mario Carneiro]

I would expect module tactic to either group by vectors or fully expand sums for its normal form

[Mitchell Lee]

To expand on the thing I said earlier about linear_combination needing a normalization tactic, consider this equation again:

(1 + x ^ 2) • (v + w) - x • (x • v - w) = v + (1 + x + x ^ 2) • w

You can't prove an equation like this one by just saying "take the equation 1 + x ^ 2 - x * x = 1 and multiply it by v, and take the equation 1 + x ^ 2 - x * (-1) = 1 + x + x ^ 2 and multiply it by w, then add them together."

The thing that is missing from this proof is some way to do the algebraic manipulations to know that (1 + x ^ 2) • (v + w) - x • (x • v - w) is the same thing as (1 + x ^ 2 - x * x) • v + (1 + x ^ 2 - x * (-1)) • w in the first place. (Note, by the way, that the fact that these two expressions are equal can be proved using only the module axioms, without using the ring axioms.) There is currently no way in Lean to do this painlessly.

[Eric Rodriguez]

Mario Carneiro said:

Eric Rodriguez said:

I agree with Mitchell here, and I also think that part of the reason we're so resistant to this change here is that our normal form tactics have been mediocre; ring_nf doesn't usually give what I'd call a normal form, it's usually messy.

Curious to hear more details about this. ring_nf shows what ring would call its normal form, and it is actually a normal form in the sense that equal expressions map to the same thing

I'm sure programmatically it makes sense, and it is reliable, but it usually looks messy to a human that wants to further edit it. I know this is not it's purpose, though

[Mario Carneiro]

no, it really is its purpose, which is why I would like more concrete examples of what it does and why it is bad

[Mario Carneiro]

it does actually try to clean up the results to be presentable to humans

[Mario Carneiro]

that's actually most of the code

[Jireh Loreaux]

I would also be interested, because I find the output of ring_nfto be pretty much usable on the rare case I actually want ring_nf.

[Joseph Myers]

Once you have something to normalize / prove equality of expressions in a module, a natural thing following on from there is to prove equality in an AddTorsor. (Pick a base point and express every other point as the sum of a vector and that base point, to turn an equality involving an AddTorsor to one where points in that torsor appear only in subtractions with the base point on the RHS of the subtraction - i.e., an equality of expressions with vectors, which is the sort of thing a module tactic would deal with. Actually doing this by hand with a long sequence of rewrites becomes rather tedious unless the expressions are very short, I found a few times when doing things in Euclidean geometry that were essentially trivial to humans by this kind of manipulation.)

[Mario Carneiro]

do you have an example theorem statement?

[Joseph Myers]

I don't have an example to hand of where I encountered such a need for a long sequence of rewrites in reality, but a toy example of what such a tactic for additive (commutative) torsors should be able to handle is:

import Mathlib

example [AddCommGroup V] [Module ℝ V] [AddTorsor V P] (a b c d e f g : P) :
    (a -ᵥ b) + (c -ᵥ d) + (e -ᵥ f) +ᵥ g = (g -ᵥ d) + (e -ᵥ b) + (c -ᵥ f) +ᵥ a := by
  sorry

[Mario Carneiro]

so you aren't thinking about convex affine combinations or anything like that, just + and - ?

[Mario Carneiro]

(plus module stuff in the vector part)

[Eric Rodriguez]

Mario Carneiro said:

it does actually try to clean up the results to be presentable to humans

I'll keep an eye out for examples when I come across them!

[Heather Macbeth]

I am thinking of writing this module-normalization tactic, and at branch#HM-module I have started collecting some tests for such a tactic. They include

• some examples discussed by @Rob Lewis and me a couple of years ago
• some examples from a proof about eigenvectors I wrote with @Johan Commelin and @Jeremy Avigad
• the above example from @Mitchell Lee
• the example in this thread from @Patrick Massot

That branch also includes a "cheap" version of the module tactic (distribute everything, ring-normalize scalars, then run abel), mostly to show that this cheap version is not good enough in several of the examples already collected.

Many people have thought about this over the years -- does anyone else have examples they have noted as test cases for such a tactic?

[Yaël Dillies]

I just generated a bunch of them in #14999. Eg L102-105, L151, L168-170. Note that it's not just normalisation I want but also cancelling simple denominators like δ, 1 - δ, ε + ‖x - y‖.

[Heather Macbeth]

@Yaël Dillies The commit you pointed to for these examples does not seem to exist any more:
https://github.com/leanprover-community/mathlib4/tree/45a8a3d311b995530e9b0e5a633dfe25a540fc10
Can you give me the line references on the current branch?

[Heather Macbeth]

(or just make MWEs)

[Yaël Dillies]

I was hoping that pointing to a specific commit would be enough to reproduce, because indeed I rebased just after that :see_no_evil:

[Yaël Dillies]

I will make MWEs

[Heather Macbeth]

I couldn't figure out how to check it out or get a cache for it.

[Yaël Dillies]

I am not a git wizard but git checkout 45a8a3d should Just Work :tm:

[Heather Macbeth]

Hmm, that gives me error: pathspec '45a8a3d' did not match any file(s) known to git. Could you indeed please make a MWE, or just a branch?

[Yaël Dillies]

Sorry, I was dragged into watching a movie and now I am falling asleep. Tomorrow you will have my MWEs

[Eric Wieser]

You need to git fetch origin the_sha first

[Heather Macbeth]

I have a prototype for the module-normalization tactic up at branch#HM-module -- the tactic "works" but all proofs built are currently sorries.

The main algorithm is for partially-normalizing an expression in M into the form c1 • x1 + c2 • x2 + ... c_k • x_k, where x1, x2, ... are distinct atoms in M, and c1, c2, ... are scalars. The scalar type of the expression 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. (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).

There is then a tactic match_scalars which reduces an equality goal in M to a collection of equality goals in the scalar type: one goal for each M-atom which occurs.

Finally, the tactic module consists of running match_scalars and then trying to resolve each of the scalar equalities by ring.

(I keep match_scalars as a separate tactic because sometimes one wants to resolve the scalar equalities by some other argument, e.g. field_simp; ring.)

[Heather Macbeth]

Before I actually write the proof-producing part of the tactic, I'd be glad to get sanity checks on this algorithm: from any potential users (does it sound like your intended goals are in scope?) and/or from the people who have written the big algebraic automation in mathlib (@Mario Carneiro, ...).

[Yaël Dillies]

What happens if you have an atom a • b where a doesn't belong to a semiring R with Algebra S R or Algebra R S for S running over the other semirings in the expression?

[Yaël Dillies]

Also algebraMap need not be injective (and docs#algebraMap_injective is terribly named). Are you further assuming it is the case?

[Heather Macbeth]

Yaël Dillies said:

What happens if you have an atom a • b where a doesn't belong to a semiring R with Algebra S R or Algebra R S for S running over the other semirings in the expression?

Since parsing happens inward-out, that scalar-multiplication will get parsed (assuming a belongs to a type which is indeed a semiring), and the conflicts will occur later.

[Heather Macbeth]

Yaël Dillies said:

Also algebraMap need not be injective (and docs#algebraMap_injective is terribly named). Are you further assuming it is the case?

This is the kind of thing I won't know until I write the proof-producing part :)

[Yaël Dillies]

That sounds a bit annoying if I have a goal of the form big_expression1 + a • b + big_expression2 = big_expression3 + a • b + big_expression4

[Heather Macbeth]

@Yaël Dillies I managed to unpack one of your examples by eye, and added it as a test:
https://github.com/leanprover-community/mathlib4/commit/d58090b038a2e0d15e93691b5853c2cc0a222d8c
Did you have a chance to write MWEs for the others?

[Yaël Dillies]

Sorry no I was climbing. Holidays are busy... I am now bored on a train so you will get the MWE :soon:

[Heather Macbeth]

Yaël Dillies said:

That sounds a bit annoying if I have a goal of the form big_expression1 + a • b + big_expression2 = big_expression3 + a • b + big_expression4

What would be the context here? That is, what (semi)rings?

[Yaël Dillies]

I don't have an example in mind, but I'm sure someone will encounter it eventually. When they do, it would be confusing behavior that adding an unrelated term to the expression makes the whole thing fail. Here is an idea for how to robustify the tactic: Make the user provide a semiring R, and only normalize the scalars that are in a semiring S for which Algebra S R. If the user doesn't provide R, fall back on the behavior your first described.

[Heather Macbeth]

I was actually thinking of the opposite (an option to provide S, the semiring in which all the scalars should be considered, and immediately force all scalars into this ring). But for a later PR, not the first version.

[Heather Macbeth]

The use case I had in mind there was something like ℤ and ℝ≥0 -- if both those occur, you want to immediately force all scalars into ℝ.

[Yaël Dillies]

Sorry, I of course put the arguments to Algebra in the wrong order

[Yaël Dillies]

@Heather Macbeth:

import Mathlib.Algebra.Module.Defs
import Mathlib.Algebra.Order.Field.Defs

variable {K V : Type*} [LinearOrderedField K] [AddCommGroup V] [Module K V]

-- From Analysis.Convex.Continuous
example {x y : V} {ε : K} (hε₀ : 0 < ε) (hε₁ : ε < 1) :
    ε⁻¹ • (x - (1 - ε)⁻¹ • x - (ε / (1 - ε)) • y) + ((1 - ε)⁻¹ • x - (ε / (1 - ε)) • y) = y := sorry

-- From Analysis.Convex.Continuous
example {x y z : V} {ε : K} (hε₀ : 0 < ε) (hε₁ : ε < 1) :
    ε • (ε⁻¹ • (z - (1 - ε)⁻¹ • x - (ε / (1 - ε)) • y) + (1 - ε)⁻¹ • x - (ε / (1 - ε)) • y) + (1 - ε) • ((1 - ε)⁻¹ • x - (ε / (1 - ε)) • y) = z := sorry

-- From Analysis.Convex.StoneSeparation
example {p q x y : V} {az bz au bu av bv : K} (hu : au + bu = 1) (hv : av + bv = 1)
    (hz : az + bz = 1) (hab : 0 < az * av + bz * au) :
    (az * av / (az * av + bz * au) * bu) • p + (bz * au / (az * av + bz * au) * bv) • q +
      ((az * av / (az * av + bz * au)) • au • x + (bz * au / (az * av + bz * au)) • av • y) =
      (az * av + bz * au)⁻¹ • ((az * av * bu) • p + ((bz * au * bv) • q +
        ((az * av) • au • x + (bz * au) • av • y))) := sorry

[Yaël Dillies]

I don't know whether you want me to get rid of the _ + _ = 1 equalities

[Yaël Dillies]

Also please tell me if I incorrectly spotted which of the three examples from #14999 you had already translated

[Heather Macbeth]

@Yaël Dillies Have you been able to prove these? Trying e.g. the first one by hand (following the algorithm of the tactic), I am having trouble with the y-coefficient:

example {x y : V} {ε : K} (hε₀ : 0 < ε) (hε₁ : ε < 1) :
    ε⁻¹ • (x - (1 - ε)⁻¹ • x - (ε / (1 - ε)) • y) + ((1 - ε)⁻¹ • x - (ε / (1 - ε)) • y) = y := by
  rw [← sub_pos] at hε₁
  trans ((ε⁻¹ * (1 - (1 - ε)⁻¹)) + (1 - ε)⁻¹) • x - ((ε / (1 - ε)) + (ε⁻¹ * (ε / (1 - ε)))) • y
  · simp only [smul_add, smul_neg, smul_sub, neg_smul, add_smul, sub_smul, mul_smul, smul_eq_mul, one_smul]
    abel
  trans (0:K) • x - (-1:K) • y
  · congrm ?_ • x - ?_ • y
    · field_simp
    · field_simp
      ring_nf
      sorry -- 1 + ε = -1 + ε
  · simp

[Yaël Dillies]

Oh no sorry. Probably a copy-paste error on my part. Can you put the broken proof on a brach for me to fix?

[Heather Macbeth]

FWIW, my tactic objects to both (1) and (2), but I haven't tried (2) by hand :)

[Heather Macbeth]

Just added (3) to the tests, let me know if you get the other two working.

[Yaël Dillies]

To be clear, I have proved the unminimized version of (1) and (2) :grinning:

[Heather Macbeth]

I have now PR'd the new match_scalars and module tactics: #16593. The module tactic consists of running match_scalars and then running ring on each scalar goal created.

Examples:

example [AddCommGroup V] [LinearOrderedField K] [Module K V]
    {a b : K} {x y : M} (ha : 0 ≤ a) (hb : 0 < b) :
    x = (a / (a + b)) • y + (b / (a + b)) • (x + (a / b) • (x - y)) := by
  match_scalars
  ·  -- ⊢ 1 = b / (a + b) * (1 + a / b * 1)
    field_simp
    ring
  · -- ⊢ 0 = a / (a + b) * 1 + b / (a + b) * (a / b * -1)
    field_simp
    ring

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

[Yaël Dillies]

My first-ever battle-testing of match_scalars (see https://github.com/YaelDillies/LeanCamCombi/blob/0e9327aa52c08a8199a81a0a0267923e2febefa2/LeanCamCombi/Sight/Sight.lean#L71). It proves

⊢ ((1 - (1 - w i) / w i / ((1 - ε) / ε + (1 - w i) / w i + 1)) * (1 - ε)) • x +
      ((1 - (1 - w i) / w i / ((1 - ε) / ε + (1 - w i) / w i + 1)) * ε) • a i +
    ((1 - w i) / w i / ((1 - ε) / ε + (1 - w i) / w i + 1)) • ∑ j ∈ t.erase i, (w j / (1 - w i)) • a j =
  (1 - (w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹)) • x +
    (((w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹) * w i) • a i +
      ((w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹) * (1 - w i)) • ∑ j ∈ t.erase i, (w j / (1 - w i)) • a j)

Worked great!

[Mitchell Lee]

#13270 is another successful use case of match_scalars and module. In fact, the problem solved in #13270 is the reason I started this thread.

[Mitchell Lee]

Thanks so much @Heather Macbeth!