Porting of exists_least_of_bdd vs leastOfBdd

Stream: mathlib4

[Hunter Monroe]

The reason exists_least_of_bdd exists is to avoid the assumption of DecidablePred like leastOfBdd (these implement the least number principle). However, the ported version of both now use DecidablePred which is duplicative and inconsistent with the documentation. The only place exists_least_of_bdd is used has the porting note "port of Int.exists_least_of_bdd requires DecidablePred, so we use classical". Is there a reason exists_least_of_bdd cannot avoid DecidablePred?

[Eric Rodriguez]

(this is docs#Int.exists_least_of_bdd)

[Yury G. Kudryashov]

I think that it's a porting bug. I'm slowly cleaning up these bugs but I'm far from being done.

[Yury G. Kudryashov]

I'm going to fix these two in a few minutes.

[Yury G. Kudryashov]

#11163

[Yury G. Kudryashov]

This file was ported manually before mathport.

[Hunter Monroe]

Many thanks!