Force dot notation

Stream: general

[Patrick Johnson]

MWE:

structure T := (n : ℕ)
def T.m (x : T) := x

example {x : T} : x.m.m = x :=
begin
  let y := _, change x.m with y,
  -- T.m y = x
  refl,
end

After let, but before refl, the goal is displayed as T.m y = x instead of y.m = x. Tactic change y.m = x does not help. Is there a way to force the dot notation? Note that this is just a minimal example. It happened to me in a real proof and the goal became totally unreadable.