# Can Lean simp arguments be ordered?

I want to simplify the expression 0 * 1 * 1 * 1 * 0 using simp only [mul_zero, zero_mul]. I would like mul_zero to fire first, so that the entire expression is simplified to zero in only one step. If mul_zero fires first, I would expect the simplification process to take 4 steps, due to there being one step to eliminate each 1.

Is there a way I can tell Lean to prioritize which simplification lemma to try first?

• My understanding is that simp operates by deeply entering expressions, seeing what applies, then working outwards. That means it'll see the 0 * 1 first no matter what. I could be wrong, though. Commented Feb 14, 2022 at 20:44

Using mathlib's simp_rw, you can order your lemmas:

example (a : nat) : a + 0 * 1 * 1 * 1 * 0 = a := by simp_rw [mul_zero, add_zero]


simp_rw [lemma1, lemma2] does the hand-waved equivalent of simp only [lemma1], simp only [lemma2].

Lean's simp arguments are already ordered:

def a := 0
def b := 0
def c := 0
def f : ℕ → ℕ := default
@[simp] lemma k (x) : f x = b := rfl
@[simp] lemma l : f b = c := rfl

example : f (f a) = c := by simp only [k, l]
example : f (f a) = c := by simp only [l, k] -- failure!