I have succeeded in having the file compile by slightly changing the formulation of lemmas like mul_def:

@[to_additive]
theorem mul_def [Mul β] (x y : α) :
  letI := Equiv.Mul e
  x * y = e.symm (e x * e y) := rfl
-- instead of
--theorem mul_def [Mul β] (x y : α) : @Mul.mul _ (Equiv.Mul e) x y = e.symm (e x * e y) :=
--  rfl

Doing so makes simp only [mul_def] work (I cannot completely explain why though...). Then, I was able to make the whole file compile. However, I believe that all the lemmas _def in this file should be modified accordingly before this is merged.

(I cannot completely explain why though...

The new spelling uses HMul, which is what * is notation for. That is why it now works.

bors merge

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style