rw can't find pattern

Stream: new members

[Bruno Bandeira Monteiro]

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]

That's right, rw cannot rewrite under binders (like this forall). Try tactic#simp_rw instead.

[Bruno Bandeira Monteiro]

It says it failed to simplify.

[Bruno Bandeira Monteiro]

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