# Zulip Chat Archive

## 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?

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

#### 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