Commit 2021-09-08 12:15 71df310f

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.