Weird dynamic definition of a `Prop` via metaprogramming

Stream: lean4

[Malcolm Langfield]

Suppose I have a lemma of the form

import Mathlib.Tactic

def P (x : Nat) : Prop := sorry

lemma thing {x : Nat} : 1 + 1 = x -> P x := by
  norm_num
  -- Possibly a strange-looking custom tactic is called here as well???
  intros h
  assumption

I would like to replace the sorry in the definition of P with a tactic that will inspect the proof state of thing and define P to be whatever the antecedent of the target is. So in this example, it will be 2 = x and in general as we simplify the equality in the antecedent of the goal of thing, the definition of P will get correspondingly simpler.

I suspect someone may think this looks like an X-Y problem, but I'm really interested in figuring out how to do exactly the above (or an explanation why it's not possible).

Is this possible with Lean 4's metaprogramming facilities?

[Alex J. Best]

When the definition P is elaborated thing is not yet in the environment, or parsed / elaborated itself, so unless you made them mutual I don't see how the value of P can depend on what you do in thing

[Adam Topaz]

You could make a term elaborator for P

[Adam Topaz]

But then the P appearing in the type of thing would be elaborated first

[Malcolm Langfield]

Thanks so much for the tips guys! Mutual would be okay. @Adam Topaz It would be totally fine to have the P in thing elaborated as well. Do you think you could give me a pointer on how to do that? I don't understand how it's possible to refer to the goal in thing from P. Is there some sort of thing analogous to withMainContext that allows me to peer into the types of stuff that's been mutually defined? An example would be a godsend!