[Merged by Bors] - chore(data/set/basic): simp attribute on mem_range_self

[sgouezel]

---

I thought for a long time that mem_range would fire before this one, and make it unusable by simp, but it turns out it's not the case (contrary to other lemmas with the same flavor: in

@[simp] theorem mem_image (f : α → β) (s : set α) (y : β) :
  y ∈ f '' s ↔ ∃ x, x ∈ s ∧ f x = y := iff.rfl

theorem mem_image_of_mem (f : α → β) {x : α} {a : set α} (h : x ∈ a) : f x ∈ f '' a :=
⟨_, h, rfl⟩

one can not put a simp attribute on the second lemma. I am not sure I understand the difference between the two situations, by the way).

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Run tests and docs
• Build mathlib
• Lint mathlib