Doubt defining classes

Stream: general

[Esteban Martínez Vañó]

I'm learning with the book Mathematics in Lean and I'm in Chapter 6, learning about structures.

I've defined the following class:

class Group₂ (α : Type*) where
  mul : α → α → α
  one : α
  inv : α → α
  mul_assoc : ∀ x y z : α, mul (mul x y) z = mul x (mul y z)
  mul_one : ∀ x : α, mul x one = x
  one_mul : ∀ x : α, mul one x = x
  mul_left_inv : ∀ x : α, mul (inv x) x = one

Following the book, I've also defined the following instances to use standard notation with this new class:

instance hasMulGroup₂ {α : Type*} [Group₂ α] : Mul α :=
  ⟨Group₂.mul⟩

instance hasOneGroup₂ {α : Type*} [Group₂ α] : One α :=
  ⟨Group₂.one⟩

instance hasInvGroup₂ {α : Type*} [Group₂ α] : Inv α :=
  ⟨Group₂.inv⟩

Now, to see if everything works I want to prove the following theorem:

theorem mul_right_inv_ {α : Type*} [Group₂ α] (x: α) : x * x⁻¹ = 1 := by
  sorry

But, when using the tactic "rw" with, for example, Group₂.mul_assoc, it doesn't work because it does not recognize the notation with the "*" instead of "mul".

How can this be solved?

Thanks in advance

[Ruben Van de Velde]

You'll need to write lemmas manually like theorem mul_one' (x) : x * 1 = x := Group₂.mul_one x and use those

[Esteban Martínez Vañó]

I see. But then, how does Lean do it with all the different structures that are defined and use this kind of notation?

[Esteban Martínez Vañó]

I've seen a way. If I add the " ' " to the definition of the class, then I can have the theorems without it :)

[Edward van de Meent]

the way Mathlib does this is by having Group extend Mul, such that the notation already is available in the fields of Group