monoid.mul appearing instead of has_mul.mul

Stream: general

[Chris Hughes]

Why does monoid.mul appear in the begin end here instead of has_mul.mul? Is there a nice solution to this problem?

def one_by_one_equiv {one R : Type*} [unique one] [ring R] : matrix one one R ≃r R :=
{ to_fun := λ M, M (default _) (default _),
  inv_fun := λ x _ _, x,
  left_inv := λ _, matrix.ext
    (λ i j, by rw [unique.eq_default i, unique.eq_default j]),
  right_inv := λ _, rfl,
  hom :=
  { map_one := rfl,
    map_mul := begin
      assume x y,


    end,
    map_add := λ _ _, rfl } }

[Mario Carneiro]

this is what happens when you try to define a layered structure all in one go. If you first define the equiv part and then the ring equiv I think it will use has_mul.mul