An easy way to convert multiplicative group to additive?

Stream: new members

[Jakub Nowak]

Is there some tactic than can convert multiplicative group to additive one, without having to re-type whole expression in additive form manually?

import Mathlib

example [CommGroup α] (a b c : α) : a * b * c / a = c * b := by
  suffices ∀ (a b c : Additive α), a + b + c - a = c + b from this a b c
  intro a b c
  abel1

[Kevin Buzzard]

Do we still not have mabel? :-( If we had mabel then would you still need this conversion tactic?

[Kevin Buzzard]

(I suppose a reasonable way of writing mabel would be to write the conversion tactic first)

[Michael Rothgang]

I believe we don't have mabel yet: there were two PRs proposing that, but IIRC in both cases the authors stopped working on them at some point.

[Jakub Nowak]

Yeah, my only point was to use abel on it. It's kinda unfortunate that we must have duplicate API too, but it's mostly solved by [to_additive] ig.