Duplicate hypothesis

Stream: new members

[André Hernández-Espiet (Rutgers)]

For some reason, when I try to rewrite the definition of S it creates a "another" y. Why does it do that, and is there any way to avoid this? Thanks!

example (α : Type) (P : Prop) (S : Set α) (y : S) (hypS : S = {x | P}) : y ∈ {x | P} := by
  rw[hypS] at y

[Yaël Dillies]

This is to avoid your goal not typechecking anymore

[Patrick Massot]

You can probably work around this by using subst hypS instead of rw.

[Yaël Dillies]

If it did change y in place, your goal would have become y ∈ {x : S | P} while y : {x : α | P}. Since there's no Mem (Set {x : S | P}) {x : α | P}, this would fail.