rw not working as expected

Stream: mathlib4

[Moritz Firsching]

During porting Data.List.ModEq, mathlib4#1566, I was trying to rewrite something that had worked in mathlib, but the rw doesn't work anymore for reasons that I don't understand.
Here's the problem:
https://github.com/leanprover-community/mathlib4/blob/ff4cf7bc6e1ed3387ea948d20d4c66333c64e892/Mathlib/Data/List/ModEq.lean#L42-L44
at that time this is

this: rotate (a :: l) (Nat.succ n) = rotate (l ++ [a]) n

and the goal is

get (rotate (a :: l) (Nat.succ n)) { val := m, isLt := (_ : m < length (rotate (a :: l) (Nat.succ n))) } =
  get (a :: l)
    { val := Nat.succ (m + n) % length (a :: l), isLt := (_ : Nat.succ (m + n) % length (a :: l) < length (a :: l)) }

When clicking on rotate (a :: l) (Nat.succ n) in both parts, I get @rotate α (a :: l) (Nat.succ n) : List α, so the seem to be of the same type.
However the rw fails with

tactic 'rewrite' failed, motive is not type correct

What is going on? How to fix these kind of problems (that occur also in other parts of the file)

[Kevin Buzzard]

Have you tried using simp only instead?

[Moritz Firsching]

yes, that didn't help

[Kevin Buzzard]

And it worked in lean 3?

[Reid Barton]

Yeah this is normal rw behavior; what was the Lean 3 version?

[Arien Malec]

I’ve had the same issues in some open PRs. My hypothesis is Lean now unfolds to structure fields or behind functions rather than seeing this is a higher level concept and won’t rewrite or simplify.

[Reid Barton]

I would check what the actual proof state (i.e. goal & this hypothesis) is at that point in the Lean 3 proof

[Reid Barton]

It seems plausible that something has gone differently already

[Arien Malec]

Ah, I didn't read correctly -- my separate issue is that rw/simp just does nothing.