mathlib_high_scores

mathlib_high_scores

#### SIZE (GARBAGE LEAN OBJECTS)
10794778 : polynomial.monic.next_coeff_mul 
1090313 : composition_as_set_equiv._proof_5 
662922 : real.pi_lt_3141593 
468943 : real.pi_gt_3141592 
413365 : real.pi_lt_31416 
342992 : sum_range_choose_halfway 
315037 : _private.4086404821.sum_four_squares_of_two_mul_sum_four_squares 
263176 : polynomial.irreducible_of_eisenstein_criterion 
228696 : AddCommGroup.kernel_iso_ker_over._proof_4 
227551 : composition_as_set_equiv._proof_6 
226028 : exp_neg_inv_glue.f_aux_deriv 
225619 : AddCommGroup.kernel_iso_ker_over._proof_3 
225117 : continuous_equiv_fun_basis 
184318 : multilinear_map.map_sum_finset_aux 
183416 : real.pi_gt_31415 
174309 : Gromov_Hausdorff.totally_bounded 
162194 : string.iterator.curr._main.equations._eqn_1 
159787 : composition_as_set_equiv._proof_2 
155768 : free_abelian_group.is_lawful_monad.equations._eqn_1 
155751 : free_abelian_group.is_lawful_monad 
153638 : category_theory.nat_trans.on_presheaf._proof_1 
149583 : Module.monoidal_category.pentagon 
143370 : category_theory.limits.prod_functor._proof_9 
138277 : Top.CommRing_yoneda._proof_8 
135271 : _private.433596857.prime_sum_four_squares 
127140 : lift_of_splits 
122671 : algebraic_geometry.PresheafedSpace.stalk_map.comp 
122095 : polynomial.coeff_comp_degree_mul_degree 
119313 : free_group.is_lawful_monad.equations._eqn_1 
119296 : free_group.is_lawful_monad 
110915 : CommRing.category_theory.creates_limit.equations._eqn_1 
110883 : CommRing.category_theory.creates_limit 
109156 : list.is_lawful_monad.equations._eqn_1 
109139 : list.is_lawful_monad 
106545 : _private.3149472077.glue_dist_triangle 
106049 : formal_multilinear_series.comp_summable_nnreal 
105882 : times_cont_mdiff_on.times_cont_mdiff_on_tangent_map_within_aux 
105228 : measure_theory.simple_func_sequence_tendsto 
103917 : basic_smooth_bundle_core.to_smooth_manifold.equations._eqn_1 
103862 : basic_smooth_bundle_core.to_smooth_manifold 
102778 : Gromov_Hausdorff.complete_space.equations._eqn_1 
102777 : gaussian_int.prime_of_nat_prime_of_mod_four_eq_three 
102761 : Gromov_Hausdorff.complete_space 
101996 : has_fpower_series_at.comp 
101877 : real.pi_gt_314 
101616 : Module.monoidal_category.associator_naturality 
101475 : CommRing.category_theory.creates_limit._proof_10 
100051 : AddCommGroup.kernel_iso_ker._proof_6 
99331 : real.sin_bound 
99085 : measure_theory.hahn_decomposition 
98735 : complex.exists_root 
98406 : times_cont_mdiff_on.times_cont_mdiff_on_tangent_map_within 
98058 : category_theory.monoidal.Mon_functor_category_equivalence.functor._proof_42 
97954 : category_theory.monoidal.Mon_functor_category_equivalence.functor._proof_44 
96955 : real.exists_sup 
96492 : ring.direct_limit.of.zero_exact_aux 
95623 : filter.is_lawful_monad 
94929 : Gromov_Hausdorff.second_countable.equations._eqn_1 
94912 : Gromov_Hausdorff.second_countable 
94452 : set.is_lawful_monad.equations._eqn_1 
94435 : set.is_lawful_monad 
94385 : category_theory.functor.map_presheaf._proof_2 
93352 : Module.monoidal_category.triangle 
93068 : exists_approx_preimage_norm_le 
92918 : real.cos_bound 
92117 : Top.CommRing_yoneda.equations._eqn_1 
92097 : Top.CommRing_yoneda 
92068 : AddCommGroup.kernel_iso_ker_inv_comp_ι 
91835 : _private.217157525.is_st_mul' 
91611 : primorial_le_4_pow 
89980 : has_ftaylor_series_up_to_on_succ_iff_right 
89586 : norm_eq_infi_iff_inner_le_zero 
89526 : is_bounded_linear_map_prod_multilinear 
89465 : pythagorean_triple.is_primitive_classified_of_coprime_of_odd_of_pos 
88440 : _private.1179974605.make_monospaced._main.equations._eqn_3 
88374 : _private.1179974605.make_monospaced._main.equations._eqn_2 
88246 : _private.1179974605.make_monospaced._main.equations._eqn_1 
87963 : gaussian_int.euclidean_domain._proof_1 
87247 : real.continuous_rpow_aux3 
86417 : real.pi_lt_315 
86056 : Top.presheaf.stalk_pushforward.comp 
85927 : Icc_smooth_manifold.equations._eqn_1 
85898 : Icc_smooth_manifold 
85580 : semiquot.is_lawful_monad.equations._eqn_1 
85563 : semiquot.is_lawful_monad 
85387 : exists_norm_eq_infi_of_complete_convex 
85127 : normed_field.tendsto_inv 
84453 : is_bounded_bilinear_map_comp_multilinear 
84254 : linear_map.continuous_iff_is_closed_ker 
84245 : inner_product_geometry.angle_add_angle_sub_add_angle_sub_eq_pi 
83918 : category_theory.monoidal.Mon_functor_category_equivalence.functor._proof_43 
82885 : half_le_harmonic_double_sub_harmonic 
82589 : formal_multilinear_series.change_origin_radius 
82247 : dense_Inter_of_open_nat 
81360 : has_ftaylor_series_up_to_on.prod 
80199 : real.abs_log_sub_add_sum_range_le 
80135 : category_theory.limits.cocones.whiskering_equivalence._proof_5 
79468 : formal_multilinear_series.bound_of_lt_radius 
78647 : is_noetherian_pi.equations._eqn_1 
78600 : is_noetherian_pi 


#### TIME (MILLISECONDS)
7584 : polynomial.monic.next_coeff_mul 
684 : composition_as_set_equiv._proof_5 
353 : Gromov_Hausdorff.totally_bounded 
346 : real.pi_lt_3141593 
233 : real.pi_gt_3141592 
213 : real.pi_lt_31416 
204 : _private.4086404821.sum_four_squares_of_two_mul_sum_four_squares 
190 : sum_range_choose_halfway 
183 : real.exists_sup 
179 : lift_of_splits 
174 : AddCommGroup.kernel_iso_ker_over._proof_4 
172 : pythagorean_triple.is_primitive_classified_of_coprime_of_odd_of_pos 
171 : AddCommGroup.kernel_iso_ker_over._proof_3 
165 : polynomial.irreducible_of_eisenstein_criterion 
161 : continuous_equiv_fun_basis 
153 : exists_approx_preimage_norm_le 
153 : _private.217157525.is_st_mul' 
150 : cauchy_product 
146 : exp_neg_inv_glue.f_aux_deriv 
143 : norm_eq_infi_iff_inner_le_zero 
136 : complex.sum_div_fact_le 
135 : real.continuous_rpow_aux3 
132 : normed_field.tendsto_inv 
131 : hofer 
129 : real.pi_lt_sqrt_two_add_series 
128 : Gromov_Hausdorff.second_countable.equations._eqn_1 
128 : Gromov_Hausdorff.second_countable 
124 : _private.433596857.prime_sum_four_squares 
124 : real.sin_bound 
122 : complex.exists_root 
122 : measure_theory.hahn_decomposition 
121 : discriminant_le_zero 
120 : linear_map.continuous_iff_is_closed_ker 
119 : composition_as_set_equiv._proof_6 
116 : half_le_harmonic_double_sub_harmonic 
115 : category_theory.limits.prod_functor._proof_9 
115 : real.cos_bound 
112 : free_abelian_group.is_lawful_monad 
112 : real.abs_log_sub_add_sum_range_le 
111 : normed_ring.inverse_one_sub_norm 
111 : real.sin_pos_of_pos_of_le_one 
111 : exists_norm_eq_infi_of_complete_convex 
110 : free_abelian_group.is_lawful_monad.equations._eqn_1 
109 : formal_multilinear_series.comp_summable_nnreal 
107 : real.sqrt_exists 
107 : real.pi_gt_31415 
105 : measure_theory.simple_func_sequence_tendsto 
105 : _private.3149472077.glue_dist_triangle 
104 : category_theory.monoidal.Mon_functor_category_equivalence.functor._proof_44 
100 : subset_tangent_cone_prod_right 
100 : subset_tangent_cone_prod_left 
100 : real.cos_pi_over_two_pow 
98 : exists_preimage_norm_le 
96 : multilinear_map.exists_bound_of_continuous 
94 : category_theory.nat_trans.on_presheaf._proof_1 
94 : multilinear_map.map_sum_finset_aux 
93 : isometric.midpoint_fixed 
93 : algebraic_geometry.PresheafedSpace.stalk_map.comp 
92 : convex_on_real_of_slope_mono_adjacent 
92 : real.sin_gt_sub_cube 
91 : real.cos_pos_of_le_one 
91 : hyperreal.is_st_neg 
89 : exists_rat_btwn 
89 : category_theory.monoidal.Mon_functor_category_equivalence.functor._proof_42 
88 : continuous_multilinear_map.continuous_eval 
88 : mem_tangent_cone_of_segment_subset 
88 : self_div_two_le_harmonic_two_pow 
87 : Gromov_Hausdorff.complete_space.equations._eqn_1 
86 : has_fpower_series_at.comp 
86 : fpow_strict_mono 
86 : Gromov_Hausdorff.complete_space 
85 : hyperreal.infinite_pos_mul_of_infinite_pos_not_infinitesimal_pos 
85 : Icc_smooth_manifold.equations._eqn_1 
85 : rescale_to_shell 
84 : Icc_smooth_manifold 
84 : mem_pos_tangent_cone_at_of_segment_subset 
84 : category_theory.monoidal.Mon_functor_category_equivalence.functor._proof_43 
83 : real.sin_lt 
82 : real.cos_lt_cos_of_nonneg_of_le_pi 
82 : real.cos_lt_cos_of_nonneg_of_le_pi_div_two 
82 : gaussian_int.norm_sq_div_sub_div_lt_one 
81 : complex.is_cau_abs_exp 
81 : inner_product_geometry.angle_add_angle_sub_add_angle_sub_eq_pi 
80 : free_group.is_lawful_monad.equations._eqn_1 
80 : formal_multilinear_series.change_origin_radius 
80 : Top.CommRing_yoneda._proof_8 
79 : riesz_extension.step 
79 : riesz_lemma 
79 : free_group.is_lawful_monad 
79 : CommRing.category_theory.creates_limit 
78 : CommRing.category_theory.creates_limit.equations._eqn_1 
78 : primorial_le_4_pow 
78 : complex.abs_exp_sub_one_sub_id_le 
77 : basic_smooth_bundle_core.to_smooth_manifold.equations._eqn_1 
77 : complex.cpow_nat_inv_pow 
77 : is_cau_geo_series 
76 : abs_sub_round 
75 : sum_bernoulli 
75 : hyperreal.is_st_add 
75 : basic_smooth_bundle_core.to_smooth_manifold