Submodule.span_induction vs prime

Stream: mathlib4

[Antoine Chambert-Loir]

docs#Submodule.span_induction and docs#Submodule.span_induction' are similar, the latter retaining the hypothesis x in Submodule.span S for the inductive proof.
One annoying difference between these two statements is the order of arguments.
For one, the hypothesisx in Submodule.span S is the first one, for the other, it is the last one…
Would it be reasonable to refactor docs#Submodule.span_induction' so as to put it first?

[Antoine Chambert-Loir]

A further change would be to switch the order of the arguments for the third hypothesis (the add field) of docs#Submodule.span_induction' , from
(add : ∀ (x : M) (hx : x ∈ Submodule.span R s) (y : M) (hy : y ∈ Submodule.span R s), p x hx → p y hy → p (x + y) ⋯)
to
(add : ∀ (x : M) (hx : x ∈ Submodule.span R s) (hx' : p x hx) (y : M) (hy : y ∈ Submodule.span R s) (hy' : p y hy), p (x + y) ⋯)
so as to avoid switching the order of which variable is involved.

[Antoine Chambert-Loir]

(Possibly making {x : M} and {y : M}`as well, but it's not clear to me.)

[Riccardo Brasca]

What is the situation with the submonoids and subgroups? (span is closure in those cases).

[Antoine Chambert-Loir]

Good point. Exactly the same (these are docs#Submonoid.closure_induction and docs#Submonoid.closure_induction', respectively docs#Subgroup.closure_induction and docs#Subgroup.closure_induction').

[Eric Wieser]

For induction to work, the argument has to be last

[Eric Wieser]

But also, you shouldn't care about the argument order if you write induction x, hx using span_induction'

[Eric Wieser]

(the add change is probably harmless)

[Antoine Chambert-Loir]

I didn't know that syntax (x, hx), I'll check if this simplifies our dirty apply… where I had to specify the property to be induced.

[Jireh Loreaux]

Also, at some point we should just remove Submodule.span_induction and friends entirely in favor of their primed counterparts.

[Jireh Loreaux]

(Because the unprimed ones don't work with induction.)

[Antoine Chambert-Loir]

In fact, the notation seems to be induction hx using Submodule.induction_on' (and without the usual with … precisions, it's a mess).

[Eric Wieser]

What do you mean by "the usual with precisions", and can you give an example of the mess?

[Antoine Chambert-Loir]

the series of | … => … whose names are difficult to remember, and without which lean inserts variables with unreachable names.

[Eric Wieser]

I think the bug report hiding here is that the light bulb doesn't appear for induction ... using

[Eric Wieser]

You don't need to remember the names, you can hover over Submodule.span_induction to see them

[Kevin Buzzard]

Yeah but (a) this is silly and (b) induction' doesn't have this problem. A blue light bulb would be wonderful