specializing forall to a set

Stream: Is there code for X?

[Eric Rodriguez]

example {α} (s : set α) {p : α → Prop} : (∀ a, p a) → ∀ a ∈ s, p a

I know by tauto will obviously do it, but I feel like this would be nice to apply without having to have ... by [some annoying rws], tauto and so on

[Yaël Dillies]

Note that you can view this as getting α → γ from α → β → γ by dropping the second argument.

[Yaël Dillies]

λ h a b, h a is, I think, a reasonable solution.

[Eric Rodriguez]

hmm, but what if s and p are fairly long? just judicious use of underscores?

[Yaël Dillies]

Yes :smiling_face:

[Eric Wieser]

Can you give more of a mwe? I can't see how the length of s and p would matter here