Applying tactics to PSigma equalities

Stream: Is there code for X?

[Arnav Sabharwal]

Hello!

Is there a clean way to apply tactics as one normally would when dealing with a PSigma equality? My question is captured by the following MWE:

open Nat

def natId (x : Nat) : Nat := x

example : (Σ' (natId : Nat → Nat), natId = (fun (x : Nat) => natId x)) := by
  -- creates unwanted synthetic hole
  apply PSigma.mk
  sorry

More generally, what is the proper way to go about proving PSigma equalities when the first term of the dependent pair could just as well have been in the context rather than in the goal? apply PSigma.mk creates unwanted synthetic holes, unfortunately, what I would like is something which provides access to natId but doesn't prevent tactic application due to the dependent pair

Thanks!

[Arnav Sabharwal]

(deleted)

[Matt Diamond]

you might have more luck using Subtype instead of PSigma, as I believe there's more API around the former

[Matt Diamond]

though I'm also not sure I understand your question... what's the desired tactic state?