Aesop fails on goal with bounded quantifiers

Stream: mathlib4

[Violeta Hernández]

Just came across this example which really feels like it should be within Aesop's capabilities, but doesn't work:

import Mathlib

example {α : Type*} {p : α → Prop} {a : α} {s : Set α} (h : ∀ a ∈ s, ∃ b ∈ s, p a ∧ p b) (h' : a ∈ s) :
    ∃ b ∈ s, p b := by
  aesop -- fails

Oddly enough, aesop has no problem solving this if we remove the bounded quantifiers

import Mathlib

example {α : Type*} {p : α → Prop} {a : α} (h : ∀ a, ∃ b, p a ∧ p b) :
    ∃ b, p b := by
  aesop -- suceeds

Is this a case of missing tags, or what's going on?

[Jannis Limperg]

Nested quantifiers in hypotheses (here: exists behind forall) are not supported particularly well. There is a fairly straightforward extension that could address this particular example, but in general this is actually a hard problem.

Without the bounded quantification, simp happens to simplify the hypothesis enough for Aesop to finish the rest; see aesop?.

[Violeta Hernández]

Is this straightforward extension a missing lemma? Or is it something more complex?

[Violeta Hernández]

Being able to solve this goal could compress a somewhat complex 8-line proof I have into a single aesop call