bind variable with existential quantifier

Stream: new members

[Matt Yan]

Hi, I'm doing the natural number game, currently I have

d : mynat,
h : a = b + d

I want to do a rw ← le_iff_exists_add b a at h, to obtain b <= a, however le_iff_exists_add is formulated with the existential quantifier, how can I bind d into h using the existential quantifier?
image.png

[Mario Carneiro]

I would instead write this as have := (le_iff_exists_add _ _).2 \<_, h\>

[Matt Yan]

Thanks! It works! Can you explain what the \< \> brackets do?

[Mario Carneiro]

They are called "anonymous constructor brackets", they construct a proof of various tuple-like things, in particular p /\ q and \exists x : A, p x

[Mario Carneiro]

It is possible to do this with a rewrite but you would have to specify exactly the existential you want first, something like have h : \exists d, a = b + d := \<_, h\>

[Mario Carneiro]

and then rw <- le_iff_exists_add at h