All Questions
Tagged with automated-theorem-proving lean3
1
question
2
votes
1
answer
314
views
Eliminating "Exists Unique" in Lean 3
In Lean 3, similar to this question, I want to exhibit a witness of $x$ of $P(x)$, given that $\exists x,P(x)$. The difference is that I can also prove $\exists! x,P(x)$, so there is exactly 1 element ...