mulabel

Stream: Is there code for X?

[Kevin Buzzard]

import tactic

example (G : Type) [add_comm_group G] (a b : G) :
a + b + -a + -b = 0 :=
begin
  abel,
end

example (G : Type) [comm_group G] (a b : G) :
a * b * a⁻¹ * b⁻¹ = 1 :=
begin
  -- now what?
  sorry
end

[Johan Commelin]

Pretty clear right? You just push things to the group ring, and use ring :grinning_face_with_smiling_eyes:

[Johan Commelin]

More seriously, I guess you can apply additive.of_mul_injective or something like that, and then simp; abel. Even more seriously... this should be fixed in abel.