Rewrite fails because of motive

Stream: lean4

[Op From The Start]

A rewrite that I am trying to do is

    /-
    p : 0 < sur_one.LO
    n_ge : is_ge (sur_one.L 0 p) (rsucc sur_zero)
    ⊢ (match (motive := (g : Game 1) → (αi : Ordinal.{u_1}) → αi < g.LO → Game αi) sur_one with
        | Game.mk α β p l r => l
        | Game.None => fun x x_1 => Game.None)
        0 p =
      sur_zero
    -/
    rw [sur_one]

Since sur_one appears in the goal. However it gives me the error failed to rewrite using equation theorems for 'sur_one'. I know from trying various things that it is probably due to the motive clause, but I don't know what a motive clause is and how to remove it. How do I put the specific value of sur_one into the goal?

[Op From The Start]

simp_rw worked in this case. Why did it work and not rw?

[Kyle Miller]

The motive is an important part of match expressions, and it explains how the type of the whole match expression depends on the value of the discriminant (sur_one in this case). If it's not provided, it's inferred, and the pretty printer only shows you the motive if it's more complicated than usual.

[Kyle Miller]

Maybe you might have some luck with using the split tactic first if you want to try using rw?

[Kyle Miller]

Op From The Start said:

simp_rw worked in this case. Why did it work and not rw?

simp can navigate some rewrites that are trickier to pull off without so-called congruence lemmas. Or, it also can do definitional unfolding that obviates the need for congruence lemmas at all, something that rw can't do.

You might also consider doing unfold sur_one, which can avoid the dependent type issues that rw has. It's sort of like simp_rw [sur_one], but if I remember correctly it unfolds only once, which is important for recursive functions.