Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-27 18:19 4cc0d525

View on Github →

refactor(data/set/basic): simpler proofs (#5920) This replaces many uses of simp and finish with direct term proofs to speed up the overall compilation of the file. This PR is WIP in the sense that not all of set.basic is converted, but there are no dependencies between the changes so this can be merged at any point.

Estimated changes

modified theorem set.ball_empty_iff
modified theorem set.compl_comp_compl
modified theorem set.compl_subset_comm
modified theorem set.compl_subset_compl
modified theorem set.compl_union_self
modified theorem set.diff_subset
modified theorem set.empty_inter
modified theorem set.empty_not_nonempty
modified theorem set.empty_subset
modified theorem set.empty_union
modified theorem set.eq_of_mem_singleton
modified theorem set.eq_of_subset_of_subset
modified theorem set.eq_sep_of_subset
modified theorem set.eq_univ_of_univ_subset
modified theorem set.forall_insert_of_forall
modified theorem set.forall_not_of_sep_empty
modified theorem set.forall_of_forall_insert
modified theorem set.insert_eq
modified theorem set.insert_nonempty
modified theorem set.insert_subset_insert
modified theorem set.insert_union
modified theorem set.inter_assoc
modified theorem set.inter_comm
modified theorem set.inter_empty
modified theorem set.inter_self
modified theorem set.inter_subset_inter
modified theorem set.inter_subset_left
modified theorem set.inter_subset_right
modified theorem set.mem_insert
modified theorem set.mem_insert_iff
modified theorem set.mem_inter
modified theorem set.mem_of_mem_insert_of_ne
modified theorem set.mem_of_mem_inter_left
modified theorem set.mem_of_mem_inter_right
modified theorem set.mem_of_mem_of_subset
modified theorem set.mem_of_subset_of_mem
modified theorem set.mem_sep_eq
modified theorem set.mem_singleton
modified theorem set.mem_singleton_iff
modified theorem set.mem_singleton_of_eq
modified theorem set.ne_empty_iff_nonempty
modified theorem set.ne_insert_of_not_mem
modified theorem set.nonempty.ne_empty
modified theorem set.nonempty_diff
modified theorem set.not_mem_empty
modified theorem set.not_not_mem
modified theorem set.not_subset
modified theorem set.pair_comm
modified theorem set.pair_eq_singleton
modified theorem set.sep_subset
modified theorem set.sep_univ
modified theorem set.singleton_def
modified theorem set.singleton_subset_iff
modified theorem set.singleton_union
modified theorem set.subset_insert
modified theorem set.subset_inter
modified theorem set.union_assoc
modified theorem set.union_comm
modified theorem set.union_compl_self
modified theorem set.union_empty
modified theorem set.union_insert
modified theorem set.union_self
modified theorem set.union_singleton
modified theorem set.union_subset_union
added theorem and_congr_left'
added theorem and_congr_left
added theorem and_congr_right'
added theorem ball_or_left_distrib
added theorem bex_eq_left
added theorem bex_or_left_distrib
added theorem or_congr_left
added theorem or_congr_right