Should `set.forall_range_iff` be tagged `simp`?

Stream: general

[Eric Wieser]

On a vaguely related note, is this a sane simp lemma?

@[simp] theorem forall_imp_swap {p : Prop} {q : α → Prop} : (∀ a, p → q a) ↔ (p → ∀ a, q a) := forall_swap

[Scott Morrison]

What effect does it have? I'm generally in favour or more simp lemmas. Typically I explore adding @[simp] whenever I get grumpy that simp didn't do something I thought it should have --- do you have an example where this helps?

[Eric Wieser]

A contrived one in an editor buffer I don't have access to right now. Essentially it transformed things into a form where #4109 and #4117 can kick in; and pushing binders to a smaller scope feels like a simplification to me

[Eric Wieser]

I've opened #4143 to try out that lemma