## Stream: general

### Topic: simp_rw

#### Michael Beeson (Aug 31 2020 at 19:36):

simp_rw is supposed to rewrite under quantifiers. But: I have
 h1 : ∀ (u a : M), u ∈ x ∧ ¬a ∈ u → u ∪ single a ∈ x 
and
 simp_rw and_comm at h1, 
fails. Why?

The error message is "simplify tactic failed to simplify".

I expected and_comm to rewrite once. But maybe it just rewrites to what it considers "canonical order".
That is, I thought, if it gets b /\ a it should produce a /\ b and vice-versa, but maybe it always produces a /\ b?

#backticks

#### Kenny Lau (Aug 31 2020 at 19:39):

also could you describe the error in more detail than "fails"?

#### Kenny Lau (Aug 31 2020 at 19:39):

you can start by copying the error message

#### Floris van Doorn (Aug 31 2020 at 20:25):

simp and simp_rw simplify until they hit a normal form. Since and_comm can be applied over and over again, it has to decide whether u ∈ x ∧ ¬a ∈ u is simpler or (¬a ∈ u) ∧ u ∈ x is simpler. I think it decided the former, and therefore didn't rewrite.

You could try simp_rw and_comm (_ ∈ x) at h1. If that doesn't work, please give a #mwe.

Last updated: May 14 2021 at 04:22 UTC