Trouble rewriting inside set definition

Stream: new members

[Stepan Nesterov]

Why can I not rewrite de Morgan's law here?|

import algebraic_geometry.elliptic_curve.weierstrass
import ring_theory.valuation.basic
import algebra.order.monoid.with_zero.defs
import ring_theory.dedekind_domain.adic_valuation
open_locale discrete_valuation


variables {R : Type*} [comm_ring R]
{A : Type*} {K : Type*} [comm_ring A] [is_domain A] [is_dedekind_domain A] [field K] [algebra A K] [is_fraction_ring A K]
(v : is_dedekind_domain.height_one_spectrum A)

example (E : elliptic_curve K) : {v : is_dedekind_domain.height_one_spectrum A |
  ¬( (is_dedekind_domain.height_one_spectrum.valuation v) E.a₁ = 0 ∧ (is_dedekind_domain.height_one_spectrum.valuation v) E.a₂ = 0 ∧ (is_dedekind_domain.height_one_spectrum.valuation v) E.a₃ = 0 ∧  (is_dedekind_domain.height_one_spectrum.valuation v) E.a₄ = 0 ∧ (is_dedekind_domain.height_one_spectrum.valuation v) E.a₆ = 0 ∧ (is_dedekind_domain.height_one_spectrum.valuation v) E.Δ  = 0 ) }.finite :=
begin
  rw not_and_distrib,
end

[Eric Wieser]

simp_rw should work

[Stepan Nesterov]

It does!
What's the difference in general?

[Jireh Loreaux]

rw doesn't allow you to rewrite expressions involving bound variables (in this casev), but simp_rw does (among other things).

[Jireh Loreaux]

Often this is phrased as "rw doesn't rewrite under binders", which is not strictly true, but almost.