Is simp only a sequence of intelligent rewrites?

Stream: general

[Assar Lannerborn]

Hi i am relatively new to lean. I encountered some proof using the tactic simp only [someprop]. Testing my understanding of simp and rw tactic, i thought i could just replace with rw [someprop], but the rw completely fails, "did not find instance of the pattern in the target expression". According to the documentation it states "The simplifier mindlessly rewrites until it can rewrite no more." I am probably missing something obvious but i can't figure it out.

[Assar Lannerborn]

the exact example is

example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := by
  rw [subset_def, inter_def, inter_def]
  rw [subset_def] at h
  simp only [mem_setOf]
  rintro x ⟨xs, xu⟩
  exact ⟨h _ xs, xu⟩

[Weiyi Wang]

(I had to guess a few declarations

import Mathlib
variable (s t : Set ℕ)
open Set
example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := by
  rw [subset_def, inter_def, inter_def]
  rw [subset_def] at h
  -- goal: ∀ x ∈ {a | a ∈ s ∧ a ∈ u}, x ∈ {a | a ∈ t ∧ a ∈ u}
  simp only [mem_setOf]
  rintro x ⟨xs, xu⟩
  exact ⟨h _ xs, xu⟩

)
This is the case where rw doesn't work because the expression being rewritten contains a binder (x), but simp can still do it

[Weiyi Wang]

https://leanprover-community.github.io/extras/pitfalls.html#rewriting-under-binders

[Assar Lannerborn]

ahh forgot to include the imports. I see so it's a unintended limitation it seems. Thanks for help and that resource :)

[Etienne Marion]

Note there is also simp_rw whose only purpose is to rewrite more efficiently than rw, in particular under binders (with the downside that it does not defer side conditions).