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

Stream: general

[Eric Wieser]

While reviewing 4087, I noticed a proof is repeated for both (∀ a ∈ range f, p a) and (∀ i, p (f i)). Is one of these considered more canonical? If its the latter, should docs#set.forall_range_iff be tagged @[simp]?

[Johan Commelin]

I prefer the second variant. And I think set.forall_range_iff would be a reasonable simp lemma.

[Johan Commelin]

@Eric Wieser Btw, thanks for reviewing!

[Eric Wieser]

No worries, seems like if I'm going to get something useful with geometric algebra in lean, I should look at how euclidean geometry is done

[Eric Wieser]

Shall I make a PR that tags it simp and see what blows up?

[Johan Commelin]

You can always try (-;

[Eric Wieser]

#4109

[Eric Wieser]

Seems not to cause any issues