# Zulip Chat Archive

## Stream: new members

### Topic: rw can't find pattern

#### Bruno Bandeira Monteiro (Dec 05 2021 at 03:43):

Hi,

I'm still leaning to use lean. So I'm trying to formalize some basic theorems.

I can often use rw without any problems, but in a particular situation it seems to not find the pattern.

This is the state in the middle of a proof:

before-rw.png

Notice that the consequent of the hypothesis dni1 almost matches the goal, but it says x is not in the complement of P. To rewrite this part of dni1 into "x is in P", i wrote a lemma (probably already in mathlib):

```
lemma notin_compl_iff_in (a : set N) (x : N): (x ∉ a.compl) ↔ x ∈ a := begin split, by_cases (a x), intro, exact h, intro b, exfalso, exact b h, intros h1 h2, exact h2 h1, end
```

Using the command

```
rw notin_compl_iff_in at dni1,
```

It rewrites the antecedent of dni1 "z \notin P.compl" into "z \in P", but using the same command again it gives me an error, even though there is a second occurrence of the same pattern. The error I get:

after-rw.png

The only difference I can see is that x is a bound variable, and z is a free variable, but I dont see why this would matter.

Any help is appreciated

#### Reid Barton (Dec 05 2021 at 03:59):

That's right, `rw`

cannot rewrite under binders (like this `forall`

). Try tactic#simp_rw instead.

#### Bruno Bandeira Monteiro (Dec 05 2021 at 04:04):

It says it failed to simplify.

#### Bruno Bandeira Monteiro (Dec 05 2021 at 04:06):

Do you see a simple way to solve this without having to eliminate these quantifiers?

Last updated: Dec 20 2023 at 11:08 UTC