[Merged by Bors] - fix(algebra/group/units): splitting out mul_one_class for group of units

[joneugster]

Without this proposed change, the following example gives a (deterministic) timeout:

import algebra.ring.basic

example (R : Type*) [comm_ring R] (a b : Rˣ) : a * (b / a) = b :=
begin
  rw mul_div_cancel'_right,
  -- or: `simp`
end

---

Note: After a lot of iterations this is now at a short solution that does not change any instance priorities, thus should hopefully not cause future problems. However, I don't understand 100% why splitting out the mul_one_class from the group αˣ instance improves things.

Zulip

[urkud]

(there was some nonsense here)

[Vierkantor]

However, I don't understand 100% why splitting out the mul_one_class from the group αˣ instance improves things.

It doesn't surprise me that adding an intermediate instance helps things along, since Lean is very slow at checking equality of instances (like units.group) of types (like units) that appear in instances (like units.mul_one_class).

Could you add the timeout example as a test case, for example in a new file test/units.lean?

[Vierkantor]

We typically copy over data like this, for better unfolding. Or does that reintroduce the timeout?

Suggested change

	{ mul_assoc := λ u₁ u₂ u₃, ext $ mul_assoc u₁ u₂ u₃,
	{ mul := (*),
	one := 1,
	mul_assoc := λ u₁ u₂ u₃, ext $ mul_assoc u₁ u₂ u₃,

[joneugster]

ok, made your suggested changes and added the test case, thx.

Out of curiosity, why does this improve unfolding if you specify mul and one like this?

[Vierkantor]

IIRC, specifying mul means the unfolded version of units.group will give theorems stated using * instead of mul_one_class.to_has_mul.mul or something like that.

[eric-wieser]

I'm much happier with this than the previous priority-based solutions. Just a small comment, and Anne's suggestion to go.

[Vierkantor]

Thanks!

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests