Quasigroup structure on Z

Stream: lean4

[Connor Gordon]

I've defined a class Quasigroup as follows:

class Quasigroup (α : Type*) extends Mul α :=
(ldiv : α → α → α)
(rdiv : α → α → α)
(mul_ldiv_cancel : ∀ a b, a * ldiv a b = b)
(rdiv_mul_cancel : ∀ a b, rdiv a b * b = a)
(ldiv_unique : ∀ a b x, a * x = b → x = ldiv a b)
(rdiv_unique : ∀ a b x, x * a = b → x = rdiv b a)

I would like to witness ℤ as a Quasigroup, where multiplication and left division are integer subtraction, while right division is integer addition. Toward this end, I have

instance : Quasigroup ℤ :=
{ mul := Int.sub
  ldiv := Int.sub
  rdiv := Int.add
  mul_ldiv_cancel := sorry
  rdiv_mul_cancel := sorry
  ldiv_unique := sorry
  rdiv_unique := sorry
  }

In trying to prove mul_ldiv_cancel, I would like for Lean to unpack mul as Int.sub. However, it is not doing this, and therefore I have been unable to make progress. Does anyone have any ideas what I should do?

[Alex J. Best]

What do you mean by it not unpacking, if I make a file

import Mathlib.Tactic
class Quasigroup (α : Type*) extends Mul α :=
(ldiv : α → α → α)
(rdiv : α → α → α)
(mul_ldiv_cancel : ∀ a b, a * ldiv a b = b)
(rdiv_mul_cancel : ∀ a b, rdiv a b * b = a)
(ldiv_unique : ∀ a b x, a * x = b → x = ldiv a b)
(rdiv_unique : ∀ a b x, x * a = b → x = rdiv b a)
instance : Quasigroup ℤ :=
{ mul := Int.sub
  ldiv := Int.sub
  rdiv := Int.add
  mul_ldiv_cancel := sorry -- ⊢ ∀ (a b : ℤ), a * Int.sub a b = b
  rdiv_mul_cancel := sorry
  ldiv_unique := sorry
  rdiv_unique := sorry
  }

I see the goal with Int.sub in

[Alex J. Best]

Ah I see, you can just do simp [(· * ·)]

[Kyle Miller]

It's usually better to use notation rather than using the underlying functions:

instance : Quasigroup ℤ :=
{ mul := (· - ·)
  ldiv := (· - ·)
  rdiv := (· + ·)
  mul_ldiv_cancel := by simp [(· * ·)]
  rdiv_mul_cancel := by simp [(· * ·)]
  ldiv_unique := by intros; subst_vars; simp [(· * ·)]
  rdiv_unique := by intros; subst_vars; simp [(· * ·)] }

[Connor Gordon]

Ah, that works! Thank you very much!

[Julian Berman]

@Kyle Miller is that because the goals look nicer or is there some more "important" reason?

[Kyle Miller]

It's because there are no lemmas about Int.sub or Int.add, but there are lemmas about - for Int and + for Int.

[Eric Wieser]

Referring to them by name would be fine if you use the names HAdd.add or HSub.sub, as these are the names the lemmas are about