Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-03 11:51 f7e82d06

View on Github →

feat(tactic/lint): check for redundant simp lemmas (#2066)

  • chore(*): fix simp lemmas
  • feat(tactic/lint): check for redundant simp lemmas

Estimated changes

modified theorem dvd_mul_unit_iff
modified theorem mul_unit_dvd_iff
modified theorem finset.prod_const_one
modified theorem finset.sum_const_zero
modified theorem nat.cast_ne_zero
modified theorem commute.inv_left
modified theorem commute.inv_right
modified theorem commute.neg_left
modified theorem commute.neg_right
modified theorem commute.units_inv_left
modified theorem commute.units_inv_right
modified theorem free_semigroup.lift_of_mul
modified theorem list.prod_repeat
modified theorem list.sum_repeat
added theorem lie_algebra.map_lie'
modified theorem lie_algebra.map_lie
modified theorem ring_hom.comp_apply
modified theorem nat.rfind_dom'
modified theorem bool.coe_to_bool
modified theorem complex.abs_of_nat
modified theorem complex.of_real_ne_zero
modified theorem dfinsupp.erase_ne
modified theorem dfinsupp.filter_apply_neg
modified theorem dfinsupp.filter_apply_pos
modified theorem dfinsupp.mem_support_iff
modified theorem dfinsupp.single_eq_of_ne
modified theorem fin.mk_val
modified theorem finset.image_val_of_inj_on
modified theorem finset.mem_image_of_mem
modified theorem finset.mem_map_of_mem
modified theorem finset.piecewise_eq_of_mem
modified theorem finset.union_self
modified theorem fintype.card_unit
modified theorem fintype.univ_unit
modified theorem int.cast_ne_zero
modified theorem int.coe_nat_ne_zero
modified theorem int.mod_one
modified theorem int.mod_self
modified theorem int.mod_zero
modified theorem int.zero_mod
modified theorem list.cons_inj'
modified theorem list.cons_ne_nil
modified theorem list.count_cons_of_ne
modified theorem list.disjoint_singleton
modified theorem list.erase_of_not_mem
modified theorem list.index_of_cons_ne
modified theorem list.index_of_of_not_mem
modified theorem list.insert_of_mem
modified theorem list.insert_of_not_mem
modified theorem list.mem_insert_of_mem
modified theorem list.mem_map_of_inj
modified theorem list.singleton_disjoint
modified theorem list.sublists'_singleton
modified theorem list.kerase_cons_eq
modified theorem list.kerase_cons_ne
modified theorem list.kerase_of_not_mem_keys
modified theorem list.mem_keys_kerase_of_ne
modified theorem multiset.cons_erase
modified theorem multiset.count_cons_of_ne
modified theorem multiset.count_erase_of_ne
modified theorem multiset.disjoint_singleton
modified theorem multiset.erase_cons_tail
modified theorem multiset.erase_of_not_mem
deleted theorem multiset.forall_mem_ne
modified theorem multiset.map_id
modified theorem multiset.mem_map_of_inj
modified theorem multiset.ndinsert_of_mem
modified theorem multiset.ndinter_eq_inter
modified theorem multiset.ndunion_eq_union
modified theorem multiset.singleton_disjoint
modified theorem enat.coe_add_get
added theorem enat.get_coe
modified theorem num.add_to_nat
modified theorem num.cast_inj
modified theorem num.cast_le
modified theorem num.cast_lt
modified theorem num.dvd_to_nat
modified theorem num.land_to_nat
modified theorem num.ldiff_to_nat
modified theorem num.le_to_nat
modified theorem num.lor_to_nat
modified theorem num.lt_to_nat
modified theorem num.lxor_to_nat
modified theorem num.mul_to_nat
modified theorem num.of_nat_cast
modified theorem num.shiftl_to_nat
modified theorem num.shiftr_to_nat
modified theorem num.to_of_nat
modified theorem pos_num.add_to_nat
modified theorem pos_num.cast_add
modified theorem pos_num.cast_inj
modified theorem pos_num.cast_le
modified theorem pos_num.cast_lt
modified theorem pos_num.cast_mul
modified theorem pos_num.cast_succ
modified theorem pos_num.le_to_nat
modified theorem pos_num.lt_to_nat
modified theorem pos_num.mul_to_nat
modified theorem znum.cast_inj
modified theorem znum.cast_le
modified theorem znum.cast_lt
modified theorem znum.le_to_int
modified theorem znum.lt_to_int
modified theorem znum.to_of_int
modified theorem padic_int.add_def
modified theorem padic_int.mul_def
modified theorem padic_norm_z.norm_one
modified theorem pnat.to_pnat'_coe
modified theorem polynomial.coeff_C_mul_X
modified theorem polynomial.coeff_one
modified theorem rat.cast_ne_zero
modified theorem ennreal.inv_le_inv
modified theorem ennreal.two_ne_top
modified theorem ennreal.two_ne_zero
modified theorem ennreal.zero_lt_coe_iff
added theorem hyperreal.cast_div
added theorem hyperreal.coe_abs
added theorem hyperreal.coe_eq_coe
added theorem hyperreal.coe_le_coe
added theorem hyperreal.coe_lt_coe
added theorem hyperreal.coe_max
added theorem hyperreal.coe_min
modified theorem nnreal.coe_mk
modified theorem seq.join_cons
modified theorem set.ball_image_iff
modified theorem set.compl_compl
modified theorem set.image_id'
modified theorem set.image_id
modified theorem set.insert_of_has_insert
deleted theorem set.set_of_mem
modified theorem subtype.range_val
modified theorem subtype.val_range
modified theorem set.piecewise_eq_of_mem
modified theorem set.piecewise_eq_of_not_mem
modified theorem set.piecewise_insert_of_ne
modified theorem set.mem_sUnion
modified theorem sigma.mk.inj_iff
modified theorem subtype.mk_eq_mk
modified theorem sum.inl.inj_iff
modified theorem sum.inl_ne_inr
modified theorem sum.inr.inj_iff
modified theorem sum.inr_ne_inl
modified theorem zmod.cast_mod_int'
modified theorem zmod.cast_mod_nat'
deleted theorem equiv.perm.swap_mul_self
modified theorem coe_fn_coe_trans
modified theorem coe_sort_coe_trans
modified theorem false_ne_true
modified theorem imp_true_iff
modified theorem not_and_not_right
modified theorem lattice.Inf_singleton
modified theorem lattice.Sup_singleton
modified theorem lattice.infi_const
modified theorem lattice.supr_const
modified theorem filter.principal_ne_bot_iff
modified theorem localization.mk_self''
modified theorem localization.mk_self'
modified theorem localization.mk_self
modified theorem power_series.inv_of_unit_eq
modified theorem cardinal.mk_unit
modified theorem initial_seg.coe_coe_fn
modified theorem initial_seg.of_iso_apply
modified theorem ordinal.nat_cast_ne_zero
modified theorem ordinal.one_add_of_omega_le
modified theorem principal_seg.coe_coe_fn
modified theorem principal_seg.lt_le_apply
modified theorem principal_seg.trans_apply
modified theorem principal_seg.trans_top
deleted theorem mem_image
added theorem add_zero
added theorem zero_add_zero