simp lemmas priority

Stream: general

[Yury G. Kudryashov]

Hi, how does Lean decide which simp lemma to apply? I'm trying to add

@[simp] theorem ball_image_iff {f : α → β} {s : set α} {p : β → Prop} :
  (∀ y ∈ f '' s, p y) ↔ (∀ x ∈ s, p (f x)) :=
iff.intro
  (assume h a ha, h _ $ mem_image_of_mem f ha)
  (ball_image_of_ball)

but Lean always applies mem_image before it, and for ∀ y ∈ f '' s, p y it leads to worse results. I tried adding @[simp, priority=20] to mem_image, with no effect.

[Floris van Doorn]

I think simp simplifies starting at the leaves (atomic expressions) and then building up. So it will always simplify subexpressions of t before simplifying t. You probably get the desired behavior if you put the LHS of the above theorem in simp-normal form.