Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-22 18:41 951bf1d9

View on Github →

refactor(data/set/basic): Remove _eq lemmas (#16572) This PR removes _eq lemmas from data.set.basic which asset a rfl propositional equality, in favour of the iff versions, and makes the latter simp lemmas if they weren't already.

Estimated changes

deleted theorem set.mem_compl_eq
modified theorem set.mem_compl_iff
deleted theorem set.mem_empty_eq
deleted theorem set.mem_image2_eq
deleted theorem set.mem_image_eq
deleted theorem set.mem_inter_eq
modified theorem set.mem_inter_iff
deleted theorem set.mem_sep_eq
modified theorem set.mem_sep_iff
modified theorem set.mem_union
deleted theorem set.mem_union_eq
deleted theorem set.nmem_set_of_eq
added theorem set.nmem_set_of_iff