simp-red-lint.lean

/- REDUNDANT SIMP LEMMAS.
Some simp lemmas can be derived from other simp lemmas using `by simp`: -/

-- topology/metric_space/hausdorff_distance.lean
#print metric.Hausdorff_dist_closure /- is redundant: by simp [metric.Hausdorff_dist_closure₁, metric.Hausdorff_dist_closure₂] -/
#print metric.Hausdorff_dist_self_closure /- is redundant: by simp [metric.Hausdorff_dist_self_zero, metric.Hausdorff_dist_closure₂] -/
#print emetric.Hausdorff_edist_self_closure /- is redundant: by simp [emetric.Hausdorff_edist_self, emetric.Hausdorff_edist_closure₂] -/
#print emetric.Hausdorff_edist_closure /- is redundant: by simp [emetric.Hausdorff_edist_closure₁, emetric.Hausdorff_edist_closure₂] -/

-- topology/category/Top/opens.lean
#print topological_space.opens.map_comp_obj_unop /- is redundant: by simp [topological_space.opens.map_comp_obj] -/
#print topological_space.opens.op_map_comp_obj /- is redundant: by simp [topological_space.opens.map_comp_obj_unop, opposite.unop_op, category_theory.functor.op_obj] -/
#print topological_space.opens.map_id_obj' /- is redundant: by simp [topological_space.opens.map_id_obj] -/
#print topological_space.opens.map_id_obj_unop /- is redundant: by simp [topological_space.opens.map_id_obj] -/
#print topological_space.opens.map_comp_obj' /- is redundant: by simp [topological_space.opens.map_obj, topological_space.opens.map_comp_obj] -/
#print topological_space.opens.op_map_id_obj /- is redundant: by simp [opposite.op_unop, topological_space.opens.map_id_obj_unop, category_theory.functor.op_obj] -/

-- topology/category/Top/open_nhds.lean
#print topological_space.open_nhds.op_map_id_obj /- is redundant: by simp [opposite.op_unop, category_theory.functor.op_obj, topological_space.open_nhds.map_id_obj_unop] -/
#print topological_space.open_nhds.map_id_obj' /- is redundant: by simp [topological_space.open_nhds.map_id_obj] -/
#print topological_space.open_nhds.map_id_obj_unop /- is redundant: by simp [topological_space.open_nhds.map_id_obj] -/

-- topology/category/Top/basic.lean
#print Top.id_app /- is redundant: by simp [category_theory.coe_id] -/

-- topology/algebra/module.lean
#print continuous_linear_equiv.coe_apply /- is redundant: by simp [coe_fn_coe_base] -/
#print continuous_linear_map.id_apply /- is redundant: by simp [id.def, continuous_linear_map.coe_id'] -/

-- tactic/converter/binders.lean
#print mem_image /- is redundant: by simp [set.mem_image] -/

-- set_theory/zfc.lean
#print Set.mem_singleton' /- is redundant: by simp [Set.mem_empty, or_false, Set.mem_insert] -/

-- set_theory/pgame.lean
#print pgame.relabel_move_right /- is redundant: by simp [equiv.symm_apply_apply, pgame.relabel_move_right'] -/
#print pgame.relabel_move_left /- is redundant: by simp [pgame.relabel_move_left', equiv.symm_apply_apply] -/

-- set_theory/ordinal.lean
#print ordinal.nat_cast_ne_zero /- is redundant: by simp [ordinal.nat_cast_eq_zero, ne.def] -/

-- set_theory/cardinal.lean
#print cardinal.mk_unit /- is redundant: by simp [cardinal.mk_punit] -/
#print cardinal.nat_cast_pow /- is redundant: by simp [cardinal.pow_cast_right, nat.cast_pow] -/

-- ring_theory/power_series.lean
#print mv_power_series.coeff_zero /- is redundant: by simp [add_monoid_hom.map_zero] -/
#print mv_power_series.coeff_zero_C /- is redundant: by simp [mv_power_series.constant_coeff_C, mv_power_series.coeff_zero_eq_constant_coeff_apply] -/
#print power_series.inv_of_unit_eq /- is redundant: by simp [eq_self_iff_true, units.mk0_val, power_series.inv_of_unit_eq'] -/
#print power_series.coeff_zero_C /- is redundant: by simp [power_series.coeff_zero_eq_constant_coeff_apply, power_series.constant_coeff_C] -/
#print power_series.constant_coeff_one /- is redundant: by simp [ring_hom.map_one] -/
#print mv_power_series.coeff_zero_one /- is redundant: by simp [mv_power_series.coeff_zero_eq_constant_coeff_apply, mv_power_series.constant_coeff_one] -/
#print power_series.coeff_zero_mul_X /- is redundant: by simp [power_series.coeff_zero_eq_constant_coeff_apply, power_series.constant_coeff_X, mul_zero, ring_hom.map_mul] -/
#print power_series.constant_coeff_zero /- is redundant: by simp [ring_hom.map_zero] -/
#print mv_power_series.constant_coeff_zero /- is redundant: by simp [ring_hom.map_zero] -/
#print mv_power_series.constant_coeff_one /- is redundant: by simp [ring_hom.map_one] -/
#print mv_power_series.coeff_zero_X /- is redundant: by simp [mv_power_series.coeff_zero_eq_constant_coeff_apply, mv_power_series.constant_coeff_X] -/
#print power_series.coeff_zero_X /- is redundant: by simp [power_series.coeff_zero_eq_constant_coeff_apply, power_series.constant_coeff_X] -/
#print mv_power_series.coeff_zero_mul_X /- is redundant: by simp [mv_power_series.coeff_zero_eq_constant_coeff_apply, mv_power_series.constant_coeff_X, mul_zero, ring_hom.map_mul] -/
#print power_series.coeff_zero_one /- is redundant: by simp [if_true, eq_self_iff_true, power_series.coeff_one] -/
#print mv_power_series.inv_of_unit_eq /- is redundant: by simp [eq_self_iff_true, mv_power_series.inv_of_unit_eq', units.mk0_val] -/

-- ring_theory/multiplicity.lean
#print multiplicity.one_left /- is redundant: by simp [multiplicity.multiplicity_unit, is_unit_one] -/

-- ring_theory/localization.lean
#print localization.coe_is_unit /- is redundant: by simp [subtype.val_prop', localization.coe_is_unit'] -/
#print localization.of_is_unit /- is redundant: by simp [subtype.val_prop', localization.of_is_unit'] -/
#print localization.fraction_ring.mk_eq_div /- timeout -/

-- ring_theory/ideal_operations.lean
#print ideal.zero_eq_bot /- is redundant: by simp [submodule.zero_eq_bot] -/
#print ideal.add_eq_sup /- is redundant: by simp [submodule.add_eq_sup] -/

-- ring_theory/algebra_operations.lean
#print submodule.one_mul /- is redundant: by simp [one_mul] -/
#print submodule.mul_one /- is redundant: by simp [mul_one] -/

-- ring_theory/algebra.lean
#print algebra.id.smul_eq_mul /- is redundant: by simp [smul_eq_mul] -/

-- order/complete_lattice.lean
#print lattice.infi_const /- is redundant: by simp [lattice.cinfi_const] -/
#print lattice.supr_const /- is redundant: by simp [lattice.csupr_const] -/
#print lattice.Sup_singleton /- is redundant: by simp [lattice.cSup_singleton] -/
#print lattice.infi_false /- is redundant: by simp [lattice.infi_neg, not_false_iff] -/
#print lattice.Inf_singleton /- is redundant: by simp [lattice.cInf_singleton] -/
#print lattice.supr_true /- is redundant: by simp [lattice.supr_pos] -/
#print lattice.supr_false /- is redundant: by simp [lattice.supr_neg, not_false_iff] -/
#print lattice.infi_true /- is redundant: by simp [lattice.infi_pos] -/

-- number_theory/pell.lean
#print pell.xn_one /- is redundant: by simp [add_zero, one_mul, pell.yn_zero, pell.xn_succ, pell.xn_zero, mul_zero] -/
#print pell.yn_one /- is redundant: by simp [add_zero, pell.yn_zero, pell.xn_zero, zero_mul, pell.yn_succ] -/

-- number_theory/dioph.lean
#print vector_allp_singleton /- is redundant: by simp [vector_allp_nil, and_true, vector_allp_cons] -/

-- logic/basic.lean
#print coe_fn_coe_trans /- is redundant: by simp [coe_fn_coe_base] -/
#print false_ne_true /- is redundant: by simp [false_iff, not_true, eq_iff_iff] -/
#print not_and_not_right /- is redundant: by simp [not_and, not_not] -/
#print bex_imp_distrib /- is redundant: by simp [exists_imp_distrib] -/
#print coe_sort_coe_trans /- is redundant: by simp [coe_sort_coe_base] -/
#print not_exists_not /- is redundant: by simp [not_exists, not_not] -/
#print imp_true_iff /- is redundant: by simp [forall_true_iff] -/

-- linear_algebra/tensor_product.lean
#print tensor_product.lift.tmul' /- is redundant: by simp [tensor_product.lift.tmul, linear_map.to_fun_eq_coe] -/

-- linear_algebra/special_linear_group.lean
#print matrix.special_linear_group.det_coe_matrix /- is redundant: by simp [matrix.special_linear_group.det_coe_fun] -/

-- linear_algebra/finite_dimensional.lean
#print finite_dimensional.findim_fin_fun /- is redundant: by simp [fintype.card_fin, finite_dimensional.findim_fintype_fun_eq_card] -/

-- linear_algebra/basic.lean
#print linear_equiv.coe_apply /- is redundant: by simp [coe_fn_coe_base] -/
#print submodule.map_subtype_top /- is redundant: by simp [submodule.range_subtype, submodule.map_top] -/
#print linear_equiv.map_ne_zero_iff /- is redundant: by simp [linear_equiv.map_eq_zero_iff, ne.def] -/

-- group_theory/free_group.lean
#print free_group.map_pure /- is redundant: by simp [is_lawful_applicative.map_pure] -/
#print free_group.pure_bind /- is redundant: by simp [is_lawful_monad.pure_bind] -/

-- group_theory/free_abelian_group.lean
#print free_abelian_group.pure_bind /- is redundant: by simp [is_lawful_monad.pure_bind] -/
#print free_abelian_group.map_pure /- is redundant: by simp [is_lawful_applicative.map_pure] -/

-- group_theory/congruence.lean
#print add_con.add_con_gen_idem /- is redundant: by simp [add_con.add_con_gen_of_add_con] -/
#print con.con_gen_idem /- is redundant: by simp [con.con_gen_of_con] -/

-- geometry/manifold/smooth_manifold_with_corners.lean
#print ext_chart_at_to_inv /- is redundant: by simp [local_equiv.left_inv, mem_ext_chart_source] -/
#print model_with_corners_left_inv /- is redundant: by simp [set.mem_univ, local_equiv.left_inv, model_with_corners.source_eq] -/

-- data/zmod/basic.lean
#print zmod.cast_mod_nat /- is redundant: by simp [zmod.cast_mod_nat', pnat.pos] -/
#print zmodp.cast_mod_nat /- is redundant: by simp [zmod.cast_mod_nat'] -/
#print zmod.cast_mod_int /- is redundant: by simp [zmod.cast_mod_int', pnat.pos] -/
#print zmodp.cast_val /- is redundant: by simp [zmod.cast_val] -/
#print zmodp.cast_mod_int /- is redundant: by simp [zmod.cast_mod_int'] -/

-- data/vector2.lean
#print vector.nth_cons_zero /- is redundant: by simp [vector.nth_zero, vector.head_cons] -/

-- data/sum.lean
#print sum.inl.inj_iff /- is redundant: by simp [] -/
#print sum.inl_ne_inr /- is redundant: by simp [] -/
#print sum.inr_ne_inl /- is redundant: by simp [] -/
#print sum.inr.inj_iff /- is redundant: by simp [] -/

-- data/subtype.lean
#print subtype.mk_eq_mk /- is redundant: by simp [] -/

-- data/sigma/basic.lean
#print sigma.mk.inj_iff /- is redundant: by simp [] -/

-- data/set/lattice.lean
#print set.compl_bUnion /- is redundant: by simp [set.compl_Union] -/
#print set.mem_sUnion /- is redundant: by simp [exists_prop, set.mem_set_of_eq] -/

-- data/set/function.lean
#print set.piecewise_insert_self /- is redundant: by simp [set.mem_insert_iff, set.piecewise_eq_of_mem, true_or, eq_self_iff_true] -/

-- data/set/finite.lean
#print set.card_singleton /- is redundant: by simp [list.pmap, list.map, fintype.card_of_subsingleton] -/

-- data/set/basic.lean
#print set.compl_compl /- is redundant: by simp [lattice.neg_neg] -/
#print set.image_id /- is redundant: by simp [id.def, set.image_id'] -/
#print set.mem_singleton /- is redundant: by simp [set.mem_singleton_iff, eq_self_iff_true] -/
#print set.mem_image /- is redundant: by simp [mem_image] -/
#print set.not_not_mem /- is redundant: by simp [not_not] -/
#print subtype.range_val /- is redundant: by simp [set.subtype.val_range, set.set_of_mem] -/
#print subtype.val_range /- is redundant: by simp [set.subtype.val_range] -/
#print set.prod_mk_mem_set_prod_eq /- is redundant: by simp [set.mem_prod] -/
#print set.pair_eq_singleton /- is redundant: by simp [set.mem_singleton, lattice.insert_of_has_insert, set.insert_eq_of_mem] -/
#print set.insert_of_has_insert /- is redundant: by simp [lattice.insert_of_has_insert] -/
#print set.set_of_mem_eq /- is redundant: by simp [set.set_of_mem] -/

-- data/seq/seq.lean
#print seq.join_cons_nil /- is redundant: by simp [seq.nil_append, seq.join_cons] -/
#print seq.join_cons_cons /- is redundant: by simp [seq.join_cons, seq.cons_append] -/

-- data/real/nnreal.lean
#print nnreal.sub_le_self /- is redundant: by simp [zero_le, le_add_iff_nonneg_right, nnreal.sub_le_iff_le_add] -/

-- data/real/ennreal.lean
#print ennreal.sub_infty /- is redundant: by simp [lattice.le_top, ennreal.sub_eq_zero_of_le] -/
#print ennreal.coe_le_coe /- is redundant: by simp [with_top.coe_le_coe] -/
#print ennreal.not_top_le_coe /- is redundant: by simp [lattice.top_le_iff, ennreal.coe_ne_top] -/
#print ennreal.max_zero_right /- is redundant: by simp [zero_le, max_eq_left] -/
#print ennreal.zero_sub /- is redundant: by simp [zero_le, ennreal.sub_eq_zero_of_le] -/
#print ennreal.coe_add /- is redundant: by simp [with_bot.coe_add] -/
#print ennreal.coe_sub_infty /- is redundant: by simp [ennreal.sub_infty] -/
#print ennreal.two_ne_top /- is redundant: by simp [ennreal.one_ne_top, ennreal.bit0_eq_top_iff] -/
#print ennreal.coe_pos /- is redundant: by simp [ennreal.zero_lt_coe_iff] -/
#print ennreal.coe_nonneg /- is redundant: by simp [zero_le] -/
#print ennreal.coe_nat /- is redundant: by simp [with_top.coe_nat] -/
#print ennreal.two_ne_zero /- is redundant: by simp [ennreal.bit0_eq_zero_iff, one_ne_zero] -/
#print ennreal.max_zero_left /- is redundant: by simp [max_eq_right, zero_le] -/

-- data/rat/cast.lean
#print rat.cast_ne_zero /- is redundant: by simp [ne.def, rat.cast_eq_zero] -/

-- data/polynomial.lean
#print polynomial.coeff_C_mul_X /- is redundant: by simp [polynomial.coeff_X_pow, mul_ite, polynomial.coeff_C_mul] -/
#print polynomial.leading_coeff_X /- is redundant: by simp [polynomial.monic_X, polynomial.monic.leading_coeff] -/
#print polynomial.leading_coeff_one /- is redundant: by simp [polynomial.monic.leading_coeff, polynomial.monic_one] -/
#print polynomial.coeff_one_zero /- is redundant: by simp [if_true, polynomial.coeff_one, eq_self_iff_true] -/

-- data/pnat/basic.lean
#print pnat.mk_coe /- is redundant: by simp [subtype.coe_mk] -/

-- data/pequiv.lean
#print pequiv.of_set_eq_some_self_iff /- is redundant: by simp [true_and, pequiv.of_set_eq_some_iff, eq_self_iff_true] -/

-- data/padics/padic_numbers.lean
#print padic_norm_e.mul /- is redundant: by simp [normed_field.norm_mul] -/

-- data/padics/padic_integers.lean
#print padic_int.add_def /- is redundant: by simp [padic_int.val_eq_coe, padic_int.coe_add] -/
#print padic_norm_z.one /- is redundant: by simp [padic_norm_z.norm_one] -/
#print padic_int.mul_def /- is redundant: by simp [padic_int.val_eq_coe, padic_int.coe_mul] -/

-- data/option/basic.lean
#print option.get_mem /- is redundant: by simp [option.some_get, eq_self_iff_true, option.mem_def] -/
#print option.not_mem_none /- is redundant: by simp [option.mem_def] -/

-- data/num/lemmas.lean
#print pos_num.lt_to_nat /- is redundant: by simp [pos_num.cast_lt] -/
#print pos_num.of_to_nat /- is redundant: by simp [pos_num.cast_to_nat, pos_num.cast_to_num] -/
#print num.mul_to_nat /- is redundant: by simp [num.cast_mul] -/
#print znum.le_to_int /- is redundant: by simp [znum.cast_le] -/
#print num.to_of_nat /- is redundant: by simp [nat.cast_id, num.of_nat_cast] -/
#print pos_num.add_to_nat /- is redundant: by simp [pos_num.cast_add] -/
#print znum.to_of_int /- is redundant: by simp [znum.of_int_cast, int.cast_id] -/
#print num.le_to_nat /- is redundant: by simp [num.cast_le] -/
#print num.add_to_nat /- is redundant: by simp [num.cast_add] -/
#print znum.lt_to_int /- is redundant: by simp [znum.cast_lt] -/
#print pos_num.mul_to_nat /- is redundant: by simp [pos_num.cast_mul] -/
#print pos_num.le_to_nat /- is redundant: by simp [pos_num.cast_le] -/
#print num.add_of_nat /- is redundant: by simp [nat.cast_add] -/
#print num.lt_to_nat /- is redundant: by simp [num.cast_lt] -/

-- data/nat/modeq.lean
#print nat.mod_mul_right_mod /- is redundant: by simp [nat.mod_mod_of_dvd, dvd_mul_right] -/
#print nat.mod_mul_left_mod /- is redundant: by simp [nat.mod_mod_of_dvd, dvd_mul_left] -/

-- data/nat/cast.lean
#print nat.cast_one /- is redundant: by simp [nat.cast_zero, nat.cast_succ, zero_add] -/

-- data/nat/basic.lean
#print nat.mod_mod /- is redundant: by simp [nat.mod_mod_of_dvd, dvd_refl] -/

-- data/multiset.lean
#print multiset.sigma_singleton /- is redundant: by simp [add_zero, multiset.map_cons, multiset.zero_sigma, multiset.cons_add, multiset.map_zero, multiset.cons_sigma] -/
#print multiset.singleton_disjoint /- is redundant: by simp [multiset.disjoint_cons_left, and_true, multiset.zero_disjoint] -/
#print multiset.card_singleton /- is redundant: by simp [multiset.card_zero, zero_add, multiset.card_cons] -/
#print multiset.disjoint_cons_left /- is redundant: by simp [multiset.disjoint_cons_right, multiset.disjoint_comm] -/
#print multiset.disjoint_union_left /- is redundant: by simp [multiset.disjoint_union_right, multiset.disjoint_comm] -/
#print multiset.map_id /- is redundant: by simp [id.def, multiset.map_id'] -/
#print multiset.repeat_one /- is redundant: by simp [multiset.repeat_succ, multiset.repeat_zero] -/
#print multiset.ndinsert_zero /- is redundant: by simp [multiset.ndinsert_of_not_mem, not_false_iff, multiset.not_mem_zero] -/
#print multiset.erase_dup_singleton /- is redundant: by simp [multiset.erase_dup_zero, not_false_iff, multiset.erase_dup_cons_of_not_mem, multiset.not_mem_zero] -/
#print multiset.singleton_ne_zero /- is redundant: by simp [multiset.cons_ne_zero] -/
#print multiset.mem_cons_self /- is redundant: by simp [multiset.mem_cons, true_or, eq_self_iff_true] -/
#print multiset.mem_ndinsert_self /- is redundant: by simp [multiset.mem_ndinsert, true_or, eq_self_iff_true] -/
#print multiset.erase_zero /- is redundant: by simp [not_false_iff, multiset.not_mem_zero, multiset.erase_of_not_mem] -/
#print multiset.disjoint_add_left /- is redundant: by simp [multiset.disjoint_add_right, multiset.disjoint_comm] -/
#print multiset.sup_singleton /- is redundant: by simp [multiset.sup_zero, multiset.sup_cons, lattice.sup_bot_eq] -/
#print multiset.product_singleton /- is redundant: by simp [add_zero, multiset.zero_product, multiset.map_cons, multiset.cons_product, multiset.cons_add, multiset.map_zero] -/
#print multiset.count_zero /- is redundant: by simp [not_false_iff, multiset.not_mem_zero, multiset.count_eq_zero_of_not_mem] -/
#print multiset.zero_ndinter /- is redundant: by simp [multiset.zero_inter, multiset.nodup_zero, multiset.ndinter_eq_inter] -/
#print multiset.mem_singleton /- is redundant: by simp [multiset.mem_cons, or_false, multiset.not_mem_zero] -/
#print multiset.disjoint_ndinsert_left /- is redundant: by simp [multiset.disjoint_comm, multiset.disjoint_ndinsert_right] -/
#print multiset.inf_singleton /- is redundant: by simp [multiset.inf_cons, lattice.inf_top_eq, multiset.inf_zero] -/

-- data/matrix/basic.lean
#print matrix.neg_val /- is redundant: by simp [pi.neg_apply] -/
#print matrix.add_val /- is redundant: by simp [pi.add_apply] -/
#print matrix.smul_val /- is redundant: by simp [smul_eq_mul, pi.smul_apply] -/

-- data/list/sort.lean
#print list.ordered_insert_nil /- is redundant: by simp [] -/
#print list.sorted_singleton /- is redundant: by simp [list.not_mem_nil, list.sorted_cons, forall_prop_of_false, list.sorted_nil, not_false_iff, and_self, forall_true_iff] -/

-- data/list/sigma.lean
#print list.kerase_nil /- is redundant: by simp [list.not_mem_nil, list.kerase_of_not_mem_keys, list.keys_nil, not_false_iff] -/

-- data/list/basic.lean
#print list.erase_nil /- is redundant: by simp [list.not_mem_nil, list.erase_of_not_mem, not_false_iff] -/
#print list.count_nil /- is redundant: by simp [list.not_mem_nil, list.count_eq_zero_of_not_mem, not_false_iff] -/
#print list.repeat_succ /- is redundant: by simp [list.repeat] -/
#print list.bind_append /- is redundant: by simp [list.append_bind] -/
#print list.singleton_disjoint /- is redundant: by simp [and_true, list.disjoint_nil_left, list.disjoint_cons_left] -/
#print list.last_cons_cons /- is redundant: by simp [list.last_cons, list.last, ne.def, not_false_iff, list.cons_ne_nil] -/
#print list.disjoint_append_left /- is redundant: by simp [list.disjoint_append_right, list.disjoint_comm] -/
#print list.cons_inj' /- is redundant: by simp [true_and, eq_self_iff_true] -/
#print list.reverse_singleton /- is redundant: by simp [list.reverse_cons, list.nil_append, list.reverse_nil] -/
#print list.insert_nil /- is redundant: by simp [list.not_mem_nil, list.insert_of_not_mem, not_false_iff] -/
#print list.sublists'_singleton /- is redundant: by simp [list.cons_append, list.sublists'_cons, list.nil_append, list.sublists'_nil, list.map] -/
#print list.mem_singleton /- is redundant: by simp [list.not_mem_nil, list.mem_cons_iff, or_false] -/
#print list.disjoint_cons_left /- is redundant: by simp [list.disjoint_cons_right, list.disjoint_comm] -/
#print list.mem_insert_self /- is redundant: by simp [true_or, eq_self_iff_true, list.mem_insert_iff] -/
#print list.index_of_nil /- is redundant: by simp [list.not_mem_nil, list.length, not_false_iff, list.index_of_of_not_mem] -/
#print list.cons_ne_nil /- is redundant: by simp [] -/
#print list.forall_mem_ne /- is redundant: by simp [multiset.forall_mem_ne] -/

-- data/int/modeq.lean
#print int.mod_mul_left_mod /- is redundant: by simp [dvd_mul_left, int.mod_mod_of_dvd] -/
#print int.mod_mul_right_mod /- is redundant: by simp [int.mod_mod_of_dvd, dvd_mul_right] -/

-- data/int/basic.lean
#print int.coe_nat_ne_zero /- is redundant: by simp [int.coe_nat_eq_zero, ne.def] -/
#print int.of_nat_div /- is redundant: by simp [int.coe_nat_div, int.of_nat_eq_coe] -/
#print int.mod_self /- is redundant: by simp [euclidean_domain.mod_self] -/
#print int.zero_mod /- is redundant: by simp [euclidean_domain.zero_mod] -/
#print int.div_zero /- is redundant: by simp [euclidean_domain.div_zero] -/
#print int.mod_mod /- is redundant: by simp [int.mod_mod_of_dvd, dvd_refl] -/
#print int.mod_zero /- is redundant: by simp [euclidean_domain.mod_zero] -/
#print int.cast_ne_zero /- is redundant: by simp [int.cast_eq_zero, ne.def] -/
#print int.zero_div /- is redundant: by simp [euclidean_domain.zero_div] -/
#print int.mod_one /- is redundant: by simp [euclidean_domain.mod_one] -/

-- data/fintype.lean
#print fintype.card_unit /- is redundant: by simp [fintype.card_punit] -/
#print fintype.card_punit /- is redundant: by simp [fintype.card_of_subsingleton] -/
#print fintype.univ_unit /- is redundant: by simp [fintype.univ_punit, finset.insert_empty_eq_singleton] -/
#print fintype.card_coe /- is redundant: by simp [iff_self, finset.mem_coe, fintype.card_of_finset, forall_true_iff] -/

-- data/finsupp.lean
#print finsupp.smul_apply /- is redundant: by simp [finsupp.smul_apply', smul_eq_mul] -/

-- data/finset.lean
#print finset.inter_assoc /- is redundant: by simp [finset.inter_comm, finset.inter_left_comm] -/
#print finset.union_idempotent /- is redundant: by simp [finset.union_self] -/
#print finset.mem_powerset_self /- is redundant: by simp [finset.mem_powerset, finset.subset.refl] -/
#print finset.insert_singleton_self_eq' /- is redundant: by simp [finset.insert_eq_of_mem, eq_self_iff_true, finset.mem_singleton] -/
#print finset.inter_right_comm /- is redundant: by simp [finset.inter_assoc, finset.inter_comm] -/
#print finset.empty_mem_powerset /- is redundant: by simp [finset.empty_subset, finset.mem_powerset] -/
#print finset.empty_union /- is redundant: by simp [finset.union_comm, finset.union_empty] -/
#print finset.insert_idem /- is redundant: by simp [finset.insert_eq_of_mem, true_or, eq_self_iff_true, finset.mem_insert] -/
#print finset.piecewise_insert_self /- is redundant: by simp [true_or, eq_self_iff_true, finset.piecewise_eq_of_mem, finset.mem_insert] -/
#print finset.insert_union /- is redundant: by simp [finset.union_comm, finset.union_insert] -/
#print finset.empty_inter /- is redundant: by simp [finset.inter_empty, finset.inter_comm] -/
#print finset.sdiff_inter_self /- is redundant: by simp [finset.inter_sdiff_self, finset.inter_comm] -/
#print finset.sdiff_union_self_eq_union /- is redundant: by simp [finset.union_comm, finset.union_sdiff_self_eq_union] -/
#print finset.singleton_eq_singleton /- is redundant: by simp [finset.insert_empty_eq_singleton] -/

-- data/fin.lean
#print fin.mk_val /- is redundant: by simp [] -/

-- data/equiv/local_equiv.lean
#print local_equiv.refl_restr_source /- is redundant: by simp [set.univ_inter, local_equiv.refl_source, local_equiv.restr_source] -/
#print local_equiv.trans_inv_apply /- is redundant: by simp [function.comp_app, local_equiv.trans_inv_fun] -/
#print local_equiv.trans_apply /- is redundant: by simp [function.comp_app, local_equiv.trans_to_fun] -/
#print local_equiv.refl_restr_target /- is redundant: by simp [local_equiv.restr_target, set.preimage_id, set.univ_inter, local_equiv.refl_inv_fun, local_equiv.refl_target] -/

-- data/equiv/encodable.lean
#print encodable.decode_nat /- is redundant: by simp [denumerable.of_nat_nat, denumerable.decode_eq_of_nat] -/

-- data/equiv/basic.lean
#print equiv.swap_apply_self /- is redundant: by simp [equiv.perm.swap_swap_apply] -/
#print equiv.swap_mul_self /- is redundant: by simp [equiv.perm.swap_mul_self] -/

-- data/equiv/algebra.lean
#print equiv.coe_units_equiv_ne_zero /- timeout -/

-- data/dfinsupp.lean
#print dfinsupp.single_eq_same /- is redundant: by simp [dif_pos, dfinsupp.single_apply, eq_self_iff_true] -/
#print dfinsupp.erase_same /- is redundant: by simp [if_true, eq_self_iff_true, dfinsupp.erase_apply] -/
#print dfinsupp.mem_support_to_fun /- is redundant: by simp [dfinsupp.mem_support_iff, ne.def] -/

-- data/complex/basic.lean
#print complex.of_real_ne_zero /- is redundant: by simp [ne.def, complex.of_real_eq_zero] -/
#print complex.abs_of_nat /- is redundant: by simp [complex.abs_cast_nat] -/

-- data/bool.lean
#print bool.coe_to_bool /- is redundant: by simp [bool.of_to_bool_iff] -/

-- category_theory/types.lean
#print category_theory.functor_to_types.hcomp /- is redundant: by simp [category_theory.types_comp, category_theory.nat_trans.hcomp_app, function.comp_app] -/
#print category_theory.functor_to_types.map_id /- is redundant: by simp [id.def, category_theory.types_id, category_theory.functor.map_id] -/
#print category_theory.functor_to_types.map_comp /- is redundant: by simp [category_theory.types_comp, function.comp_app, category_theory.functor.map_comp] -/
#print category_theory.functor_to_types.comp /- is redundant: by simp [category_theory.types_comp, category_theory.nat_trans.comp_app, function.comp_app] -/

-- category_theory/natural_isomorphism.lean
#print category_theory.nat_iso.hom_inv_id_app /- is redundant: by simp [category_theory.nat_iso.hom_app_inv_app_id] -/
#print category_theory.nat_iso.app_hom /- is redundant: by simp [] -/
#print category_theory.nat_iso.app_inv /- is redundant: by simp [] -/
#print category_theory.nat_iso.inv_hom_id_app /- is redundant: by simp [category_theory.nat_iso.inv_app_hom_app_id] -/

-- category_theory/monoidal/category.lean
#print category_theory.monoidal_category.triangle /- is redundant: by simp [category_theory.monoidal_category.triangle_assoc_comp_left] -/

-- category_theory/functor_category.lean
#print category_theory.nat_trans.vcomp_app' /- is redundant: by simp [category_theory.nat_trans.comp_app] -/

-- category_theory/comma.lean
#print category_theory.over.comp_left /- is redundant: by simp [category_theory.comma.comp_left] -/
#print category_theory.under.comp_right /- is redundant: by simp [category_theory.comma.comp_right] -/

-- category_theory/adjunction/basic.lean
#print category_theory.adjunction.hom_equiv_naturality_right /- is redundant: by simp [category_theory.category.assoc, category_theory.functor.map_comp, category_theory.adjunction.hom_equiv_unit] -/
#print category_theory.adjunction.hom_equiv_naturality_right_symm /- is redundant: by simp [category_theory.adjunction.counit_naturality, category_theory.category.assoc, category_theory.adjunction.hom_equiv_naturality_left_symm, category_theory.adjunction.hom_equiv_counit] -/
#print category_theory.adjunction.hom_equiv_naturality_left /- is redundant: by simp [category_theory.adjunction.hom_equiv_naturality_right, category_theory.adjunction.unit_naturality, category_theory.category.assoc, category_theory.adjunction.hom_equiv_unit] -/
#print category_theory.adjunction.hom_equiv_naturality_left_symm /- is redundant: by simp [category_theory.category.assoc, category_theory.functor.map_comp, category_theory.adjunction.hom_equiv_counit] -/

-- analysis/normed_space/operator_norm.lean
#print continuous_linear_map.norm_zero /- is redundant: by simp [norm_zero] -/

-- analysis/normed_space/multilinear.lean
#print continuous_multilinear_map.norm_zero /- is redundant: by simp [norm_zero] -/

-- analysis/complex/basic.lean
#print complex.norm_nat /- is redundant: by simp [complex.abs_cast_nat, complex.norm_eq_abs] -/

-- algebra/ring.lean
#print units.coe_mul_dvd /- is redundant: by simp [mul_unit_dvd_iff] -/
#print units.dvd_coe_mul /- is redundant: by simp [dvd_mul_unit_iff] -/
#print units.neg_mul_neg /- is redundant: by simp [units.neg_neg, units.mul_neg, units.neg_mul] -/
#print ring_hom.comp_apply /- is redundant: by simp [function.comp_app, ring_hom.coe_comp] -/

-- algebra/punit_instances.lean
#print punit.smul_eq /- is redundant: by simp [punit.mul_eq, algebra.id.smul_eq_mul] -/

-- algebra/ordered_ring.lean
#print with_top.top_mul_top /- is redundant: by simp [with_top.top_mul, ne.def, not_false_iff, with_top.top_ne_zero] -/

-- algebra/group/units_hom.lean
#print units.coe_map' /- is redundant: by simp [units.coe_map, monoid_hom.coe_of] -/

-- algebra/group/hom.lean
#print add_monoid_hom.map_add_neg /- is redundant: by simp [add_monoid_hom.map_add, add_monoid_hom.map_neg] -/
#print monoid_hom.map_mul_inv /- is redundant: by simp [monoid_hom.map_mul, monoid_hom.map_inv] -/

-- algebra/group/basic.lean
#print mul_self_iff_eq_one /- is redundant: by simp [mul_right_eq_self] -/
#print add_self_iff_eq_zero /- is redundant: by simp [add_right_eq_self] -/
#print inv_ne_one /- is redundant: by simp [inv_eq_one, ne.def] -/
#print neg_ne_zero /- is redundant: by simp [ne.def, neg_eq_zero] -/

-- algebra/free.lean
#print free_semigroup.pure_bind /- is redundant: by simp [is_lawful_monad.pure_bind] -/
#print free_semigroup.map_pure /- is redundant: by simp [is_lawful_applicative.map_pure] -/
#print free_magma.map_pure /- is redundant: by simp [is_lawful_applicative.map_pure] -/
#print free_magma.pure_bind /- is redundant: by simp [is_lawful_monad.pure_bind] -/
#print free_semigroup.lift_of_mul /- is redundant: by simp [free_semigroup.lift_mul, free_semigroup.lift_of] -/

-- algebra/floor.lean
#print fract_floor /- is redundant: by simp [fract_coe] -/

-- algebra/direct_limit.lean
#print ring.direct_limit.lift_neg /- timeout -/

-- algebra/continued_fractions/basic.lean
#print continued_fraction.coe_to_generalized_continued_fraction /- is redundant: by simp [simple_continued_fraction.coe_to_generalized_continued_fraction, continued_fraction.coe_to_simple_continued_fraction, coe_coe] -/

-- algebra/commute.lean
#print commute.self_gsmul /- is redundant: by simp [commute.refl, commute.gsmul_right] -/
#print commute.gpow_gpow_self /- is redundant: by simp [commute.gpow_gpow, commute.refl] -/
#print commute.self_smul_smul /- is redundant: by simp [commute.smul_smul, commute.refl] -/
#print commute.self_pow /- is redundant: by simp [commute.refl, commute.pow_right] -/
#print commute.smul_self /- is redundant: by simp [commute.smul_left, commute.refl] -/
#print commute.self_gsmul_gsmul /- is redundant: by simp [commute.gsmul_gsmul, commute.refl] -/
#print commute.gsmul_self /- is redundant: by simp [commute.refl, commute.gsmul_left] -/
#print commute.pow_self /- is redundant: by simp [commute.refl, commute.pow_left] -/
#print commute.inv_inv_iff /- is redundant: by simp [commute.inv_right_iff, commute.inv_left_iff] -/
#print commute.gpow_self /- is redundant: by simp [commute.refl, commute.gpow_left] -/
#print commute.self_smul /- is redundant: by simp [commute.refl, commute.smul_right] -/
#print commute.pow_pow_self /- is redundant: by simp [commute.refl, commute.pow_pow] -/
#print commute.self_gpow /- is redundant: by simp [commute.gpow_right, commute.refl] -/

-- algebra/char_zero.lean
#print nat.cast_ne_zero /- is redundant: by simp [ne.def, nat.cast_eq_zero] -/

-- algebra/category/Module/basic.lean
#print Module.id_apply /- is redundant: by simp [category_theory.coe_id] -/

-- algebra/category/Group.lean
#print mul_equiv.to_CommGroup_iso_hom /- is redundant: by simp [mul_equiv.to_CommGroup_iso_hom_2] -/
#print mul_equiv.to_CommGroup_iso_inv /- is redundant: by simp [mul_equiv.to_CommGroup_iso_inv_2] -/

-- algebra/big_operators.lean
#print finset.prod_const_one /- is redundant: by simp [one_pow, finset.prod_const] -/
#print finset.sum_const_zero /- is redundant: by simp [add_monoid.smul_zero, finset.sum_const] -/

-- algebra/associated.lean
#print not_is_unit_zero /- is redundant: by simp [is_unit_zero_iff, zero_ne_one] -/