sanity_check_mathlib

/- Note: This command is still in development. -/
/- Checking 26901 declarations in mathlib (only in imported files) -/

/- UNUSED ARGUMENTS: -/

-- topology/stone_cech.lean
#print ultrafilter.extend /- argument 4: [_inst_2 : t2_space γ] -/

-- topology/instances/polynomial.lean
#print polynomial.continuous_eval /- argument 3: [_inst_2 : decidable_eq α] -/
#print polynomial.tendsto_infinity /- argument 7: [_inst_4 : decidable_eq α] -/

-- topology/algebra/uniform_ring.lean
#print uniform_space.completion.has_one /- argument 4: [_inst_3 : uniform_add_group α], argument 5: [_inst_4 : topological_ring α] -/
#print uniform_space.completion.has_mul /- argument 4: [_inst_3 : uniform_add_group α], argument 5: [_inst_4 : topological_ring α] -/

-- topology/algebra/open_subgroup.lean
#print open_add_subgroup /- argument 4: [_inst_3 : topological_add_group G] -/
#print open_subgroup /- argument 4: [_inst_3 : topological_group G] -/

-- topology/algebra/group_completion.lean
#print uniform_space.completion.is_add_group_hom_map /- argument 8: [_inst_6 : uniform_add_group β] -/

-- tactic/where.lean
#print where.where_cmd /- argument 1: (_x : interactive.decl_meta_info) -/

-- tactic/tfae.lean
#print tactic.interactive.tfae_have /- argument 5: (discharger : opt_param (tactic unit) tactic.solve_by_elim) -/

-- tactic/ring2.lean
#print tactic.ring2.horner_expr.inv /- argument 1: (e : tactic.ring2.horner_expr) -/

-- tactic/restate_axiom.lean
#print restate_axiom_cmd /- argument 1: (meta_info : interactive.decl_meta_info) -/

-- tactic/replacer.lean
#print tactic.def_replacer_cmd /- argument 1: (meta_info : interactive.decl_meta_info) -/

-- tactic/norm_num.lean
#print norm_num.prove_lt /- argument 1: (simp : expr → tactic (expr × expr)) -/

-- tactic/monotonicity/interactive.lean
#print tactic.interactive.mono_aux /- argument 2: (cfg : opt_param tactic.interactive.mono_cfg {unify := ff}) -/
#print tactic.interactive.match_ac /- argument 2: (unif : bool) -/

-- tactic/monotonicity/basic.lean
#print tactic.interactive.monotoncity.check /- argument 2: (prio : ℕ), argument 3: (persistent : bool) -/
#print tactic.interactive.monotoncity.check_rel /- argument 1: (xs : list expr) -/

-- tactic/localized.lean
#print localized_cmd /- argument 1: (meta_info : interactive.decl_meta_info) -/
#print open_locale_cmd /- argument 1: (meta_info : interactive.decl_meta_info) -/

-- tactic/local_cache.lean
#print tactic.local_cache.internal.save_data /- argument 3: [_inst_2 : has_reflect α] -/
#print tactic.local_cache.internal.load_data /- argument 3: [_inst_2 : has_reflect α] -/

-- tactic/linarith.lean
#print linarith.mul_eq /- argument 6: (hb : b > 0) -/

-- tactic/doc_blame.lean
#print doc_cmd /- argument 1: (_x : interactive.decl_meta_info) -/

-- tactic/core.lean
#print tactic.symmetry_hyp /- argument 2: (md : opt_param tactic.transparency semireducible) -/

-- tactic/converter/interactive.lean
#print old_conv.istep /- argument 3: (col0 : ℕ) (duplicate) -/

-- tactic/converter/binders.lean
#print binder_eq_elim.check_eq /- argument 1: (b : binder_eq_elim) -/

-- tactic/chain.lean
#print tactic.trace_output /- argument 2: [_inst_1 : has_to_string (tactic.tactic_script α)] -/

-- set_theory/zfc.lean
#print Set.map_definable_aux /- argument 2: [H : pSet.definable 1 f] -/

-- set_theory/surreal.lean
#print pgame.add_lt_add /- argument 5: (ow : pgame.numeric w), argument 6: (ox : pgame.numeric x) -/
#print pgame.numeric.lt_move_right /- argument 2: (o : pgame.numeric x) -/
#print pgame.numeric.move_left_lt /- argument 2: (o : pgame.numeric x) -/

-- set_theory/ordinal_notation.lean
#print onote.oadd_lt_oadd_2 /- argument 7: (h₂ : onote.NF (onote.oadd e n₂ o₂)) -/
#print onote.oadd_lt_oadd_1 /- argument 8: (h₂ : onote.NF (onote.oadd e₂ n₂ o₂)) -/
#print onote.oadd_lt_oadd_3 /- argument 5: (h₁ : onote.NF (onote.oadd e n a₁)), argument 6: (h₂ : onote.NF (onote.oadd e n a₂)) -/

-- set_theory/ordinal.lean
#print principal_seg.of_element /- argument 3: [_inst_1 : is_well_order α r] -/
#print principal_seg.lt_le /- argument 7: [_inst_1 : is_trans β s] -/
#print principal_seg.lt_le_top /- argument 8: [_inst_2 : is_trans γ t] -/
#print principal_seg.lt_equiv /- argument 7: [_inst_1 : is_trans β s], argument 8: [_inst_2 : is_trans γ t] -/
#print principal_seg.equiv_lt /- argument 7: [_inst_1 : is_trans β s], argument 8: [_inst_2 : is_trans γ t] -/

-- ring_theory/unique_factorization_domain.lean
#print associates.factor_set /- argument 3: [_inst_5 : unique_factorization_domain α] -/
#print associates.unique' /- argument 4: [_inst_3 : decidable_eq (associates α)] -/
#print associates.factor_set.coe_add /- argument 4: [_inst_3 : decidable_eq (associates α)] -/
#print unique_factorization_domain.exists_mem_factors_of_dvd /- argument 4: [_inst_3 : decidable_eq (associates α)] -/
#print associates.factors' /- argument 4: [_inst_3 : decidable_eq (associates α)] -/
#print associates.factor_set.prod /- argument 4: [_inst_3 : decidable_eq (associates α)] -/

-- ring_theory/power_series.lean
#print mv_power_series.map /- argument 3: [_inst_1 : semiring α], argument 5: [_inst_2 : semiring β] -/

-- ring_theory/polynomial.lean
#print polynomial.of_subring /- argument 3: [_inst_2 : decidable_eq R] -/

-- ring_theory/multiplicity.lean
#print multiplicity.finite_mul_aux /- argument 3: [_inst_2 : decidable_rel has_dvd.dvd] -/

-- ring_theory/localization.lean
#print localization.r /- argument 4: [_inst_2 : is_submonoid S] -/
#print localization.fraction_ring.eq_zero_of_ne_zero_of_mul_eq_zero /- argument 3: [_inst_4 : decidable_eq β] -/

-- ring_theory/integral_closure.lean
#print is_integral /- argument 6: [_inst_4 : decidable_eq A] -/

-- ring_theory/ideal_operations.lean
#print ideal.map /- argument 6: [_inst_3 : is_ring_hom f] -/

-- ring_theory/algebra.lean
#print algebra.comap /- argument 7: [_inst_4 : algebra R S], argument 8: [_inst_5 : algebra S A] -/
#print mv_polynomial.eval_unique /- argument 7: [_inst_5 : decidable_eq A] -/
#print algebra.mv_polynomial /- argument 3: [_inst_6 : decidable_eq R], argument 5: [_inst_7 : decidable_eq ι] -/
#print algebra.polynomial /- argument 3: [_inst_6 : decidable_eq R] -/

-- ring_theory/adjoin_root.lean
#print adjoin_root /- argument 3: [_inst_2 : decidable_eq α] -/

-- ring_theory/adjoin.lean
#print algebra.adjoin_singleton_eq_range /- argument 7: [_inst_5 : decidable_eq A] -/

-- order/filter/filter_product.lean
#print filter.filter_product.of_seq_zero /- argument 5: (f : α → β) -/
#print filter.filter_product.of_seq_one /- argument 5: (f : α → β) -/
#print filter.filter_product.abs_def /- argument 7: (y : filter.filterprod β φ) (duplicate) -/

-- number_theory/pell.lean
#print pell.x_sub_y_dvd_pow_lem /- argument 2: (a1 : a > 1) -/
#print pell.az /- argument 2: (a1 : a > 1) -/
#print pell.eq_of_xn_modeq_lem1 /- argument 5: (npos : n > 0) -/

-- meta/rb_map.lean
#print native.rb_map.find_def /- argument 3: [_inst_1 : has_lt α] -/

-- measure_theory/measure_space.lean
#print measure_theory.measure' /- argument 4: (m0 : m ∅ is_measurable.empty = 0) -/

-- measure_theory/measurable_space.lean
#print is_measurable_range_inl /- argument 3: [_inst_1 : measurable_space α] (duplicate), argument 4: [_inst_2 : measurable_space β] (duplicate) -/
#print is_measurable_inl_image /- argument 3: [_inst_1 : measurable_space α] (duplicate), argument 4: [_inst_2 : measurable_space β] (duplicate) -/
#print is_measurable_inr_image /- argument 3: [_inst_1 : measurable_space α] (duplicate), argument 4: [_inst_2 : measurable_space β] (duplicate) -/
#print is_measurable_range_inr /- argument 3: [_inst_1 : measurable_space α] (duplicate), argument 4: [_inst_2 : measurable_space β] (duplicate) -/

-- measure_theory/l1_space.lean
#print measure_theory.lintegral_nnnorm_add /- argument 5: [_inst_3 : topological_space.second_countable_topology γ] -/
#print measure_theory.lintegral_nnnorm_neg /- argument 5: [_inst_3 : topological_space.second_countable_topology γ], argument 7: (hf : measurable f) -/
#print measure_theory.integrable /- argument 5: [_inst_3 : topological_space.second_countable_topology γ] -/
#print measure_theory.lintegral_nnnorm_zero /- argument 5: [_inst_3 : topological_space.second_countable_topology γ] -/

-- measure_theory/integration.lean
#print measure_theory.limsup_lintegral_le /- argument 6: (hg_meas : measurable g) -/
#print measure_theory.dominated_convergence_nn /- argument 7: (hf_meas : measurable f) -/
#print measure_theory.simple_func.integral_map /- argument 8: (hm : measurable m) -/
#print measure_theory.simple_func.approx /- argument 4: [_inst_2 : topological_space β] -/
#print measure_theory.simple_func.has_scalar /- argument 5: [_inst_3 : add_monoid β] -/
#print measure_theory.simple_func.ennreal_rat_embed_encode /- argument 2: (hq : 0 ≤ q) -/

-- measure_theory/borel_space.lean
#print measure_theory.is_measurable_Iio /- argument 2: [_inst_1 : topological_space α] (duplicate) -/
#print measure_theory.is_measurable_Ico /- argument 2: [_inst_1 : topological_space α] (duplicate) -/
#print measure_theory.borel_eq_subtype /- argument 2: [_inst_1 : topological_space α] (duplicate) -/
#print measure_theory.is_measurable_Ioo /- argument 2: [_inst_1 : topological_space α] (duplicate) -/
#print measure_theory.measurable.supr_Prop /- argument 4: [_inst_4 : orderable_topology α], argument 5: [_inst_5 : topological_space.second_countable_topology α] -/
#print measure_theory.borel_induced /- argument 3: [_inst_1 : topological_space α] -/
#print measure_theory.measurable.infi_Prop /- argument 4: [_inst_4 : orderable_topology α], argument 5: [_inst_5 : topological_space.second_countable_topology α] -/
#print measure_theory.measurable_smul /- argument 6: [_inst_3 : topological_space.second_countable_topology α], argument 9: [_inst_6 : topological_space.second_countable_topology β] -/
#print measure_theory.measurable_of_continuous2 /- argument 5: [_inst_1 : topological_space α] (duplicate) -/

-- measure_theory/bochner_integration.lean
#print measure_theory.l1.simple_func.to_simple_func /- argument 6: [_inst_4 : normed_space ℝ γ] -/

-- measure_theory/ae_eq_fun.lean
#print measure_theory.ae_eq_fun.preorder /- argument 4: [_inst_2 : measurable_space β] (duplicate) -/
#print measure_theory.ae_eq_fun.partial_order /- argument 4: [_inst_2 : measurable_space β] (duplicate) -/
#print measure_theory.ae_eq_fun.edist_eq_add_add /- argument 6: [_inst_5 : topological_add_group γ] -/
#print measure_theory.ae_eq_fun.neg /- argument 5: [_inst_4 : topological_space.second_countable_topology γ] -/
#print measure_theory.ae_eq_fun.mk_le_mk /- argument 4: [_inst_2 : measurable_space β] (duplicate) -/

-- logic/basic.lean
#print imp_intro /- argument 4: (a : β) -/

-- linear_algebra/finsupp.lean
#print finsupp.supported_eq_span_single /- argument 6: [_inst_3 : module γ β], argument 7: [_inst_4 : has_one β] -/

-- linear_algebra/finite_dimensional.lean
#print finite_dimensional.of_fg /- argument 6: [_inst_4 : decidable_eq V] -/

-- linear_algebra/dual.lean
#print is_basis.eval_finsupp_at /- argument 4: [_inst_6 : decidable_eq ι] -/
#print is_basis.coord_fun /- argument 8: [_inst_5 : decidable_eq (module.dual K V)] -/

-- linear_algebra/dimension.lean
#print dim_quotient /- argument 7: [_inst_8 : decidable_eq (submodule.quotient p)] -/

-- linear_algebra/basis.lean
#print mem_span_insert_exchange /- argument 3: [_inst_3 : decidable_eq α], argument 4: [_inst_4 : decidable_eq β] -/
#print is_basis.constr /- argument 9: [_inst_5 : decidable_eq γ] -/
#print disjoint_span_singleton /- argument 4: [_inst_4 : decidable_eq β] -/
#print linear_independent /- argument 5: [_inst_1 : decidable_eq ι], argument 6: [_inst_3 : decidable_eq α], argument 7: [_inst_4 : decidable_eq β] -/
#print constr_smul /- argument 7: [_inst_16 : decidable_eq β], argument 12: [_inst_21 : module α β], argument 18: {b : β} -/
#print is_basis.ext /- argument 9: [_inst_5 : decidable_eq γ] -/

-- linear_algebra/basic.lean
#print linear_map.sum_apply /- argument 11: [_inst_8 : module α δ], argument 12: [_inst_10 : decidable_eq δ] -/
#print linear_map.std_basis_eq_single /- argument 5: [_inst_11 : decidable_eq α] -/

-- group_theory/subgroup.lean
#print is_add_subgroup.mem_trivial /- argument 2: [_inst_1 : add_group α] (duplicate) -/
#print is_group_hom.ker /- argument 6: [_inst_3 : is_group_hom f] -/
#print is_subgroup.normalizer_is_subgroup /- argument 4: [_inst_2 : is_subgroup s] -/
#print is_add_subgroup.normalizer_is_add_subgroup /- argument 4: [_inst_2 : is_add_subgroup s] -/
#print is_add_group_hom.ker /- argument 6: [_inst_3 : is_add_group_hom f] -/
#print is_subgroup.mem_trivial /- argument 2: [_inst_1 : group α] (duplicate) -/

-- group_theory/perm/sign.lean
#print equiv.perm.sign_cycle /- argument 3: [_inst_2 : fintype α] (duplicate) -/
#print equiv.perm.is_cycle_swap /- argument 3: [_inst_2 : fintype α] -/
#print equiv.perm.eq_swap_of_is_cycle_of_apply_apply_eq_self /- argument 3: [_inst_2 : fintype α] -/
#print equiv.perm.card_support_swap /- argument 3: [_inst_2 : fintype α] (duplicate) -/
#print equiv.perm.is_cycle_swap_mul_aux₁ /- argument 3: [_inst_2 : fintype α] -/
#print equiv.perm.support_swap /- argument 3: [_inst_2 : fintype α] (duplicate) -/

-- group_theory/order_of_element.lean
#print card_subgroup_dvd_card /- argument 4: [_inst_3 : decidable_eq α] -/
#print card_trivial /- argument 3: [_inst_2 : fintype α], argument 4: [_inst_3 : decidable_eq α] -/
#print quotient_group.fintype /- argument 4: [_inst_3 : decidable_eq α] -/

-- group_theory/eckmann_hilton.lean
#print eckmann_hilton.comm_group /- argument 7: (h₂ : eckmann_hilton.is_unital m₂ e₂) -/

-- group_theory/coset.lean
#print quotient_group.eq_class_eq_left_coset /- argument 2: [_inst_1 : group α] (duplicate) -/
#print quotient_group.inhabited /- argument 2: [_inst_1 : group α] (duplicate) -/
#print normal_of_eq_cosets /- argument 4: [_inst_2 : is_subgroup s] -/
#print normal_of_eq_add_cosets /- argument 4: [_inst_2 : is_add_subgroup s] -/
#print quotient_add_group.eq_class_eq_left_coset /- argument 2: [_inst_1 : add_group α] (duplicate) -/
#print quotient_add_group.inhabited /- argument 2: [_inst_1 : add_group α] (duplicate) -/

-- group_theory/abelianization.lean
#print abelianization.lift.unique /- argument 8: [_inst_4 : is_group_hom g] -/

-- field_theory/splitting_field.lean
#print polynomial.splits /- argument 6: [_inst_4 : is_field_hom i] -/

-- field_theory/perfect_closure.lean
#print perfect_closure.has_inv /- argument 4: [_inst_2 : prime p], argument 5: [_inst_3 : char_p α p] -/
#print perfect_closure.eq_iff' /- argument 4: [_inst_2 : prime p], argument 5: [_inst_3 : char_p α p] -/

-- field_theory/mv_polynomial.lean
#print mv_polynomial.R /- argument 3: [_inst_1 : fintype σ] -/
#print mv_polynomial.evalₗ /- argument 4: [_inst_2 : fintype α], argument 5: [_inst_3 : fintype σ] -/

-- field_theory/finite.lean
#print subgroup_units_cyclic /- argument 3: [_inst_2 : decidable_eq α] -/

-- data/zmod/quadratic_reciprocity.lean
#print quadratic_reciprocity_aux.card_range_p_mul_q_filter_not_coprime /- argument 4: (hq : prime q), argument 7: (hpq : p ≠ q) -/
#print quadratic_reciprocity_aux.prod_range_div_two_erase_zero /- argument 4: (hq : prime q), argument 6: (hq1 : q % 2 = 1), argument 7: (hpq : p ≠ q) -/
#print quadratic_reciprocity_aux.filter_range_p_mul_q_div_two_eq /- argument 7: (hpq : p ≠ q) -/

-- data/vector2.lean
#print vector.traverse_def /- argument 4: [_inst_3 : is_lawful_applicative F] -/

-- data/set/function.lean
#print set.right_inv_on_of_eq_on_left /- argument 6: {a : set α} -/

-- data/set/finite.lean
#print set.not_injective_nat_fintype /- argument 3: [_inst_2 : decidable_eq α] -/
#print set.fintype_of_fintype_image /- argument 3: [_inst_1 : decidable_eq β] -/
#print finset.coe_to_finset' /- argument 2: [_inst_2 : decidable_eq α] -/

-- data/seq/wseq.lean
#print wseq.think_congr /- argument 4: (a : α) -/

-- data/seq/computation.lean
#print computation.map_congr /- argument 3: (R : α → α → Prop), argument 4: (S : β → β → Prop) -/

-- data/real/cau_seq.lean
#print cau_seq.lim_zero /- argument 6: [_inst_3 : is_absolute_value abv] -/

-- data/rat/order.lean
#print rat.le_def' /- argument 3: (p_pos : 0 < p), argument 4: (q_pos : 0 < q) -/

-- data/prod.lean
#print prod.lex.decidable /- argument 4: [_inst_2 : decidable_eq β] -/

-- data/polynomial.lean
#print polynomial.eval₂_zero /- argument 7: [_inst_3 : is_semiring_hom f] -/

-- data/pnat/basic.lean
#print pnat.div_exact /- argument 3: (h : k ∣ m) -/

-- data/pequiv.lean
#print pequiv.trans_single_of_eq_none /- argument 4: [_inst_1 : decidable_eq α] -/

-- data/padics/padic_numbers.lean
#print padic_seq /- argument 2: [_inst_1 : prime p] -/

-- data/padics/padic_norm.lean
#print padic_norm.neg /- argument 2: [hp : prime p] -/

-- data/num/basic.lean
#print cast_pos_num /- argument 2: [_inst_1 : has_zero α] -/

-- data/mv_polynomial.lean
#print mv_polynomial.eval₂_congr /- argument 8: [_inst_3 : is_semiring_hom f] -/
#print mv_polynomial.map /- argument 7: [_inst_3 : is_semiring_hom f] -/

-- data/multiset.lean
#print multiset.length_ndinsert_of_mem /- argument 2: [_inst_1 : decidable_eq α] (duplicate) -/
#print multiset.length_ndinsert_of_not_mem /- argument 2: [_inst_1 : decidable_eq α] (duplicate) -/
#print multiset.le_inf /- argument 3: [_inst_2 : decidable_eq α] -/
#print multiset.sup_le /- argument 3: [_inst_2 : decidable_eq α] -/
#print multiset.pi.empty /- argument 2: [_inst_1 : decidable_eq α] -/

-- data/mllist.lean
#print tactic.mllist.m_of_list /- argument 2: [_inst_1 : alternative m] -/
#print tactic.mllist.force /- argument 2: [_inst_1 : alternative m] -/
#print tactic.mllist.enum_from /- argument 2: [_inst_1 : alternative m] -/
#print tactic.mllist.map /- argument 2: [_inst_1 : alternative m] -/
#print tactic.mllist.filter /- argument 2: [_inst_1 : alternative m] -/
#print tactic.mllist.of_list /- argument 2: [_inst_1 : alternative m] -/
#print tactic.mllist.uncons /- argument 2: [_inst_1 : alternative m] -/
#print tactic.mllist.mmap /- argument 2: [_inst_1 : alternative m] -/
#print tactic.mllist.filter_map /- argument 2: [_inst_1 : alternative m] -/
#print tactic.mllist.monad_lift /- argument 2: [_inst_1 : alternative m] -/
#print tactic.mllist.join /- argument 2: [_inst_1 : alternative m] -/
#print tactic.mllist.take /- argument 2: [_inst_1 : alternative m] -/
#print tactic.mllist.mfilter /- argument 2: [_inst_1 : alternative m] (duplicate) -/
#print tactic.mllist.append /- argument 2: [_inst_1 : alternative m] -/
#print tactic.mllist.mfilter_map /- argument 2: [_inst_1 : alternative m] (duplicate) -/

-- data/matrix/pequiv.lean
#print pequiv.matrix_mul_apply /- argument 7: [_inst_6 : decidable_eq l] -/
#print pequiv.mul_matrix_apply /- argument 9: [_inst_8 : decidable_eq n] -/
#print pequiv.to_matrix /- argument 5: [_inst_7 : decidable_eq m] -/
#print pequiv.single_mul_single_right /- argument 10: [_inst_6 : decidable_eq l] -/

-- data/matrix/basic.lean
#print matrix /- argument 3: [_inst_1 : fintype m], argument 4: [_inst_2 : fintype n] -/

-- data/list/sigma.lean
#print list.mem_ext /- argument 3: [_inst_1 : decidable_eq α] -/

-- data/list/defs.lean
#print list.func.neg /- argument 2: [_inst_1 : inhabited α] -/

-- data/list/basic.lean
#print list.length_insert_of_mem /- argument 2: [_inst_1 : decidable_eq α] (duplicate) -/
#print list.rel_filter_map /- argument 7: {f : α → option γ}, argument 8: {q : β → option δ} -/
#print list.length_insert_of_not_mem /- argument 2: [_inst_1 : decidable_eq α] (duplicate) -/
#print list.chain'.iff_mem /- argument 3: {S : α → α → Prop} (duplicate) -/

-- data/list/alist.lean
#print alist.disjoint /- argument 3: [_inst_1 : decidable_eq α] -/
#print alist.foldl /- argument 3: [_inst_1 : decidable_eq α] -/

-- data/int/basic.lean
#print int.div_eq_div_of_mul_eq_mul /- argument 5: (H1 : b ∣ a) -/
#print int.eq_mul_div_of_mul_eq_mul_of_dvd_left /- argument 6: (hd : d ≠ 0) -/

-- data/hash_map.lean
#print hash_map.mk_as_list /- argument 3: [_inst_1 : decidable_eq α] -/

-- data/fp/basic.lean
#print fp.div_nat_lt_two_pow /- argument 1: [C : fp.float_cfg] -/

-- data/fintype.lean
#print fintype.bij_inv /- argument 5: [_inst_3 : fintype β] -/
#print fintype.choose_x /- argument 3: [_inst_2 : decidable_eq α] -/
#print fintype.decidable_surjective_fintype /- argument 4: [_inst_2 : decidable_eq α] -/

-- data/finsupp.lean
#print finsupp.subtype_domain.is_add_monoid_hom /- argument 4: [_inst_2 : add_monoid β] (duplicate) -/

-- data/finset.lean
#print finset.card_lt_card /- argument 2: [_inst_1 : decidable_eq α] -/
#print finset.map_empty /- argument 4: (s : finset α) -/
#print finset.subset_image_iff /- argument 3: [_inst_1 : decidable_eq β] (duplicate) -/
#print finset.card_le_card_of_inj_on /- argument 3: [_inst_1 : decidable_eq α] -/
#print finset.fold_map /- argument 9: [_inst_1 : decidable_eq α] -/
#print finset.image_singleton /- argument 4: [_inst_2 : decidable_eq α] -/
#print finset.subset_insert /- argument 2: [_inst_1 : decidable_eq α] (duplicate) -/
#print finset.pi.empty /- argument 2: [_inst_1 : decidable_eq α] (duplicate) -/
#print finset.image_const /- argument 3: [_inst_1 : decidable_eq β] (duplicate) -/
#print finset.coe_filter /- argument 4: [_inst_3 : decidable_eq α] -/

-- data/finmap.lean
#print finmap.disjoint /- argument 3: [_inst_1 : decidable_eq α] -/
#print finmap.foldl /- argument 3: [_inst_1 : decidable_eq α] -/

-- data/fin.lean
#print fin.add_nat_val /- argument 4: (h : m ≤ i.val) -/

-- data/equiv/basic.lean
#print equiv.symm_trans_swap_trans /- argument 3: [_inst_1 : decidable_eq α] (duplicate) -/

-- data/equiv/algebra.lean
#print equiv.coe_units_equiv_ne_zero /- argument 2: [_inst_1 : group α] -/

-- data/dfinsupp.lean
#print dfinsupp.subtype_domain_sum /- argument 3: [_inst_1 : decidable_eq ι], argument 6: [_inst_3 : Π (i : ι), decidable_pred (eq 0)] -/
#print dfinsupp.map_range_def /- argument 8: [_inst_7 : Π (i : ι), decidable_pred (eq 0)] -/
#print dfinsupp.decidable_eq /- argument 3: [_inst_1 : decidable_eq ι] (duplicate) -/
#print dfinsupp.map_range_single /- argument 7: [_inst_6 : Π (i : ι), decidable_pred (eq 0)], argument 8: [_inst_7 : Π (i : ι), decidable_pred (eq 0)] -/
#print dfinsupp.sum_apply /- argument 3: [_inst_1 : decidable_eq ι] -/
#print dfinsupp.zip_with_def /- argument 5: [_inst_3 : Π (i : ι), decidable_pred (eq 0)] -/

-- data/complex/exponential.lean
#print is_cau_series_of_abv_le_cau /- argument 5: [_inst_3 : archimedean α] -/
#print abv_sum_le_sum_abv /- argument 5: [_inst_3 : archimedean α] -/

-- data/analysis/topology.lean
#print ctop.realizer.nhds_F /- argument 4: (m : α → β) -/
#print ctop.realizer.nhds_σ /- argument 4: (m : α → β) -/
#print compact.realizer /- argument 3: (R : ctop.realizer α) -/

-- computability/turing_machine.lean
#print turing.TM1to1.supports_stmt_write /- argument 7: [_inst_4 : fintype Γ] -/
#print turing.TM2to1.st_run /- argument 5: [_inst_2 : inhabited Λ] -/
#print turing.TM1to1.tr_tape_drop_right /- argument 2: [_inst_1 : inhabited Γ] -/
#print turing.TM1to1.step_aux_write /- argument 10: (enc0 : enc (default Γ) = vector.repeat ff n), argument 11: (encdec : ∀ (a : Γ), dec (enc a) = a) -/
#print turing.TM1to1.supports_stmt_move /- argument 8: [_inst_4 : fintype Γ] -/
#print turing.TM2.stmts₁ /- argument 6: [_inst_2 : inhabited Λ], argument 7: [_inst_3 : inhabited σ], argument 8: [_inst_4 : fintype K], argument 9: [_inst_5 : Π (k : K), fintype (Γ k)], argument 10: [_inst_6 : fintype σ] -/
#print turing.TM0.machine.map_step /- argument 15: (ss : turing.TM0.supports M S) -/
#print turing.TM1.stmts₁ /- argument 5: [_inst_2 : inhabited Λ], argument 6: [_inst_3 : inhabited σ], argument 7: [_inst_4 : fintype Γ] -/
#print turing.TM2to1.tr_stk /- argument 5: [_inst_2 : inhabited Λ], argument 7: [_inst_3 : inhabited σ], argument 8: (M : Λ → turing.TM2.stmt Γ Λ σ) -/
#print turing.TM1to1.tr_tape' /- argument 2: [_inst_1 : inhabited Γ] -/
#print turing.TM1to1.step_aux_move /- argument 9: (enc0 : enc (default Γ) = vector.repeat ff n) -/
#print turing.TM1to0.Λ' /- argument 4: [_inst_2 : inhabited Λ], argument 6: [_inst_3 : inhabited σ], argument 7: (M : Λ → turing.TM1.stmt Γ Λ σ) -/
#print turing.TM2to1.tr_stmts₁ /- argument 8: (M : Λ → turing.TM2.stmt Γ Λ σ), argument 9: [_inst_4 : fintype K], argument 10: [_inst_5 : Π (k : K), fintype (Γ k)], argument 11: [_inst_6 : fintype σ] -/
#print turing.TM1.supports_stmt /- argument 5: [_inst_2 : inhabited Λ], argument 6: [_inst_3 : inhabited σ], argument 7: [_inst_4 : fintype Γ] -/
#print turing.TM2.supports_stmt /- argument 6: [_inst_2 : inhabited Λ], argument 7: [_inst_3 : inhabited σ], argument 8: [_inst_4 : fintype K], argument 9: [_inst_5 : Π (k : K), fintype (Γ k)], argument 10: [_inst_6 : fintype σ] -/
#print turing.TM0.machine.map_respects /- argument 17: [_inst_6 : turing.pointed_map g₁] -/
#print turing.TM1to0.tr_eval /- argument 8: [_inst_4 : fintype Γ], argument 9: [_inst_5 : fintype σ] -/
#print turing.TM0.machine /- argument 4: [_inst_2 : inhabited Λ] -/

-- category_theory/single_obj.lean
#print category_theory.single_obj /- argument 1: (α : Type u) -/

-- category_theory/monad/limits.lean
#print category_theory.monad.forget_creates_limits.γ /- argument 8: [_inst_2 : category_theory.limits.has_limit (D ⋙ category_theory.monad.forget T)] -/

-- category_theory/limits/types.lean
#print category_theory.limits.types.types_colimit_pre /- argument 7: (g : (category_theory.limits.types.colimit (E ⋙ F)).X) -/

-- category_theory/limits/shapes/pullbacks.lean
#print category_theory.limits.pullback.condition /- argument 3: {W : C} (duplicate) -/
#print category_theory.limits.pushout.condition /- argument 3: {W : C} (duplicate) -/

-- category_theory/limits/preserves.lean
#print category_theory.limits.id_preserves_colimits /- argument 4: [𝒟 : category_theory.category D] -/
#print category_theory.limits.id_reflects_colimits /- argument 4: [𝒟 : category_theory.category D] -/
#print category_theory.limits.id_reflects_limits /- argument 4: [𝒟 : category_theory.category D] -/
#print category_theory.limits.id_preserves_limits /- argument 4: [𝒟 : category_theory.category D] -/

-- category_theory/full_subcategory.lean
#print category_theory.induced_category /- argument 3: [𝒟 : category_theory.category D], argument 4: (F : C → D) -/

-- category_theory/category/Kleisli.lean
#print category_theory.Kleisli /- argument 2: [_inst_1 : monad m] -/
#print category_theory.Kleisli.comp_def /- argument 3: [_inst_2 : is_lawful_monad m] -/
#print category_theory.Kleisli.id_def /- argument 3: [_inst_2 : is_lawful_monad m] -/

-- category/traversable/instances.lean
#print list.comp_traverse /- argument 5: [_inst_3 : is_lawful_applicative F] -/
#print sum.traverse_map /- argument 4: [_inst_4 : is_lawful_applicative G] -/
#print sum.comp_traverse /- argument 6: [_inst_3 : is_lawful_applicative F] -/
#print option.comp_traverse /- argument 5: [_inst_3 : is_lawful_applicative F] -/

-- category/traversable/derive.lean
#print tactic.interactive.traverse_field /- argument 2: (appl_inst : expr) (duplicate) -/
#print tactic.interactive.traverse_constructor /- argument 6: (β : expr) (duplicate) -/

-- category/monad/writer.lean
#print writer_t.ext /- argument 3: [_inst_1 : monad m] -/
#print writer_t.adapt /- argument 3: [_inst_1 : monad m] (duplicate) -/
#print writer_t.monad_map /- argument 4: [_inst_2 : monad m], argument 5: [_inst_3 : monad m'] -/
#print writer_t.monad_except /- argument 3: [_inst_1 : monad m] (duplicate) -/

-- category/monad/cont.lean
#print writer_t.monad_cont /- argument 2: [_inst_1 : monad m] (duplicate) -/
#print state_t.mk_label /- argument 2: [_inst_1 : monad m] -/

-- category/functor.lean
#print functor.const /- argument 2: (β : Type u_2) -/
#print functor.comp.run_map /- argument 5: [_inst_3 : is_lawful_functor F], argument 6: [_inst_4 : is_lawful_functor G] -/
#print functor.const.map /- argument 4: (f : α → β) -/

-- category/fold.lean
#print traversable.mfoldl.unop_of_free_monoid /- argument 5: [_inst_2 : is_lawful_monad m] -/

-- category/bitraversable/instances.lean
#print bitraversable.traversable /- argument 3: [_inst_3 : is_lawful_bitraversable t] -/
#print const.bitraverse /- argument 2: [_inst_2 : applicative F], argument 8: (f' : β → F β') -/
#print bitraversable.is_lawful_traversable /- argument 3: [_inst_3 : is_lawful_bitraversable t] (duplicate) -/

-- category/basic.lean
#print map_seq /- argument 6: [_inst_2 : is_lawful_applicative F] (duplicate) -/
#print seq_map_assoc /- argument 6: [_inst_2 : is_lawful_applicative F] (duplicate) -/

-- analysis/calculus/times_cont_diff.lean
#print times_cont_diff.times_cont_diff_fderiv_apply /- argument 11: {s : set E} -/

-- algebra/ordered_ring.lean
#print with_top.has_one /- argument 3: [_inst_2 : decidable_eq α] -/
#print with_top.coe_eq_zero /- argument 4: [_inst_3 : partial_order α] -/
#print with_top.zero_ne_top /- argument 4: [_inst_3 : partial_order α] -/
#print with_top.canonically_ordered_comm_semiring /- argument 2: [_inst_1 : canonically_ordered_comm_semiring α] (duplicate), argument 3: [_inst_2 : decidable_eq α] (duplicate) -/
#print with_top.top_ne_zero /- argument 4: [_inst_3 : partial_order α] -/
#print with_top.coe_zero /- argument 4: [_inst_3 : partial_order α] -/

-- algebra/group/with_one.lean
#print with_zero.map_eq /- argument 2: [_inst_1 : add_semigroup α] (duplicate), argument 3: [_inst_3 : add_semigroup α] (duplicate), argument 5: [_inst_4 : add_semigroup β] -/
#print with_zero.lift_coe /- argument 2: [_inst_1 : add_semigroup α] -/
#print with_zero.lift_unique /- argument 2: [_inst_1 : add_semigroup α] -/
#print with_one.lift_unique /- argument 2: [_inst_1 : semigroup α] -/
#print with_one.lift_coe /- argument 2: [_inst_1 : semigroup α] -/
#print with_one.map_eq /- argument 2: [_inst_1 : semigroup α] (duplicate), argument 3: [_inst_3 : semigroup α] (duplicate), argument 5: [_inst_4 : semigroup β] -/
#print with_zero.lift_zero /- argument 2: [_inst_1 : add_semigroup α] -/
#print with_one.lift_one /- argument 2: [_inst_1 : semigroup α] -/

-- algebra/group/units.lean
#print divp_inv /- argument 4: (x : α) (duplicate) -/

-- algebra/floor.lean
#print floor_ring_unique /- argument 3: [_inst_2 : floor_ring α] -/

-- algebra/direct_sum.lean
#print direct_sum /- argument 2: [_inst_1 : decidable_eq ι] -/

-- algebra/direct_limit.lean
#print module.direct_limit.totalize /- argument 12: [_inst_8 : module.directed_system G f] -/
#print module.direct_limit /- argument 12: [_inst_8 : module.directed_system G f] -/
#print ring.direct_limit /- argument 9: [_inst_7 : ∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)], argument 10: [_inst_8 : directed_system G f] -/

-- algebra/big_operators.lean
#print finset.sum_le_sum_of_subset /- argument 8: [_inst_3 : decidable_rel has_le.le] -/
#print finset.sum_eq_zero /- argument 3: [_inst_1 : add_comm_monoid β] (duplicate) -/
#print finset.prod_eq_one /- argument 3: [_inst_1 : comm_monoid β] (duplicate) -/

-- algebra/associated.lean
#print associates.has_dvd /- argument 2: [_inst_1 : comm_monoid α] (duplicate) -/
#print associates.le_of_mul_le_mul_left /- argument 2: [_inst_1 : integral_domain α] (duplicate) -/
#print associates.dvd_eq_le /- argument 2: [_inst_1 : comm_monoid α] (duplicate) -/
#print associates.eq_of_mul_eq_mul_left /- argument 2: [_inst_1 : integral_domain α] (duplicate) -/
#print associates.one_or_eq_of_le_of_prime /- argument 2: [_inst_1 : integral_domain α] (duplicate) -/

-- algebra/archimedean.lean
#print round /- argument 3: [_inst_2 : archimedean α] -/

/- INCORRECT DEF/LEMMA: -/

-- tactic/interactive.lean
#print tactic.interactive.generalize_a_aux /- is a lemma/theorem, should be a def -/

-- tactic/chain.lean
#print tactic.tactic_script.base.inj_eq /- is a def, should be a lemma/theorem -/
#print tactic.tactic_script.pack_1_2.inj /- is a def, should be a lemma/theorem -/
#print tactic.tactic_script.primitive.pack_unpack /- is a def, should be a lemma/theorem -/
#print tactic.tactic_script.work.sizeof_spec /- is a def, should be a lemma/theorem -/
#print tactic.tactic_script.unpack_pack_1_2 /- is a def, should be a lemma/theorem -/
#print tactic.tactic_script.work.inj_eq /- is a def, should be a lemma/theorem -/
#print tactic.tactic_script.primitive.pack.list.nil.spec /- is a def, should be a lemma/theorem -/
#print tactic.tactic_script.sizeof_pack_1_2 /- is a def, should be a lemma/theorem -/
#print tactic.tactic_script.base.inj /- is a def, should be a lemma/theorem -/
#print tactic.tactic_script.base.sizeof_spec /- is a def, should be a lemma/theorem -/
#print tactic.tactic_script.primitive.pack.list.cons.spec /- is a def, should be a lemma/theorem -/
#print tactic.tactic_script.primitive.pack.inj /- is a def, should be a lemma/theorem -/
#print tactic.tactic_script.pack_unpack_1_2 /- is a def, should be a lemma/theorem -/
#print tactic.tactic_script.primitive.unpack_pack /- is a def, should be a lemma/theorem -/
#print tactic.tactic_script.primitive.sizeof_pack /- is a def, should be a lemma/theorem -/
#print tactic.tactic_script.work.inj /- is a def, should be a lemma/theorem -/

-- set_theory/ordinal.lean
#print cardinal.ord_eq_min /- is a def, should be a lemma/theorem -/
#print ordinal.div_def /- is a def, should be a lemma/theorem -/

-- set_theory/lists.lean
#print lists'.subset.nil /- is a def, should be a lemma/theorem -/
#print lists'.subset.cons /- is a def, should be a lemma/theorem -/
#print lists'.subset.rec /- is a def, should be a lemma/theorem -/
#print lists'.subset.cases_on /- is a def, should be a lemma/theorem -/
#print lists.equiv.antisymm /- is a def, should be a lemma/theorem -/
#print lists.equiv.refl /- is a def, should be a lemma/theorem -/
#print lists.equiv.rec /- is a def, should be a lemma/theorem -/
#print lists.equiv.cases_on /- is a def, should be a lemma/theorem -/

-- logic/basic.lean
#print Exists.imp /- is a def, should be a lemma/theorem -/
#print classical.dec_rel /- is a lemma/theorem, should be a def -/
#print classical.dec_eq /- is a lemma/theorem, should be a def -/
#print classical.dec_pred /- is a lemma/theorem, should be a def -/
#print classical.dec /- is a lemma/theorem, should be a def -/

-- data/seq/computation.lean
#print computation.lift_rel_aux.ret_left /- is a def, should be a lemma/theorem -/
#print computation.corec_eq /- is a def, should be a lemma/theorem -/
#print computation.lift_rel_aux.ret_right /- is a def, should be a lemma/theorem -/

-- computability/turing_machine.lean
#print turing.TM2to1.stmt_st_rec /- is a lemma/theorem, should be a def -/

-- category_theory/limits/shapes/equalizers.lean
#print category_theory.limits.fork.condition /- is a def, should be a lemma/theorem -/
#print category_theory.limits.cofork.condition /- is a def, should be a lemma/theorem -/

-- algebra/order_functions.lean
#print abs_add /- is a def, should be a lemma/theorem -/
#print sub_abs_le_abs_sub /- is a def, should be a lemma/theorem -/

/- DUPLICATED NAMESPACES IN NAME: -/

-- topology/uniform_space/separation.lean
#print uniform_space.uniform_space /- The namespace `uniform_space` is duplicated in the name -/

-- topology/metric_space/isometry.lean
#print Kuratowski_embedding.Kuratowski_embedding /- The namespace `Kuratowski_embedding` is duplicated in the name -/

-- topology/category/Top/open_nhds.lean
#print topological_space.open_nhds.open_nhds /- The namespace `open_nhds` is duplicated in the name -/

-- tactic/transfer.lean
#print transfer.transfer /- The namespace `transfer` is duplicated in the name -/

-- tactic/core.lean
#print tactic.tactic.has_to_tactic_format /- The namespace `tactic` is duplicated in the name -/
#print tactic.tactic.use /- The namespace `tactic` is duplicated in the name -/

-- ring_theory/subring.lean
#print is_ring_hom.is_ring_hom /- The namespace `is_ring_hom` is duplicated in the name -/

-- ring_theory/adjoin_root.lean
#print adjoin_root.adjoin_root.has_coe_t /- The namespace `adjoin_root` is duplicated in the name -/

-- order/zorn.lean
#print zorn.zorn /- The namespace `zorn` is duplicated in the name -/

-- order/lattice.lean
#print order_dual.lattice.lattice /- The namespace `lattice` is duplicated in the name -/
#print prod.lattice.lattice /- The namespace `lattice` is duplicated in the name -/
#print lattice.lattice.to_semilattice_sup /- The namespace `lattice` is duplicated in the name -/
#print lattice.lattice.to_semilattice_inf /- The namespace `lattice` is duplicated in the name -/
#print lattice.lattice.ext /- The namespace `lattice` is duplicated in the name -/
#print lattice.lattice /- The namespace `lattice` is duplicated in the name -/

-- order/conditionally_complete_lattice.lean
#print lattice.lattice.has_Sup /- The namespace `lattice` is duplicated in the name -/
#print lattice.lattice.has_Inf /- The namespace `lattice` is duplicated in the name -/
#print lattice.lattice.conditionally_complete_linear_order_bot /- The namespace `lattice` is duplicated in the name -/
#print lattice.lattice.lattice /- The namespace `lattice` is duplicated in the name -/

-- order/complete_boolean_algebra.lean
#print lattice.lattice.bounded_distrib_lattice /- The namespace `lattice` is duplicated in the name -/

-- number_theory/pell.lean
#print pell.pell /- The namespace `pell` is duplicated in the name -/

-- measure_theory/outer_measure.lean
#print measure_theory.outer_measure.outer_measure.order_bot /- The namespace `outer_measure` is duplicated in the name -/

-- measure_theory/lebesgue_measure.lean
#print measure_theory.measure_theory.measure_space /- The namespace `measure_theory` is duplicated in the name -/

-- measure_theory/integration.lean
#print measure_theory.simple_func.lattice.lattice /- The namespace `lattice` is duplicated in the name -/

-- linear_algebra/finite_dimensional.lean
#print finite_dimensional.finite_dimensional /- The namespace `finite_dimensional` is duplicated in the name -/

-- linear_algebra/basic.lean
#print linear_map.linear_map.is_add_group_hom /- The namespace `linear_map` is duplicated in the name -/

-- group_theory/group_action.lean
#print mul_action.mul_action /- The namespace `mul_action` is duplicated in the name -/

-- group_theory/free_group.lean
#print free_group.sum.sum /- The namespace `sum` is duplicated in the name -/

-- data/real/basic.lean
#print real.lattice.lattice /- The namespace `lattice` is duplicated in the name -/

-- data/rat/order.lean
#print rat.lattice.lattice /- The namespace `lattice` is duplicated in the name -/

-- data/opposite.lean
#print opposite.opposite /- The namespace `opposite` is duplicated in the name -/

-- data/multiset.lean
#print multiset.lattice.lattice /- The namespace `lattice` is duplicated in the name -/

-- data/finsupp.lean
#print finsupp.finsupp.decidable_eq /- The namespace `finsupp` is duplicated in the name -/

-- data/finset.lean
#print finset.lattice.lattice /- The namespace `lattice` is duplicated in the name -/

-- category_theory/monad/types.lean
#print category_theory.category_theory.monad /- The namespace `category_theory` is duplicated in the name -/

-- category_theory/isomorphism.lean
#print category_theory.is_iso.is_iso.inv_inv /- The namespace `is_iso` is duplicated in the name -/

-- analysis/complex/exponential.lean
#print real.angle.angle /- The namespace `angle` is duplicated in the name -/
#print real.angle.angle.add_comm_group /- The namespace `angle` is duplicated in the name -/
#print real.angle.angle.is_add_group_hom /- The namespace `angle` is duplicated in the name -/
#print real.angle.angle.has_coe /- The namespace `angle` is duplicated in the name -/

-- algebra/ordered_group.lean
#print with_zero.lattice.lattice /- The namespace `lattice` is duplicated in the name -/