unused arguments

unused.lean

-- this Git is supposed to be used on branch sanity_check
-- You have to run the script "scripts/mk_all.sh", and then this file should compile.
-- The list after each declaration gives all the positions of the unused arguments (starting at 1). E.g. [2] means that the second argument is unused.
import all

#sanity_check_mathlib

-- topology\uniform_space\uniform_embedding.lean
#print uniformly_extend_exists -- [7]

-- topology\uniform_space\separation.lean
#print uniform_space.uniform_continuous_quotient_lift₂ -- [6]

-- topology\uniform_space\completion.lean
#print Cauchy.extend -- [5, 6]
#print uniform_space.completion.extension -- [5, 6]

-- topology\uniform_space\cauchy.lean
#print totally_bounded_subset -- [2]
#print cauchy_seq -- [4]
#print totally_bounded_image -- [3]
#print cauchy_iff_exists_le_nhds -- [2]
#print totally_bounded_closure -- [2]
#print totally_bounded_empty -- [2]
#print cauchy_map_iff_exists_tendsto -- [3]

-- topology\uniform_space\basic.lean
#print sum.uniformity -- [3, 4]
#print to_topological_space_prod -- [3, 4]
#print mem_uniformity_is_closed -- [2]
#print sum.uniform_space -- [3, 4]

-- topology\subset_properties.lean
#print compact_of_closed -- [2]
#print compact_univ -- [2]

-- topology\stone_cech.lean
#print ultrafilter.extend -- [4]
#print stone_cech_extend_extends -- [6, 8]

-- topology\separation.lean
#print prod.t2_space -- [3]
#print Pi.t2_space -- [2]
#print t2_space_discrete -- [2]
#print subtype.t2_space -- [2]

-- topology\order.lean
#print principal_subtype -- [2]
#print induced_compose -- [4]
#print continuous_within_at_iff_ptendsto_res -- [8]
#print map_nhds_induced_of_surjective -- [7]

-- topology\metric_space\gluing.lean
#print metric.glue_dist -- [4]

-- topology\metric_space\emetric_space.lean
#print subtype.emetric_space -- [2]
#print subtype.edist_eq -- [2]

-- topology\metric_space\cau_seq_filter.lean
#print sequentially_complete.B2 -- [2]

-- topology\metric_space\basic.lean
#print second_countable_of_proper -- [2]
#print locally_compact_of_proper -- [2]
#print proper_of_compact -- [2]
#print subtype.dist_eq -- [2]
#print subtype.metric_space -- [2]

-- topology\maps.lean
#print dense_range -- [3]
#print dense_range_iff_closure_eq -- [3]
#print dense_inducing.mk' -- [3, 4]
#print inducing.map_nhds_eq -- [3, 4]
#print inducing.nhds_eq_comap -- [3, 4]
#print embedding.map_nhds_eq -- [3, 4]

-- topology\constructions.lean
#print diagonal_eq_range_diagonal_map -- [2]
#print is_closed_property -- [3]
#print locally_compact_of_compact -- [2]
#print quotient.compact_space -- [2]
#print list.tendsto_cons -- [3]
#print sum.compact_space -- [3, 4]
#print list.continuous_at_length -- [2]
#print quot.compact_space -- [2]
#print prod_generate_from_generate_from_eq -- [3, 4]
#print continuous_at_subtype_val -- [2]
#print is_closed_eq -- [3, 4]
#print is_closed_diagonal -- [2]
#print mem_closure2 -- [4, 5, 6]
#print is_closed_prod -- [3, 4]
#print prod_eq_generate_from -- [3, 4]
#print prod.discrete_topology -- [3, 4]
#print list.tendsto_insert_nth -- [4]
#print normal_of_compact_t2 -- [2]
#print dense_embedding.subtype_emb -- [7]
#print is_open_map.prod -- [5, 6, 7]
#print locally_compact_of_compact_nhds -- [2]
#print tendsto_subtype_rng -- [3, 4]
#print list.tendsto_cons_iff -- [4, 5]
#print list.tendsto_nhds -- [4]

-- topology\basic.lean
#print mem_closure -- [3, 4]
#print lim_spec -- [3]
#print tendsto_pure_nhds -- [3]

-- topology\bases.lean
#print topological_space.subtype.second_countable_topology -- [2]

-- topology\algebra\uniform_ring.lean
#print uniform_space.completion.coe_one -- [4, 5]
#print uniform_space.completion.has_one -- [4, 5]
#print uniform_space.completion.coe_mul -- [4]
#print uniform_space.completion.has_mul -- [4, 5]

-- topology\algebra\uniform_group.lean
#print is_Z_bilin.tendsto_zero_left -- [5, 8, 12, 13, 14]
#print tendsto_sub_comap_self -- [8]
#print is_Z_bilin.tendsto_zero_right -- [5, 8, 12, 13, 14]

-- topology\algebra\ring.lean
#print quotient_ring_saturate -- [4]
#print topological_ring_quotient_topology -- [4]

-- topology\algebra\ordered.lean
#print neg_preimage_closure -- [4]
#print tendsto_min -- [6]
#print tendsto_max -- [6]
#print lt_mem_sets_of_Limsup_lt -- [4]

-- topology\algebra\open_subgroup.lean
#print open_add_subgroup -- [4]
#print open_subgroup -- [4]

-- topology\algebra\monoid.lean
#print is_submonoid.mem_nhds_one -- [4]
#print is_add_submonoid.mem_nhds_zero -- [4]

-- topology\algebra\module.lean
#print continuous_linear_map.scalar_prod_space_iso -- [10]
#print continuous_linear_map.map_neg -- [3]
#print continuous_linear_map.continuous -- [3]
#print continuous_linear_map.id -- [3]
#print continuous_linear_map.coe_neg -- [13]
#print continuous_linear_map.coe_sub -- [14]
#print continuous_linear_map.coe_add' -- [14]
#print continuous_linear_map.prod -- [3]
#print continuous_linear_map.to_fun -- [3]
#print continuous_linear_map.coe_neg' -- [13]
#print continuous_linear_map.coe_sub' -- [14]
#print continuous_linear_map.map_add -- [3]
#print continuous_linear_map.has_scalar -- [10]
#print continuous_linear_map.coe_add -- [14]
#print continuous_linear_map.coe_apply' -- [10, 13]
#print continuous_linear_map.map_sub -- [3]
#print continuous_linear_map.has_coe -- [3]
#print topological_vector_space.mk.inj -- [10]
#print continuous_linear_map.comp -- [3]
#print continuous_linear_map.coe_apply -- [10, 13]
#print continuous_linear_map.zero -- [3]
#print continuous_linear_map.map_zero -- [3]
#print continuous_linear_map.map_smul -- [3]

-- topology\algebra\infinite_sum.lean
#print summable_iff_cauchy -- [6]
#print has_sum_unique -- [5]
#print has_sum -- [5]
#print has_sum_hom -- [12]
#print has_sum_sum_of_ne_finset_zero -- [5]

-- topology\algebra\group_completion.lean
#print uniform_space.completion.is_add_group_hom_prod -- [8]
#print uniform_space.completion.is_add_group_hom_map -- [8]

-- topology\algebra\group.lean
#print quotient_group.quotient.topological_space -- [4]
#print quotient_add_group_saturate -- [4]
#print quotient_group_saturate -- [4]
#print quotient_add_group.quotient.topological_space -- [4]

-- topology\Top\presheaf.lean
#print Top.presheaf.pushforward_eq_eq -- [8]

-- tactic\where.lean
#print where.where_cmd -- [1, 2]

-- tactic\tfae.lean
#print tactic.tfae.arrow.left.inj -- [1]
#print tactic.interactive.tfae_have -- [5]
#print tactic.tfae.arrow.right.inj -- [1]
#print tactic.tfae.arrow.left_right.inj -- [1]

-- tactic\sanity_check.lean
#print sanity_check_mathlib_cmd -- [1]
#print sanity_check_cmd -- [1]

-- tactic\ring2.lean
#print tactic.ring2.horner_expr.inv -- [1]
#print tactic.ring2.tree.nil.inj -- [2]

-- tactic\ring.lean
#print tactic.ring.normalize_mode.SOP.inj -- [1]
#print tactic.ring.normalize_mode.raw.inj -- [1]
#print tactic.ring.pow_add_rev -- [4]
#print tactic.ring.normalize_mode.horner.inj -- [1]

-- tactic\rewrite_all\congr.lean
#print tactic.rewrite_all.congr.expr_lens.entire.inj -- [1]

-- tactic\rewrite_all\basic.lean
#print side.R.inj -- [1]
#print side.L.inj -- [1]

-- tactic\restate_axiom.lean
#print restate_axiom_cmd -- [1, 2]

-- tactic\replacer.lean
#print tactic.def_replacer_cmd -- [1, 2]

-- tactic\rcases.lean
#print tactic.rcases_patt_inverted.below -- [1]
#print tactic.rcases_patt.below -- [1]
#print tactic.rcases_patt_inverted.ibelow -- [1]
#print tactic.rcases_patt.ibelow -- [1]

-- tactic\omega\eq_elim.lean
#print omega.ee.neg.inj -- [1]
#print omega.ee.drop.inj -- [1]

-- tactic\norm_num.lean
#print norm_num.prove_lt -- [1]

-- tactic\monotonicity\interactive.lean
#print tactic.interactive.rep_arity.one.inj -- [1]
#print tactic.interactive.rep_arity.many.inj -- [1]
#print tactic.interactive.mono_aux -- [2]
#print tactic.interactive.match_ac -- [2]

-- tactic\monotonicity\basic.lean
#print tactic.interactive.mono_selection.left.inj -- [1]
#print tactic.interactive.monotoncity.check -- [2, 3]
#print tactic.interactive.mono_selection.both.inj -- [1]
#print tactic.interactive.mono_selection.right.inj -- [1]
#print tactic.interactive.monotoncity.check_rel -- [1]

-- tactic\localized.lean
#print localized_cmd -- [1, 2]
#print open_locale_cmd -- [1, 2]

-- tactic\local_cache.lean
#print tactic.local_cache.internal.save_data -- [3]
#print tactic.local_cache.internal.load_data -- [3]

-- tactic\linarith.lean
#print linarith.ineq.eq.inj -- [1]
#print linarith.ineq.lt.inj -- [1]
#print linarith.mul_eq -- [6]
#print linarith.ineq.le.inj -- [1]
#print linarith.tree.nil.inj -- [2]

-- tactic\library_search.lean
#print tactic.library_search.head_symbol_match.ex.inj -- [1]
#print tactic.library_search.head_symbol_match.both.inj -- [1]
#print tactic.library_search.head_symbol_match.mp.inj -- [1]
#print tactic.library_search.head_symbol_match.mpr.inj -- [1]

-- tactic\interactive.lean
#print tactic.interactive.generalize_hyp -- [2]
#print tactic.interactive.set -- [4]
#print tactic.interactive.h_generalize -- [3]

-- tactic\finish.lean
#print auto.case_option.force.inj -- [1]
#print auto.case_option.accept.inj -- [1]
#print auto.case_option.at_most_one.inj -- [1]

-- tactic\find.lean
#print find_cmd -- [1]

-- tactic\explode.lean
#print tactic.explode.status.intro.inj -- [1]
#print tactic.explode.status.sintro.inj -- [1]
#print tactic.explode.status.reg.inj -- [1]
#print tactic.explode.status.lam.inj -- [1]
#print tactic.explode_cmd -- [1]

-- tactic\doc_blame.lean
#print print_item -- [2]
#print doc_cmd -- [1, 2]

-- tactic\core.lean
#print tactic.symmetry_hyp -- [2]
#print tactic.trace_macro -- [1]
#print tactic.trace_error -- [3]
#print tactic.pformat_macro -- [1]
#print tactic.setup_tactic_parser_cmd -- [1]
#print tactic.fail_macro -- [1]

-- tactic\converter\interactive.lean
#print old_conv.istep -- [3]

-- tactic\converter\binders.lean
#print binder_eq_elim.check_eq -- [1]

-- tactic\chain.lean
#print tactic.trace_output -- [2]

-- tactic\alias.lean
#print tactic.alias.alias_cmd -- [2]

-- tactic\abel.lean
#print tactic.abel.normalize_mode.term.inj -- [1]
#print tactic.abel.normalize_mode.raw.inj -- [1]

-- set_theory\zfc.lean
#print Set.map_definable_aux -- [2]
#print pSet.definable.mk.inj -- [3]

-- set_theory\surreal.lean
#print pSurreal.inv_ty.zero.inj -- [3]

-- set_theory\ordinal_notation.lean
#print onote.oadd_lt_oadd_2 -- [7]
#print onote.oadd_lt_oadd_1 -- [8]
#print onote.zero.inj -- [1]
#print onote.oadd_lt_oadd_3 -- [5, 6]

-- set_theory\ordinal.lean
#print principal_seg.of_element -- [3]
#print principal_seg.lt_le -- [7]
#print principal_seg.lt_le_apply -- [7, 8]
#print principal_seg.equiv_lt_apply -- [7, 8]
#print principal_seg.lt_le_top -- [8]
#print ordinal.type_def' -- [3]
#print principal_seg.lt_equiv -- [7, 8]
#print principal_seg.equiv_lt -- [7, 8]
#print ordinal.card_typein -- [3]

-- set_theory\lists.lean
#print lists'.nil.inj -- [2]

-- ring_theory\unique_factorization_domain.lean
#print associates.factor_set -- [3]
#print associates.unique' -- [4]
#print associates.factor_set.coe_add -- [3, 4]
#print unique_factorization_domain.exists_mem_factors_of_dvd -- [4]
#print associates.factors' -- [4]
#print associates.factor_set.prod -- [4]

-- ring_theory\power_series.lean
#print mv_power_series.map_comp -- [7]
#print mv_power_series.zero -- [3]
#print power_series.map_comp -- [5]
#print mv_power_series.coeff -- [3]
#print mv_power_series.map -- [4, 6]

-- ring_theory\polynomial.lean
#print polynomial.of_subring -- [3]

-- ring_theory\multiplicity.lean
#print multiplicity.finite_mul_aux -- [3]
#print multiplicity.finite_iff_dom -- [3]

-- ring_theory\localization.lean
#print localization.r -- [4]
#print localization.fraction_ring.eq_zero_of_ne_zero_of_mul_eq_zero -- [3]

-- ring_theory\integral_closure.lean
#print is_integral -- [6]
#print is_integral_algebra_map -- [6]

-- ring_theory\ideals.lean
#print ideal.is_coprime_def -- [2]
#print ideal.mem_span_pair -- [2]
#print ideal.is_coprime_self -- [2, 5]

-- ring_theory\ideal_operations.lean
#print ideal.comap_mono -- [6]
#print ideal.map_mono -- [6]
#print ideal.mem_map_of_mem -- [6]
#print ideal.map -- [6]

-- ring_theory\algebra.lean
#print algebra.comap.module -- [7]
#print algebra.comap -- [7, 8]
#print mv_polynomial.eval_unique -- [7]
#print algebra.comap.ring -- [7, 8]
#print algebra.comap.has_scalar -- [7]
#print algebra.comap.comm_ring -- [7, 8]
#print algebra.comap.to_comap -- [7, 8]

-- ring_theory\adjoin_root.lean
#print adjoin_root.lift_is_field_hom -- [5]
#print adjoin_root.is_field_hom -- [4]

-- ring_theory\adjoin.lean
#print algebra.adjoin_singleton_eq_range -- [7]

-- order\liminf_limsup.lean
#print filter.liminf_le_liminf -- [3]
#print filter.limsup_le_limsup -- [3]

-- order\filter\filter_product.lean
#print filter.filter_product.of_seq_zero -- [5]
#print filter.filter_product.of_seq_one -- [5]
#print filter.filter_product.of_div -- [5]
#print filter.filter_product.abs_def -- [7]

-- order\filter\basic.lean
#print filter.mem_bot_sets -- [2]

-- order\conditionally_complete_lattice.lean
#print lattice.cInf_interval -- [2]
#print lattice.cSup_interval -- [2]
#print lattice.cSup_empty -- [2]

-- order\complete_lattice.lean
#print lattice.insert_of_has_insert -- [2]

-- order\bounded_lattice.lean
#print with_top.top_ne_coe -- [2]
#print with_top.coe_ne_top -- [2]

-- order\basic.lean
#print dense_or_discrete -- [5]
#print comp_le_comp_left_of_monotone -- [6]

-- number_theory\pell.lean
#print pell.x_sub_y_dvd_pow_lem -- [2]
#print pell.az -- [2]
#print pell.eq_of_xn_modeq_lem1 -- [5]

-- number_theory\dioph.lean
#print fin2.fz.inj -- [2]
#print fin2.is_lt.mk.inj -- [5]

-- meta\rb_map.lean
#print native.rb_map.find_def -- [4]

-- meta\coinductive_predicates.lean
#print tactic.coinductive_predicate -- [2]

-- measure_theory\measure_space.lean
#print measure_theory.measure' -- [4]
#print measure_theory.to_measure_apply -- [4]

-- measure_theory\measurable_space.lean
#print is_measurable_range_inl -- [3, 4]
#print measurable_space.is_measurable_top -- [2]
#print is_measurable_inl_image -- [3, 4]
#print is_measurable_inr_image -- [3, 4]
#print is_measurable_range_inr -- [3, 4]

-- measure_theory\l1_space.lean
#print measure_theory.lintegral_nnnorm_add -- [5]
#print measure_theory.lintegral_nnnorm_neg -- [5, 7]
#print measure_theory.integrable -- [5]
#print measure_theory.lintegral_nnnorm_zero -- [5]

-- measure_theory\integration.lean
#print measure_theory.limsup_lintegral_le -- [6]
#print measure_theory.dominated_convergence_nn -- [7]
#print measure_theory.simple_func.integral_map -- [8]
#print measure_theory.simple_func.approx -- [4]
#print measure_theory.simple_func.monotone_approx -- [4]
#print measure_theory.simple_func.has_scalar -- [5]
#print measure_theory.simple_func.ennreal_rat_embed_encode -- [2]

-- measure_theory\borel_space.lean
#print measure_theory.is_measurable_Iio -- [2]
#print measure_theory.is_measurable_Ico -- [2]
#print measure_theory.borel_eq_subtype -- [2]
#print measure_theory.is_measurable_Ioo -- [2]
#print measure_theory.measurable.supr_Prop -- [4, 5]
#print measure_theory.borel_induced -- [3]
#print measure_theory.measurable.infi_Prop -- [4, 5]
#print measure_theory.measurable_smul -- [6, 9]
#print measure_theory.measurable_of_continuous2 -- [5]

-- measure_theory\bochner_integration.lean
#print measure_theory.l1.simple_func.to_simple_func -- [6]

-- measure_theory\ae_eq_fun.lean
#print measure_theory.ae_eq_fun.preorder -- [4]
#print measure_theory.ae_eq_fun.partial_order -- [4]
#print measure_theory.ae_eq_fun.edist_eq_add_add -- [6]
#print measure_theory.ae_eq_fun.neg -- [5]
#print measure_theory.ae_eq_fun.mk_le_mk -- [4]
#print measure_theory.ae_eq_fun.edist_mk_mk' -- [5, 8, 9]

-- logic\basic.lean
#print imp_intro -- [4]
#print not_iff -- [3]
#print ball_of_forall -- [6]
#print pempty.no_confusion_type -- [1, 3]

-- linear_algebra\finsupp.lean
#print finsupp.lsum -- [5]
#print finsupp.single_mem_supported -- [8]
#print finsupp.total_comap_domain -- [10]
#print finsupp.supported_eq_span_single -- [5, 8, 10]
#print finsupp.supported_comap_lmap_domain -- [8]

-- linear_algebra\finite_dimensional.lean
#print finite_dimensional.of_fg -- [6]

-- linear_algebra\dual.lean
#print is_basis.coord_fun -- [8]

-- linear_algebra\direct_sum_module.lean
#print direct_sum.component.of -- [7]
#print direct_sum.apply_eq_component -- [7]
#print direct_sum.single_eq_lof -- [7]
#print direct_sum.module -- [4]

-- linear_algebra\dimension.lean
#print dim_quotient -- [7]

-- linear_algebra\basis.lean
#print mem_span_insert_exchange -- [3, 4]
#print disjoint_span_singleton -- [4]
#print constr_smul -- [7, 12, 18]
#print is_basis.ext -- [9]

-- linear_algebra\basic.lean
#print linear_map.sum_apply -- [11, 12]
#print submodule.mem_top -- [5, 6]
#print submodule.mem_bot -- [5]

-- group_theory\subgroup.lean
#print is_group_hom.mem_ker -- [6]
#print is_add_subgroup.mem_trivial -- [2]
#print is_subgroup.is_subgroup -- [4]
#print is_add_group_hom.mem_ker -- [6]
#print is_group_hom.ker -- [6]
#print is_add_group_hom.ker -- [6]
#print is_subgroup.mem_trivial -- [2]

-- group_theory\presented_group.lean
#print presented_group.to_group.of -- [6]

-- group_theory\perm\sign.lean
#print equiv.perm.sign_cycle -- [3]
#print equiv.perm.is_cycle_swap -- [3]
#print equiv.perm.eq_swap_of_is_cycle_of_apply_apply_eq_self -- [3]
#print equiv.perm.card_support_swap -- [3]
#print equiv.perm.is_cycle_swap_mul_aux₁ -- [3]
#print equiv.perm.support_swap -- [3]

-- group_theory\order_of_element.lean
#print card_subgroup_dvd_card -- [4]
#print card_trivial -- [3, 4]
#print quotient_group.fintype -- [4]

-- group_theory\eckmann_hilton.lean
#print eckmann_hilton.comm_group -- [7]

-- group_theory\coset.lean
#print quotient_group.eq_class_eq_left_coset -- [2]
#print quotient_group.inhabited -- [2]
#print normal_of_eq_cosets -- [4]
#print normal_of_eq_add_cosets -- [4]
#print quotient_add_group.eq_class_eq_left_coset -- [2]
#print quotient_add_group.inhabited -- [2]

-- group_theory\abelianization.lean
#print abelianization.lift.unique -- [8]

-- field_theory\splitting_field.lean
#print polynomial.splits_zero -- [6]
#print polynomial.splits -- [6]

-- field_theory\perfect_closure.lean
#print perfect_closure.has_inv -- [4, 5]
#print perfect_closure.eq_iff' -- [4, 5]

-- field_theory\mv_polynomial.lean
#print mv_polynomial.R -- [4]
#print mv_polynomial.decidable_restrict_degree -- [2]
#print mv_polynomial.evalₗ -- [4, 5]

-- field_theory\finite.lean
#print subgroup_units_cyclic -- [3]

-- data\zmod\quadratic_reciprocity.lean
#print quadratic_reciprocity_aux.card_range_p_mul_q_filter_not_coprime -- [4, 7]
#print quadratic_reciprocity_aux.prod_range_div_two_erase_zero -- [4, 6, 7]
#print quadratic_reciprocity_aux.filter_range_p_mul_q_div_two_eq -- [7]

-- data\vector2.lean
#print vector.traverse_def -- [4]

-- data\set\function.lean
#print set.maps_to_univ -- [3]
#print set.right_inv_on_of_eq_on_left -- [6]

-- data\set\finite.lean
#print set.not_injective_nat_fintype -- [3]
#print set.fintype_of_fintype_image -- [3]
#print finset.coe_to_finset' -- [2]

-- data\set\basic.lean
#print set.mem_univ -- [2]

-- data\seq\wseq.lean
#print wseq.think_congr -- [4]

-- data\seq\computation.lean
#print computation.map_congr -- [3, 4]

-- data\semiquot.lean
#print semiquot.mem_univ -- [2]

-- data\real\cau_seq_completion.lean
#print cau_seq.is_complete.mk.inj -- [9]

-- data\real\cau_seq.lean
#print cau_seq.lim_zero -- [6]

-- data\prod.lean
#print prod.lex.decidable -- [4]

-- data\polynomial.lean
#print polynomial.has_zero -- [3]
#print polynomial.polynomial.has_coe_to_fun -- [3]
#print polynomial.pow_sub_pow_factor -- [3]
#print polynomial.eval₂_zero -- [4, 8]
#print polynomial.coeff_sum -- [4]
#print polynomial.eval₂ -- [4]
#print polynomial.coeff -- [3]
#print polynomial.degree -- [3]
#print polynomial.coeff_one_zero -- [4]

-- data\pnat\basic.lean
#print pnat.div_exact -- [3]

-- data\pfun.lean
#print roption.none_decidable -- [1]
#print roption.some_decidable -- [2]
#print pfun.pure_defined -- [4]

-- data\pequiv.lean
#print pequiv.trans_single_of_eq_none -- [4]
#print pequiv.mem_single -- [4]
#print pequiv.single_apply_of_ne -- [4]
#print pequiv.single_apply -- [4]

-- data\padics\padic_numbers.lean
#print padic_seq -- [2]

-- data\padics\padic_norm.lean
#print padic_norm.neg -- [2]

-- data\num\basic.lean
#print cast_pos_num -- [2]
#print num.zero.inj -- [1]
#print znum.zero.inj -- [1]
#print pos_num.one.inj -- [1]

-- data\mv_polynomial.lean
#print mv_polynomial.map_rename -- [5]
#print mv_polynomial.rename_add -- [4]
#print mv_polynomial.eval₂ -- [4, 5]
#print mv_polynomial.eval₂_rename_prodmk -- [5, 8]
#print mv_polynomial.rename_prodmk_eval₂ -- [4]
#print mv_polynomial.tmp.coe -- [3, 4]
#print mv_polynomial.rename_mul -- [4]
#print mv_polynomial.total_degree -- [3, 4]
#print mv_polynomial.ext -- [3, 4]
#print mv_polynomial.rename_monomial -- [4]
#print mv_polynomial.eval₂_rename -- [5, 8]
#print mv_polynomial.rename_X -- [4]
#print mv_polynomial.rename_C -- [4]
#print mv_polynomial.eval₂_congr -- [10]
#print mv_polynomial.eval_rename_prodmk -- [4]
#print mv_polynomial.eval₂_prod -- [12]
#print mv_polynomial.rename_eq -- [4]
#print mv_polynomial.injective_rename -- [4]
#print mv_polynomial.has_zero -- [3, 4]
#print mv_polynomial.rename_pow -- [4]
#print mv_polynomial.degrees_sub -- [5]
#print mv_polynomial.rename_one -- [4]
#print mv_polynomial.total_degree_rename_le -- [4]
#print mv_polynomial.rename_zero -- [4]
#print mv_polynomial.degrees_zero -- [4, 5]
#print mv_polynomial.rename_eval₂ -- [4]
#print mv_polynomial.rename.is_semiring_hom -- [4]
#print mv_polynomial.rename -- [4]
#print mv_polynomial.map -- [10]
#print mv_polynomial.degrees -- [4]
#print mv_polynomial.rename_id -- [3]
#print mv_polynomial.eval₂_sum -- [12]
#print mv_polynomial.degrees_neg -- [5]
#print mv_polynomial.eval₂_zero -- [4, 5]
#print mv_polynomial.rename_rename -- [5]

-- data\multiset.lean
#print multiset.length_ndinsert_of_mem -- [2]
#print multiset.length_ndinsert_of_not_mem -- [2]
#print multiset.le_inf -- [3]
#print multiset.sup_le -- [3]
#print multiset.pi.empty -- [2]

-- data\mllist.lean
#print tactic.mllist.m_of_list -- [2]
#print tactic.mllist.force -- [2]
#print tactic.mllist.enum_from -- [2]
#print tactic.mllist.map -- [2]
#print tactic.mllist.filter -- [2]
#print tactic.mllist.nil.inj -- [3]
#print tactic.mllist.of_list -- [2]
#print tactic.mllist.uncons -- [2]
#print tactic.mllist.mmap -- [2]
#print tactic.mllist.filter_map -- [2]
#print tactic.mllist.monad_lift -- [2]
#print tactic.mllist.join -- [2]
#print tactic.mllist.take -- [2]
#print tactic.mllist.mfilter -- [2]
#print tactic.mllist.append -- [2]
#print tactic.mllist.ibelow -- [3]
#print tactic.mllist.below -- [3]
#print tactic.mllist.mfilter_map -- [2]

-- data\matrix\pequiv.lean
#print pequiv.matrix_mul_apply -- [7]
#print pequiv.mul_matrix_apply -- [9]
#print pequiv.to_matrix -- [5]
#print pequiv.single_mul_single_right -- [10]

-- data\matrix\basic.lean
#print matrix.add_semigroup -- [3, 4]
#print matrix.add_comm_group -- [3, 4]
#print matrix.has_zero -- [3, 4]
#print matrix.minor -- [5, 8]
#print matrix.has_neg -- [3, 4]
#print matrix.module -- [3, 4]
#print matrix.add_monoid -- [3, 4]
#print matrix.add_group -- [3, 4]
#print matrix.diagonal -- [2]
#print matrix.has_add -- [3, 4]
#print matrix -- [3, 4]
#print matrix.add_comm_monoid -- [3, 4]
#print matrix.add_comm_semigroup -- [3, 4]
#print matrix.has_scalar -- [3, 4]

-- data\list\sigma.lean
#print list.nodupkeys_nil -- [2]
#print list.mem_ext -- [3]

-- data\list\min_max.lean
#print list.mem_foldr_min -- [2]
#print list.le_of_foldr_max -- [2]
#print list.mem_foldr_max -- [2]
#print list.le_of_foldr_min -- [2]

-- data\list\defs.lean
#print list.func.neg -- [2]
#print list.decidable_chain' -- [4]

-- data\list\basic.lean
#print list.length_insert_of_mem -- [2]
#print list.rel_filter_map -- [7, 8]
#print list.length_insert_of_not_mem -- [2]
#print list.chain'.iff_mem -- [3]

-- data\list\alist.lean
#print alist.disjoint -- [3]
#print alist.foldl -- [3]
#print alist.not_mem_empty -- [2]

-- data\int\sqrt.lean
#print int.sqrt_nonneg -- [1]

-- data\int\basic.lean
#print int.cast_one -- [4]
#print int.div_eq_div_of_mul_eq_mul -- [5]
#print int.eq_mul_div_of_mul_eq_mul_of_dvd_left -- [6]

-- data\hash_map.lean
#print hash_map.mk_as_list -- [3]

-- data\fp\basic.lean
#print fp.div_nat_lt_two_pow -- [1]
#print fp.rmode.NE.inj -- [1]
#print fp.float.nan.inj -- [2]

-- data\fintype.lean
#print fintype.bij_inv -- [5]
#print fintype.right_inverse_bij_inv -- [5]
#print fintype.choose_x -- [3]
#print fintype.decidable_surjective_fintype -- [4]

-- data\finsupp.lean
#print finsupp.uncurry -- [4, 5]
#print finsupp.sum_smul_index -- [4]
#print finsupp.mem_support_multiset_sum -- [3, 4]
#print finsupp.equiv_multiset -- [2]
#print finsupp.filter_apply_pos -- [3, 4]
#print finsupp.map_domain_zero -- [4]
#print finsupp.multiset_sum_sum_index -- [4, 5]
#print finsupp.preorder -- [3]
#print finsupp.prod_neg_index -- [4]
#print finsupp.sum_neg_index -- [4]
#print finsupp.has_scalar -- [4]
#print finsupp.erase_ne -- [4]
#print finsupp.single_of_emb_domain_single -- [5]
#print finsupp.filter -- [3]
#print finsupp.erase -- [4]
#print finsupp.mem_support_single -- [3, 4]
#print finsupp.comap_domain -- [4]
#print finsupp.curry -- [4, 5]
#print finsupp.map_range_finset_sum -- [12]
#print finsupp.single_eq_same -- [4]
#print finsupp.finsupp_prod_equiv -- [4, 5]
#print finsupp.erase_same -- [4]
#print finsupp.frange -- [3]
#print finsupp.sum_curry_index -- [5, 6]
#print finsupp.split -- [4]
#print finsupp.single_multiset_sum -- [3, 4]
#print finsupp.sum_neg -- [4, 5]
#print finsupp.sum_add -- [4, 5]
#print finsupp.subtype_domain -- [3, 4]
#print finsupp.single_finset_sum -- [4, 5]
#print finsupp.support_on_finset_subset -- [7]
#print finsupp.filter_apply_neg -- [3, 4]
#print finsupp.mem_frange -- [3]
#print finsupp.multiset_map_sum -- [5, 6]
#print finsupp.mem_support_finset_sum -- [4, 5]
#print finsupp.of_multiset_apply -- [2]
#print finsupp.split_support -- [5]
#print finsupp.single_sum -- [5, 6]
#print finsupp.to_multiset -- [2]
#print finsupp.sum_zero -- [4, 5]
#print finsupp.map_domain -- [5]
#print finsupp.support_single_ne_zero -- [3]
#print finsupp.subtype_domain.is_add_monoid_hom -- [7]
#print finsupp.multiset_sum_sum -- [4, 5]
#print finsupp.of_multiset -- [2]
#print finsupp.single_eq_of_ne -- [4]
#print finsupp.emb_domain_map_range -- [8]
#print finsupp.count_to_multiset -- [2]
#print finsupp.map_domain_congr -- [4]
#print finsupp.eq_zero_of_comap_domain_eq_zero -- [6]
#print finsupp.support_subset_iff -- [6]

-- data\finset.lean
#print finset.card_lt_card -- [2]
#print finset.map_empty -- [4]
#print finset.subset_image_iff -- [3]
#print finset.card_le_card_of_inj_on -- [3]
#print finset.fold_map -- [9]
#print finset.image_singleton -- [4]
#print finset.subset_insert -- [2]
#print finset.pi.empty -- [2]
#print finset.image_const -- [3]
#print finset.coe_filter -- [4]

-- data\finmap.lean
#print finmap.disjoint_empty -- [3]
#print finmap.disjoint -- [3]
#print finmap.foldl -- [3]
#print finmap.not_mem_empty -- [2]

-- data\fin.lean
#print fin.add_nat_val -- [4]

-- data\equiv\basic.lean
#print equiv.symm_trans_swap_trans -- [3]

-- data\equiv\algebra.lean
#print equiv.coe_units_equiv_ne_zero -- [2]

-- data\dfinsupp.lean
#print dfinsupp.subtype_domain_sum -- [3, 6]
#print dfinsupp.map_range_def -- [8]
#print dfinsupp.decidable_eq -- [3]
#print dfinsupp.map_range_single -- [7, 8]
#print dfinsupp.sum_apply -- [3]
#print dfinsupp.zip_with_def -- [5]

-- data\complex\exponential.lean
#print is_cau_series_of_abv_le_cau -- [5]
#print abv_sum_le_sum_abv -- [5]

-- data\analysis\topology.lean
#print ctop.realizer.nhds_F -- [4]
#print ctop.realizer.nhds_σ -- [4]
#print compact.realizer -- [3]

-- computability\turing_machine.lean
#print turing.TM1.stmt.halt.inj -- [5]
#print turing.TM1to1.supports_stmt_write -- [7]
#print turing.TM2to1.st_run -- [5]
#print turing.TM1to1.tr_tape_drop_right -- [2]
#print turing.TM2to1.stackel.bottom.inj -- [5]
#print turing.TM1to1.step_aux_write -- [10, 11]
#print turing.TM2.stmt.halt.inj -- [6]
#print turing.TM1to1.supports_stmt_move -- [8]
#print turing.TM2.stmts₁ -- [6, 7, 8, 9, 10]
#print turing.TM0.machine.map_step -- [15]
#print turing.TM1.stmts₁ -- [5, 6, 7]
#print turing.TM2to1.tr_stk -- [5, 7, 8]
#print turing.TM1to1.tr_tape' -- [2]
#print turing.TM1to1.step_aux_move -- [9]
#print turing.dir.left.inj -- [1]
#print turing.TM1to0.Λ' -- [4, 6, 7]
#print turing.TM2to1.tr_stmts₁ -- [8, 9, 10, 11]
#print turing.TM1.supports_stmt -- [5, 6, 7]
#print turing.dir.right.inj -- [1]
#print turing.TM2to1.stackel.top.inj -- [5]
#print turing.TM2.supports_stmt -- [6, 7, 8, 9, 10]
#print turing.TM0.machine.map_respects -- [17]
#print turing.TM1to0.tr_eval -- [8, 9]
#print turing.TM0.machine -- [4]

-- computability\partrec_code.lean
#print nat.partrec.code.zero.inj -- [1]
#print nat.partrec.code.left.inj -- [1]
#print nat.partrec.code.succ.inj -- [1]
#print nat.partrec.code.right.inj -- [1]

-- category_theory\single_obj.lean
#print category_theory.single_obj.star -- [1]
#print category_theory.single_obj.to_End -- [2]
#print category_theory.single_obj -- [1]

-- category_theory\monoidal\category_aux.lean
#print category_theory.tensor_obj_type -- [2]

-- category_theory\monad\limits.lean
#print category_theory.monad.forget_creates_limits.γ -- [8]

-- category_theory\limits\types.lean
#print category_theory.limits.types.types_colimit_pre -- [7]

-- category_theory\limits\shapes\pullbacks.lean
#print category_theory.limits.walking_span.right.inj -- [1]
#print category_theory.limits.walking_cospan.hom.inr.inj -- [1]
#print category_theory.limits.walking_span.hom.id.inj -- [2]
#print category_theory.limits.walking_span.left.inj -- [1]
#print category_theory.limits.walking_cospan.one.inj -- [1]
#print category_theory.limits.walking_cospan.right.inj -- [1]
#print category_theory.limits.walking_cospan.hom.inl.inj -- [1]
#print category_theory.limits.walking_span.hom.snd.inj -- [1]
#print category_theory.limits.walking_span.zero.inj -- [1]
#print category_theory.limits.walking_span.hom.fst.inj -- [1]
#print category_theory.limits.walking_cospan.left.inj -- [1]
#print category_theory.limits.walking_cospan.hom.id.inj -- [2]

-- category_theory\limits\shapes\equalizers.lean
#print category_theory.limits.walking_parallel_pair_hom.right.inj -- [1]
#print category_theory.limits.walking_parallel_pair.zero.inj -- [1]
#print category_theory.limits.walking_parallel_pair_hom.left.inj -- [1]
#print category_theory.limits.walking_parallel_pair_hom.id.inj -- [2]
#print category_theory.limits.walking_parallel_pair.one.inj -- [1]

-- category_theory\limits\shapes\binary_products.lean
#print category_theory.limits.walking_pair.left.inj -- [1]
#print category_theory.limits.walking_pair.right.inj -- [1]

-- category_theory\limits\preserves.lean
#print category_theory.limits.id_preserves_colimits -- [4]
#print category_theory.limits.id_reflects_colimits -- [4]
#print category_theory.limits.id_reflects_limits -- [4]
#print category_theory.limits.id_preserves_limits -- [4]

-- category_theory\isomorphism.lean
#print category_theory.iso.trans_mk -- [14, 15]

-- category_theory\instances\kleisli.lean
#print category_theory.Kleisli.mk -- [2]
#print category_theory.Kleisli -- [2]
#print category_theory.Kleisli.comp_def -- [3]
#print category_theory.Kleisli.id_def -- [3]

-- category_theory\full_subcategory.lean
#print category_theory.induced_category -- [3, 4]

-- category_theory\concrete_category.lean
#print category_theory.concrete_category.mk.inj -- [7]

-- category\traversable\instances.lean
#print list.comp_traverse -- [5]
#print sum.traverse_map -- [4]
#print sum.comp_traverse -- [6]
#print option.comp_traverse -- [5]

-- category\traversable\derive.lean
#print tactic.interactive.traverse_field -- [2]
#print tactic.interactive.traverse_constructor -- [6]

-- category\traversable\basic.lean
#print is_lawful_traversable.mk.inj -- [13]

-- category\monad\writer.lean
#print writer_t.ext -- [3]
#print writer_t.adapt -- [3]
#print writer_t.monad_map -- [4, 5]
#print writer_t.monad_except -- [3]

-- category\monad\cont.lean
#print writer_t.monad_cont -- [2]
#print is_lawful_monad_cont.mk.inj -- [12]
#print state_t.mk_label -- [2]

-- category\functor.lean
#print functor.const -- [2]
#print functor.const.mk -- [2]
#print functor.add_const.mk -- [2]
#print functor.comp.run_map -- [5, 6]
#print functor.const.map -- [4]

-- category\fold.lean
#print traversable.mfoldl.unop_of_free_monoid -- [5]
#print monoid.mfoldr.mk -- [2]

-- category\bitraversable\instances.lean
#print bitraversable.traversable -- [3]
#print const.bitraverse -- [2, 8]
#print bitraversable.is_lawful_traversable -- [3]

-- category\bifunctor.lean
#print is_lawful_bifunctor.mk.inj -- [7]

-- category\basic.lean
#print map_seq -- [6]
#print seq_map_assoc -- [6]

-- analysis\normed_space\operator_norm.lean
#print exists_pos_bound_of_bound -- [6, 8]
#print continuous_linear_map.is_O_comp -- [7]

-- analysis\normed_space\bounded_linear_maps.lean
#print is_bounded_linear_map.is_O_comp -- [5]

-- analysis\normed_space\basic.lean
#print normed_group.core.mk.inj -- [10]

-- analysis\convex.lean
#print convex_on_sum -- [9]

-- analysis\calculus\times_cont_diff.lean
#print times_cont_diff.times_cont_diff_fderiv_apply -- [11]

-- analysis\asymptotics.lean
#print asymptotics.is_o_iff_tendsto -- [3]

-- algebra\punit_instances.lean
#print punit.le -- [1, 2]
#print punit.not_lt -- [1, 2]

-- algebra\ordered_ring.lean
#print with_top.has_one -- [3]
#print with_top.coe_eq_zero -- [4]
#print with_top.zero_ne_top -- [4]
#print with_top.canonically_ordered_comm_semiring -- [2, 3]
#print with_top.top_ne_zero -- [4]
#print with_top.coe_zero -- [3, 4]

-- algebra\group\with_one.lean
#print with_zero.map_eq -- [2, 3, 5]
#print with_zero.lift_coe -- [2]
#print with_zero.lift_unique -- [2]
#print with_one.lift_unique -- [2]
#print with_one.lift_coe -- [2]
#print with_one.map_eq -- [2, 3, 5]
#print with_zero.lift_zero -- [2]
#print with_one.lift_one -- [2]

-- algebra\direct_sum.lean
#print direct_sum -- [2]
#print direct_sum.has_coe_to_fun -- [2]
#print direct_sum.add_comm_group -- [2]
#print direct_sum.to_group_of -- [8]

-- algebra\direct_limit.lean
#print ring.direct_limit.comm_ring -- [9, 10]
#print ring.direct_limit.of_f -- [9, 10]
#print ring.direct_limit.lift_of -- [9, 10, 14, 15]
#print ring.direct_limit.lift -- [9, 10]
#print module.direct_limit.totalize -- [12]
#print module.direct_limit.lift_of -- [12, 17]
#print module.direct_limit -- [12]
#print module.direct_limit.add_comm_group -- [12]
#print module.direct_limit.module -- [12]
#print ring.direct_limit -- [9, 10]
#print ring.direct_limit.of -- [9, 10]
#print module.direct_limit.lift -- [12]
#print module.direct_limit.of -- [12]

-- algebra\big_operators.lean
#print finset.sum_le_sum_of_subset -- [8]
#print finset.sum_eq_zero -- [3]
#print finset.prod_eq_one -- [3]

-- algebra\associated.lean
#print associates.has_dvd -- [2]
#print associates.le_of_mul_le_mul_left -- [2]
#print associates.dvd_eq_le -- [2]
#print associates.eq_of_mul_eq_mul_left -- [2]
#print associates.one_or_eq_of_le_of_prime -- [2]

-- algebra\archimedean.lean
#print round -- [3]

-- algebra\Mon\colimits.lean
#print Mon.colimits.prequotient.one.inj -- [4]

-- algebra\CommRing\colimits.lean
#print CommRing.colimits.prequotient.one.inj -- [4]
#print CommRing.colimits.prequotient.zero.inj -- [4]