Will simp go in a loop?

Stream: general

[Kenny Lau]

If I have two simp lemmas that are the inverse of each other, will simp go into a loop? For example:

@[simp] lemma mul_act : (g * h) • x = g • h • x :=
group_action.mul g h x

@[simp] lemma act_act : g • h • x = (g * h) • x :=
eq.symm $ group_action.mul g h x

[Mario Carneiro]

Why don't you try it? I think the answer is yes

[Kenny Lau]

I tried it and it succeeded

[Kenny Lau]

oh, it went in a loop when the goal can't be closed

[Simon Hudon]

I think you should think of simp lemmas as a way to decrease the complexity of your expressions. If they cancel each other, one of them must not be decreasing the complexity. Which one should you apply by name?