rewrite and instance fails

[craff]

This should type_check :

structure Group where
  carrier : Type u
  mul : carrier → carrier → carrier
  mul_assoc (a b c : carrier) : mul (mul a b) c = mul a (mul b c)
  e : carrier
  e_left (a : carrier) : mul e a = a
  e_right (a : carrier) : mul a e = a
  inv : carrier -> carrier
  inv_left (a : carrier) : mul (inv a) a = e
  inv_right (a : carrier) : mul a (inv a) = e

instance (G : Group) : Mul G.carrier where
  mul a b := G.mul a b

instance : CoeSort Group (Type u) where
  coe s := s.carrier

theorem resp_inv (G: Group) (a b : G)
  (h : a * b = G.e) : (a = G.inv b) :=
  let lem : (a * b) * (G.inv b) = G.e * (G.inv b) := by rw [h]
    by rw [Group.mul_assoc G a b (G.inv b)] at lem; -- FAILS AND SHOULD WORK
       {}

The above works if I replace all * by G.mul.

[semorrison]

@craff, it's not intended that this should work: rw only works syntactically, and will not unfold definitions, so it can not see that Group.mul and * are related.

How about raise this question on https://leanprover.zulipchat.com?