GroupTheory.Divisible !4#2149

Stream: mathlib4

[Ruben Van de Velde]

I got some annoying issues with to_additive; fixed most of them by adding explicit names, but haven't figured out the last error. If someone could take a look, that would be great

[Floris van Doorn]

For the naming: you should add rootable to
https://github.com/leanprover-community/mathlib4/blob/59ce0e8641506f646405607f92d84b300a2d0d67/Mathlib/Tactic/ToAdditive.lean#L676

[Floris van Doorn]

i.e. | "rootable" => ["divisible"]

[Floris van Doorn]

For the other error, please make sure A is the first variable in all lemma statements, i.e. reorder variables {α A B : Type*}. That should fix the error.

[Floris van Doorn]

The fact that it worked in Lean 3 is probably a regression in the behavior of docs4#ToAdditive.firstMultiplicativeArg. I will investigate, but you make life easier for to_additive if you change the argument order (and that shouldn't break anything down the line, but you could add a porting note).

[Ruben Van de Velde]

Thanks, will try