mem_upperBounds

Stream: mathlib4

[Violeta Hernández]

Is there any reason docs#mem_upperBounds is not tagged simp?

[Anne Baanen]

(Historical note: looks like these were added by @Yury G. Kudryashov in mathlib3#2877.)

The only reason I can quickly figure out is that the rewrite might conflict with docs#mem_upperBounds_iff_subset_Iic. But mem_Iic is a @[simp] lemma, so that doesn't seem to be particularly compelling either. So I would say: try adding the attribute and see if anything breaks!