Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-06-30 11:29 48fb5b52

View on Github →

refactor(*): move all mk_simp_attribute commands to 1 file (#19223)

Estimated changes

modified theorem prod.map_mk
modified theorem set.inter_subset_left
modified theorem set.inter_univ
modified theorem set.mem_inter_iff
modified theorem set.mem_univ
modified theorem set.univ_inter
modified theorem set.image_eq_empty
modified theorem set.mem_preimage
modified theorem set.mem_range_self
modified theorem set.preimage_id
modified theorem set.preimage_inter
modified theorem set.preimage_univ
modified theorem set.range_id
modified theorem set.mem_prod
modified theorem set.prod_mk_mem_set_prod_eq
modified theorem set.range_prod_map
modified theorem set.univ_prod_univ
modified theorem subtype.coe_mk
modified theorem and_imp
modified theorem eq_iff_true_of_subsingleton
modified theorem forall_const
modified theorem heq_iff_eq
modified theorem equiv.apply_symm_apply
modified theorem equiv.symm_apply_apply
modified theorem equiv.symm_symm