Additional Expr recognizers needing theory imports

def Lean.Expr.coeTypeSet? (e : Expr) : Option Expr

If e is a coercion of a set to a type, return the set. Succeeds either for Set.Elem s terms or {x // x ∈ s} subtype terms.