Quicker between `simp only` and `rw`

Stream: new members

[Anatole Dedecker]

I have a few proof that are one-line tactics where both rw and simp only work, so I was wondering which one is faster in general ? E.g for :

lemma nhds_cleft_sup_nhds_cright (a : α) [topological_space α] [linear_order α] :
  nhds_within a (Iic a) ⊔ nhds_within a (Ici a) = 𝓝 a :=
by simp only [← nhds_within_union, nhds_within_univ, Iic_union_Ici]

[Alex J. Best]

Put set_option profiler true above your lemma and you can time them yourself.

[Anatole Dedecker]

Thanks ! In case you were wondering, rw is about two times faster in this case