Unfold fails

Stream: new members

[Op From The Start]

I have the goal:

numeric
  ((match (motive := (x : PreNo) → right x → PreNo) addpre (PreNo.mk xL xR xLS xRS) (PreNo.mk yL yR yLS yRS) with
    | PreNo.mk L R a xRS => xRS)
    sr)

and I need to replace addpre with its definition, but I get error:

Tactic `unfold` failed to unfold `addpre` in
  numeric
    ((match (motive := (x : PreNo) → right x → PreNo) addpre (PreNo.mk xL xR xLS xRS) (PreNo.mk yL yR yLS yRS) with
      | PreNo.mk L R a xRS => xRS)
      sr)

The command right before is unfold rightm, and the goal before that is:

numeric (rightm (addpre (PreNo.mk xL xR xLS xRS) (PreNo.mk yL yR yLS yRS)) sr)

How can I expand this using the definitions?

[Op From The Start]

simp [addpre] also does nothing.

[Op From The Start]

unfold addpre also doesn't work on the goal numeric (rightm (addpre (PreNo.mk xL xR xLS xRS) (PreNo.mk yL yR yLS yRS)) sr) with a similar error.

[Aaron Liu]

Try split and then unfold it in the splitting equation

[Op From The Start]

The split fails:

[split.failure] `split` tactic failed at
      match (motive := (x : PreNo) → right x → PreNo) addpre (PreNo.mk xL xR xLS xRS) (PreNo.mk yL yR yLS yRS) with
      | PreNo.mk L R a xRS => xRS
    Internal error in `split` tactic: Failed to find match-expression discriminants

    Note: This error typically occurs when the `split` tactic's internal functions have been used in a new metaprogram

[Op From The Start]

I was able to get around it by doing unfold addpre earlier in the proof.