mathlib

71df310f - chore(*): remove instance binders in exists, for mathport (#9083)

chore(*): remove instance binders in exists, for mathport (#9083) Per @digama0's request at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Instance.20binders.20in.20exists. Instance binders under an "Exists" aren't allowed in Lean4, so we're backport removing them. I've just turned relevant `[X]` binders into `(_ : X)` binders, and it seems to all still work. (i.e. the instance binders weren't actually doing anything). It turns out two of the problem binders were in `infi` or `supr`, not `Exists`, but I treated them the same way. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>