Nat.pair_unpair rewrite not working

Stream: new members

[Matt Diamond]

Here's something mildly annoying I just ran into:

import Mathlib

def f (P : Set ℕ) : ℕ →. ℕ := fun m => Nat.rfind (fun n => Part.assert (m.pair n ∈ P) fun _ => Part.some true)

example (P : Set ℕ) (P_re : REPred P) : Partrec (f P) :=
by
  apply Partrec.rfind
  rw [← Partrec₂.unpaired]
  unfold Nat.unpaired
  beta_reduce
  simp_rw [Nat.pair_unpair] -- why isn't this working?
  sorry

Any idea why the rewrite isn't working? It would seem to match perfectly... the goal state is:

Partrec fun n => Part.assert (Nat.pair (Nat.unpair n).1 (Nat.unpair n).2 ∈ P) fun x => Part.some true

which you would think could be rewritten to:

Partrec fun n => Part.assert (n ∈ P) fun x => Part.some true

but no dice.

[Aaron Liu]

Part.assert is dependent

[Matt Diamond]

ah

[Matt Diamond]

alright, maybe I just need to do a Partrec.of_eq instead

[Matt Diamond]

(don't finish this for me, though hints are welcome)

[Matt Diamond]

yeah I just needed to go the Partrec.of_eq route, thanks