feat(tactic/choose): derive local nonempty instances (#3842)
This allows `choose!` to work even in cases like `{A : Type} (p : A -> Prop) (h : ∀ x : A, p x → ∃ y : A, p y)`, where we don't know that `A` is nonempty because it is generic, but it can be derived from the inhabitance of other variables in the context of the `∃ y : A` statement. As requested on zulip: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/non.20dependent.20chooser/near/207126587
