Rewrite fails in `ite` !4#4205

Stream: mathlib4

[Nikolas Kuhn]

The following is not working for me. The result I get is tactic 'rewrite' failed, motive is not type correct. Does anyone understand what the issue is? (maybe something with the ite?)

lemma test (n: ℕ) : (if n % 4 = 1 then (1: ℤ) else -1) = (-1) ^ (n / 2) := by
  nth_rewrite 1 [← Nat.div_add_mod n 4]
  sorry

[Nikolas Kuhn]

Strangely, changing nt_rewrite 1 to rw works (but rewrites both occurences of n).

[Eric Wieser]

There are three occurences of n in this expression, but one isn't visible in the goal view (it's in the Decidable argument toite)

[Eric Wieser]

The first two have to be rewritten together

[Kevin Buzzard]

This demonstrates exactly what the "motive is not type correct" error is about.

[Nikolas Kuhn]

Ah, nice. Thanks! That fixes the issue for my purpose, since I wanted to change the third n anyway, but out of curiosity: Is there a neat way to change the first two occurences of n together? (i.e. easier than congruence for ite)

[Ruben Van de Velde]

In this case, conv_lhs, perhaps