profile per decl 2020-05-13

38.0 src/number_theory/sum_four_squares.lean
27.8 src/topology/metric_space/completion.lean
26.2 src/topology/category/Top/adjunctions.lean
26.15 src/algebra/category/Group/biproducts.lean
23.0 src/category_theory/products/basic.lean
22.666666666666668 src/data/padics/hensel.lean
22.2 src/category_theory/limits/shapes/constructions/limits_of_products_and_equalizers.lean
22.1 src/analysis/normed_space/hahn_banach.lean
16.7 src/topology/category/TopCommRing.lean
16.54 src/category_theory/elements.lean
15.7 src/measure_theory/simple_func_dense.lean
14.95 src/category_theory/limits/functor_category.lean
14.9 src/category_theory/monad/algebra.lean
14.75 src/data/zsqrtd/basic.lean
12.971428571428572 src/data/matrix/notation.lean
12.725 src/analysis/calculus/extend_deriv.lean
12.4 src/category_theory/limits/over.lean
12.363636363636363 src/geometry/manifold/basic_smooth_bundle.lean
11.95 src/analysis/complex/polynomial.lean
11.7 src/analysis/complex/basic.lean
11.6125 src/category_theory/limits/shapes/wide_pullbacks.lean
10.84 src/topology/category/UniformSpace.lean
10.6 src/measure_theory/decomposition.lean
10.6 src/algebraic_geometry/stalks.lean
10.25 src/topology/metric_space/cau_seq_filter.lean
9.675 src/number_theory/pell.lean
9.42 src/analysis/normed_space/banach.lean
9.233333333333333 src/category_theory/monad/adjunction.lean
9.0625 src/category_theory/limits/shapes/binary_products.lean
8.725 src/category_theory/currying.lean
8.65 archive/imo1988_q6.lean
7.7272727272727275 src/measure_theory/outer_measure.lean
7.266666666666667 src/category_theory/graded_object.lean
7.0 src/category_theory/pempty.lean
6.914285714285714 src/category_theory/adjunction/limits.lean
6.9 src/analysis/normed_space/riesz_lemma.lean
6.8999999999999995 src/linear_algebra/determinant.lean
6.825 src/analysis/normed_space/mazur_ulam.lean
6.75 src/algebra/category/Group/adjunctions.lean
6.7368421052631575 src/topology/metric_space/gromov_hausdorff.lean
6.7 src/linear_algebra/linear_action.lean
6.588235294117647 src/category_theory/comma.lean
6.366666666666666 src/geometry/manifold/real_instances.lean
6.24 src/analysis/normed_space/real_inner_product.lean
6.116666666666666 src/analysis/special_functions/pow.lean
6.042553191489362 src/analysis/normed_space/multilinear.lean
5.966666666666666 src/number_theory/bernoulli.lean
5.8 src/number_theory/quadratic_reciprocity.lean
5.675 src/data/int/parity.lean
5.55 src/category_theory/products/associator.lean
5.542857142857143 src/analysis/analytic/composition.lean
5.428571428571429 src/data/padics/padic_integers.lean
5.275 src/category_theory/limits/shapes/constructions/pullbacks.lean
5.25 src/measure_theory/lebesgue_measure.lean
5.15 src/ring_theory/integral_domain.lean
5.05 src/topology/algebra/polynomial.lean
4.904999999999999 src/data/zsqrtd/gaussian_int.lean
4.84 src/ring_theory/principal_ideal_domain.lean
4.7924528301886795 src/data/dfinsupp.lean
4.791666666666667 src/data/padics/padic_norm.lean
4.75 src/topology/metric_space/premetric_space.lean
4.7125 src/algebra/category/Module/basic.lean
4.666666666666667 src/topology/sheaves/presheaf.lean
4.64 src/topology/metric_space/gromov_hausdorff_realized.lean
4.625 src/category_theory/limits/connected.lean
4.553333333333333 src/algebra/homology/homology.lean
4.521739130434782 src/linear_algebra/multilinear.lean
4.5 src/topology/metric_space/hausdorff_distance.lean
4.493333333333334 src/algebra/category/Module/monoidal.lean
4.49 src/order/complete_boolean_algebra.lean
4.455 src/category_theory/limits/shapes/products.lean
4.45 src/category_theory/differential_object.lean
4.45 src/algebraic_geometry/presheafed_space.lean
4.4 src/category_theory/yoneda.lean
4.36 src/order/lexicographic.lean
4.22 src/analysis/analytic/basic.lean
4.211111111111111 src/analysis/normed_space/finite_dimension.lean
4.2 src/topology/category/Top/opens.lean
4.19 src/data/pnat/intervals.lean
4.133333333333334 src/topology/sheaves/presheaf_of_functions.lean
4.133333333333334 src/category_theory/const.lean
4.038461538461538 archive/sensitivity.lean
4.0 src/analysis/calculus/specific_functions.lean
3.9799999999999995 src/control/traversable/instances.lean
3.8444444444444446 src/algebra/category/CommRing/colimits.lean
3.84 src/data/finsupp/pointwise.lean
3.8363636363636364 src/data/padics/padic_numbers.lean
3.8249999999999997 src/linear_algebra/quadratic_form.lean
3.811111111111111 src/category_theory/monad/limits.lean
3.75 src/data/real/cardinality.lean
3.6999999999999997 src/topology/metric_space/closeds.lean
3.6 src/topology/sheaves/stalks.lean
3.6 src/algebra/category/CommRing/basic.lean
3.5749999999999997 src/field_theory/splitting_field.lean
3.5666666666666664 src/category_theory/sums/associator.lean
3.5666666666666664 src/algebra/category/Group/limits.lean
3.5500000000000003 src/category_theory/monoidal/of_has_finite_products.lean
3.55 src/measure_theory/probability_mass_function.lean
3.5 src/topology/algebra/uniform_ring.lean
3.485 src/algebra/category/CommRing/adjunctions.lean
3.466666666666667 src/data/rat/cast.lean
3.466666666666667 src/algebra/category/CommRing/limits.lean
3.435 src/category_theory/limits/shapes/terminal.lean
3.38 src/number_theory/sum_two_squares.lean
3.35 test/ring_exp.lean
3.32 src/category_theory/hom_functor.lean
3.310344827586207 src/data/complex/basic.lean
3.2399999999999998 src/algebra/classical_lie_algebras.lean
3.2222222222222223 src/data/analysis/filter.lean
3.2 src/data/matrix/basic.lean
3.1999999999999997 src/analysis/convex/specific_functions.lean
3.1842105263157894 src/analysis/normed_space/bounded_linear_maps.lean
3.156 src/algebra/lie_algebra.lean
3.1545454545454548 src/field_theory/finite.lean
3.1500000000000004 src/analysis/calculus/iterated_deriv.lean
3.130434782608696 src/ring_theory/localization.lean
3.1285714285714286 src/field_theory/minimal_polynomial.lean
3.12 src/category_theory/whiskering.lean
3.09 src/data/matrix/pequiv.lean
3.075 src/category_theory/limits/cones.lean
3.042452830188679 src/analysis/special_functions/trigonometric.lean
3.04 src/category_theory/limits/shapes/constructions/equalizers.lean
3.0375 src/ring_theory/adjoin_root.lean
2.9444444444444446 src/data/monoid_algebra.lean
2.7875 src/category_theory/limits/shapes/images.lean
2.784375 src/category_theory/limits/shapes/pullbacks.lean
2.7222222222222223 src/algebra/category/Group/colimits.lean
2.716 src/topology/metric_space/gluing.lean
2.7 test/transport/basic.lean
2.676470588235294 src/computability/partrec_code.lean
2.65 src/category_theory/category/Groupoid.lean
2.636842105263158 src/algebra/category/Group/basic.lean
2.609677419354839 src/data/real/pi.lean
2.525 src/category_theory/limits/types.lean
2.523076923076923 src/data/analysis/topology.lean
2.5121951219512195 src/linear_algebra/finsupp.lean
2.479338842975207 src/data/mv_polynomial.lean
2.46 src/order/pilex.lean
2.46 src/linear_algebra/matrix.lean
2.45 src/tactic/norm_cast.lean
2.445 src/data/lazy_list2.lean
2.41 src/category_theory/monoidal/functorial.lean
2.408333333333333 src/ring_theory/unique_factorization_domain.lean
2.405 src/data/real/ereal.lean
2.392857142857143 src/algebra/category/Mon/basic.lean
2.3777777777777778 src/algebra/category/Mon/colimits.lean
2.316666666666667 src/data/fin_enum.lean
2.31 src/category_theory/reflect_isomorphisms.lean
2.295 src/data/list/bag_inter.lean
2.275 src/set_theory/game/short.lean
2.2733333333333334 src/category_theory/limits/shapes/strong_epi.lean
2.2529411764705882 src/topology/bounded_continuous_function.lean
2.25 src/topology/category/Top/open_nhds.lean
2.24 src/category_theory/category/Rel.lean
2.2333333333333334 src/topology/uniform_space/absolute_value.lean
2.2083333333333335 src/linear_algebra/basis.lean
2.1894736842105265 src/ring_theory/power_series.lean
2.188679245283019 src/topology/instances/ennreal.lean
2.18 src/topology/algebra/group_completion.lean
2.18 src/tactic/omega/nat/main.lean
2.1666666666666665 src/ring_theory/fractional_ideal.lean
2.15 src/tactic/core.lean
2.125 src/ring_theory/euclidean_domain.lean
2.1100000000000003 src/measure_theory/giry_monad.lean
2.1 src/category_theory/single_obj.lean
2.1 src/category_theory/discrete_category.lean
2.095652173913044 src/topology/topological_fiber_bundle.lean
2.079295154185022 src/data/polynomial.lean
2.045977011494253 src/analysis/normed_space/basic.lean
2.0444444444444443 src/group_theory/free_abelian_group.lean
2.02 src/category_theory/sums/basic.lean
2.02 src/analysis/calculus/darboux.lean
2.01 src/geometry/manifold/smooth_manifold_with_corners.lean
2.01 src/category_theory/monoidal/functor.lean
1.9925 src/category_theory/limits/shapes/regular_mono.lean
1.9857142857142858 src/data/nat/parity.lean
1.94 src/algebra/quadratic_discriminant.lean
1.9166666666666667 src/category_theory/limits/shapes/biproducts.lean
1.8571428571428572 src/category_theory/adjunction/basic.lean
1.8517241379310345 src/topology/algebra/uniform_group.lean
1.8484848484848484 src/measure_theory/integration.lean
1.8141592920353982 src/analysis/calculus/times_cont_diff.lean
1.791304347826087 src/data/fintype/card.lean
1.7791666666666668 src/ring_theory/polynomial.lean
1.778 src/analysis/normed_space/operator_norm.lean
1.7625 src/category_theory/limits/shapes/zero.lean
1.7593984962406015 src/geometry/manifold/mfderiv.lean
1.75 src/data/nat/multiplicity.lean
1.732394366197183 src/combinatorics/composition.lean
1.7275 src/category_theory/limits/preserves.lean
1.7156862745098038 src/topology/algebra/module.lean
1.7113636363636362 src/set_theory/cofinality.lean
1.6772727272727272 src/ring_theory/integral_closure.lean
1.671641791044776 src/group_theory/perm/sign.lean
1.6666666666666667 src/algebra/direct_limit.lean
1.6375 src/linear_algebra/linear_pmap.lean
1.6357142857142857 src/topology/algebra/multilinear.lean
1.625 src/topology/instances/nnreal.lean
1.6189189189189188 src/data/rat/basic.lean
1.6176470588235294 src/data/complex/exponential.lean
1.6142857142857143 src/ring_theory/noetherian.lean
1.6108695652173912 src/analysis/special_functions/exp_log.lean
1.59 src/data/string/basic.lean
1.5862068965517242 src/topology/algebra/infinite_sum.lean
1.585 src/tactic/monotonicity/interactive.lean
1.5833333333333333 src/category_theory/limits/shapes/equalizers.lean
1.58 src/tactic/omega/int/main.lean
1.58 src/category_theory/opposites.lean
1.5666666666666667 src/group_theory/sylow.lean
1.5588235294117647 src/topology/metric_space/baire.lean
1.535 src/data/buffer/basic.lean
1.5250000000000001 src/topology/uniform_space/separation.lean
1.5075 src/data/nat/totient.lean
1.455 src/data/equiv/transfer_instance.lean
1.4534883720930232 src/linear_algebra/tensor_product.lean
1.4533333333333334 src/geometry/manifold/manifold.lean
1.453125 src/data/pequiv.lean
1.4444444444444444 src/set_theory/ordinal_notation.lean
1.4306569343065694 src/data/finsupp.lean
1.4285714285714286 src/analysis/calculus/local_extr.lean
1.4263157894736842 src/group_theory/order_of_element.lean
1.426 src/data/set/enumerate.lean
1.4181818181818182 src/analysis/mean_inequalities.lean
1.4172413793103449 src/order/filter/filter_product.lean
1.41 src/data/rat/order.lean
1.3925925925925926 src/algebra/pi_instances.lean
1.392 src/category_theory/core.lean
1.3255813953488371 src/category_theory/limits/limits.lean
1.3169014084507042 src/data/real/ennreal.lean
1.3 src/algebra/continued_fractions/convergents_equiv.lean
1.3 archive/cubing_a_cube.lean
1.2946859903381642 src/linear_algebra/basic.lean
1.29 src/data/dlist/instances.lean
1.28 src/algebra/group/conj.lean
1.2733333333333332 src/data/finmap.lean
1.2684210526315791 src/analysis/calculus/tangent_cone.lean
1.263157894736842 src/data/equiv/denumerable.lean
1.2470588235294118 src/data/holor.lean
1.2392156862745098 src/data/real/basic.lean
1.2166666666666666 src/algebraic_geometry/prime_spectrum.lean
1.2114285714285713 src/topology/algebra/group.lean
1.2 src/ring_theory/multiplicity.lean
1.19 src/linear_algebra/special_linear_group.lean
1.180952380952381 src/measure_theory/ae_eq_fun.lean
1.1758620689655173 src/linear_algebra/nonsingular_inverse.lean
1.175 src/control/bitraversable/instances.lean
1.1452830188679246 src/data/real/nnreal.lean
1.1416666666666666 src/linear_algebra/finite_dimensional.lean
1.12 src/tactic/interactive.lean
1.1166666666666667 src/data/vector2.lean
1.1159999999999999 src/group_theory/coset.lean
1.11375 src/algebra/direct_sum.lean
1.1116666666666666 src/algebra/category/Group/images.lean
1.1 src/data/int/gcd.lean
1.0966666666666667 src/linear_algebra/dual.lean
1.09 src/tactic/suggest.lean
1.0727272727272728 src/topology/algebra/open_subgroup.lean
1.0699999999999998 src/data/list/rotate.lean
1.05 src/analysis/normed_space/point_reflection.lean
1.0485436893203883 src/measure_theory/measure_space.lean
1.0480349344978166 src/analysis/calculus/deriv.lean
1.0475 src/topology/algebra/ring.lean
1.0277777777777777 src/topology/compact_open.lean
1.0226190476190478 src/data/fintype/basic.lean
0.995 src/category_theory/concrete_category/bundled_hom.lean
0.9846153846153847 src/algebra/field_power.lean
0.9740740740740741 src/group_theory/monoid_localization.lean
0.9633333333333333 src/analysis/calculus/inverse.lean
0.95 src/tactic/monotonicity/basic.lean
0.9455445544554455 src/data/multiset.lean
0.9411764705882353 src/topology/algebra/monoid.lean
0.9214285714285715 src/data/seq/parallel.lean
0.9199999999999999 archive/examples/prop_encodable.lean
0.9186046511627907 src/analysis/calculus/mean_value.lean
0.9172413793103449 src/data/real/cau_seq_completion.lean
0.9024390243902439 src/topology/instances/real.lean
0.9 src/category_theory/monoidal/category.lean
0.888235294117647 src/order/filter/partial.lean
0.8827160493827161 src/topology/metric_space/emetric_space.lean
0.8761904761904762 src/algebra/module.lean
0.87 src/measure_theory/category/Meas.lean
0.8647058823529412 src/topology/metric_space/basic.lean
0.8645454545454545 src/topology/metric_space/lipschitz.lean
0.8566666666666667 src/computability/halting.lean
0.852 src/linear_algebra/bilinear_form.lean
0.8450000000000001 src/category_theory/functor_category.lean
0.84375 src/algebra/invertible.lean
0.8429906542056075 src/topology/subset_properties.lean
0.8372549019607843 src/number_theory/dioph.lean
0.8338709677419355 src/analysis/specific_limits.lean
0.8304347826086957 src/data/indicator_function.lean
0.8240000000000001 src/tactic/ring2.lean
0.824 src/algebra/big_operators.lean
0.8157894736842105 src/ring_theory/algebra_operations.lean
0.8153846153846154 src/analysis/convex/topology.lean
0.8078947368421052 src/topology/metric_space/isometry.lean
0.8076923076923077 src/data/set/countable.lean
0.79375 src/set_theory/game/domineering.lean
0.7909090909090909 src/field_theory/mv_polynomial.lean
0.7833333333333333 src/algebra/geom_sum.lean
0.7772727272727273 src/data/zmod/basic.lean
0.7766666666666667 src/category_theory/groupoid.lean
0.7765217391304348 src/analysis/convex/basic.lean
0.775 src/set_theory/schroeder_bernstein.lean
0.7666666666666667 src/category_theory/equivalence.lean
0.766 src/data/nat/choose.lean
0.7633333333333333 src/data/equiv/nat.lean
0.7608333333333334 src/category_theory/natural_isomorphism.lean
0.76 src/ring_theory/ideals.lean
0.7523809523809524 src/topology/separation.lean
0.7483870967741936 src/data/equiv/list.lean
0.748 src/data/list/sigma.lean
0.746774193548387 src/data/seq/seq.lean
0.7458333333333332 src/data/list/sort.lean
0.74125 src/category_theory/eq_to_hom.lean
0.7346153846153847 src/analysis/convex/cone.lean
0.729 src/data/nat/pairing.lean
0.7282051282051282 src/algebra/floor.lean
0.7258064516129032 src/tactic/linarith.lean
0.7162162162162162 src/group_theory/free_group.lean
0.7151162790697675 src/topology/algebra/ordered.lean
0.7086956521739131 src/tactic/ring.lean
0.7000000000000001 src/data/array/lemmas.lean
0.6991666666666667 src/topology/opens.lean
0.6991071428571428 src/topology/uniform_space/basic.lean
0.6984615384615385 src/data/set/disjointed.lean
0.6875 test/equiv_rw.lean
0.6799999999999999 src/algebra/gcd_domain.lean
0.6793650793650793 src/data/seq/wseq.lean
0.6764285714285715 src/topology/metric_space/antilipschitz.lean
0.6736842105263158 src/category_theory/limits/shapes/kernels.lean
0.6730769230769231 src/data/real/cau_seq.lean
0.6666666666666666 src/analysis/calculus/fderiv.lean
0.6658333333333334 test/monotonicity.lean
0.665 src/topology/list.lean
0.6575757575757576 src/topology/uniform_space/uniform_embedding.lean
0.645 src/data/list/antidiagonal.lean
0.6419354838709677 src/topology/uniform_space/uniform_convergence.lean
0.6410852713178294 src/data/int/basic.lean
0.6392156862745099 src/order/lattice.lean
0.6385542168674698 src/computability/turing_machine.lean
0.6321428571428571 src/group_theory/subgroup.lean
0.6166666666666667 src/topology/bases.lean
0.616551724137931 src/set_theory/cardinal.lean
0.6102941176470589 src/data/set/finite.lean
0.6096774193548387 src/data/fin.lean
0.6056603773584905 src/data/hash_map.lean
0.6000000000000001 src/data/list/min_max.lean
0.5966850828729282 src/data/finset.lean
0.5964285714285714 src/measure_theory/borel_space.lean
0.5927083333333333 src/measure_theory/bochner_integration.lean
0.59 src/group_theory/abelianization.lean
0.587 src/linear_algebra/finsupp_vector_space.lean
0.5648648648648649 src/algebra/ring.lean
0.5623529411764706 src/order/filter/pointwise.lean
0.5570588235294118 src/group_theory/perm/cycles.lean
0.5565217391304348 src/data/nat/enat.lean
0.5543859649122808 src/ring_theory/algebra.lean
0.55 src/data/nat/cast.lean
0.5481818181818182 docs/tutorial/Zmod37.lean
0.545 src/data/nat/fib.lean
0.5333333333333333 src/data/int/modeq.lean
0.5294444444444444 src/data/list/intervals.lean
0.5231707317073171 src/algebra/associated.lean
0.5109375 src/topology/local_homeomorph.lean
0.5 src/order/copy.lean
0.495 src/category_theory/quotient.lean
0.49400000000000005 src/algebra/continued_fractions/continuants_recurrence.lean
0.49175257731958766 src/computability/partrec.lean
0.4846153846153846 src/order/order_iso.lean
0.4842857142857143 src/data/equiv/fin.lean
0.48392857142857143 src/order/liminf_limsup.lean
0.481 src/category_theory/fully_faithful.lean
0.48000000000000004 src/ring_theory/free_comm_ring.lean
0.46923076923076923 src/set_theory/lists.lean
0.4681818181818182 src/algebra/archimedean.lean
0.4636363636363636 src/measure_theory/set_integral.lean
0.46111111111111114 src/data/nat/modeq.lean
0.4575 src/field_theory/subfield.lean
0.4566666666666667 src/topology/uniform_space/compare_reals.lean
0.452 src/tactic/abel.lean
0.45 src/control/monad/writer.lean
0.4473684210526316 src/category_theory/types.lean
0.44027777777777777 src/measure_theory/l1_space.lean
0.44 src/topology/category/Top/limits.lean
0.4302816901408451 src/data/real/hyperreal.lean
0.42875 src/ring_theory/algebraic.lean
0.42857142857142855 src/algebra/pointwise.lean
0.42642857142857143 src/category_theory/connected.lean
0.4255813953488372 src/linear_algebra/dimension.lean
0.425531914893617 src/tactic/ring_exp.lean
0.425 src/set_theory/game/state.lean
0.4150442477876106 src/measure_theory/measurable_space.lean
0.4105263157894737 src/data/equiv/encodable.lean
0.409375 src/algebra/euclidean_domain.lean
0.4011111111111111 src/topology/instances/complex.lean
0.4 src/topology/uniform_space/cauchy.lean
0.39916666666666667 src/group_theory/quotient_group.lean
0.396875 src/data/list/alist.lean
0.39571428571428574 src/topology/sequences.lean
0.395 src/category_theory/isomorphism_classes.lean
0.3875 test/finish4.lean
0.3836734693877551 src/topology/uniform_space/completion.lean
0.3806451612903226 src/topology/dense_embedding.lean
0.37857142857142856 src/group_theory/group_action.lean
0.37730769230769234 src/field_theory/perfect_closure.lean
0.375 src/control/applicative.lean
0.37254901960784315 src/order/conditionally_complete_lattice.lean
0.3666666666666667 src/topology/constructions.lean
0.36585365853658536 src/data/set/intervals/basic.lean
0.3647058823529412 src/algebra/char_p.lean
0.3646153846153846 src/order/filter/bases.lean
0.36333333333333334 src/category_theory/full_subcategory.lean
0.358 src/category_theory/epi_mono.lean
0.35571428571428576 src/category_theory/limits/creates.lean
0.35107913669064744 src/data/set/lattice.lean
0.3510204081632653 src/data/nat/prime.lean
0.3465 src/tactic/omega/eq_elim.lean
0.34375 src/ring_theory/adjoin.lean
0.3422222222222222 src/tactic/omega/coeffs.lean
0.341 src/data/fp/basic.lean
0.33999999999999997 src/category_theory/endomorphism.lean
0.33314606741573033 src/computability/primrec.lean
0.33166666666666667 src/linear_algebra/sesquilinear_form.lean
0.33015873015873015 src/algebra/ordered_ring.lean
0.328695652173913 src/algebra/free.lean
0.32652173913043475 src/data/list/func.lean
0.32426229508196724 src/order/filter/basic.lean
0.32 src/data/list/of_fn.lean
0.31511627906976747 src/set_theory/pgame.lean
0.3143333333333333 src/data/real/irrational.lean
0.3125 src/data/pfun.lean
0.31136363636363634 src/data/nat/sqrt.lean
0.3109090909090909 src/measure_theory/indicator_function.lean
0.3091304347826087 src/algebra/continued_fractions/translations.lean
0.30428571428571427 src/category_theory/isomorphism.lean
0.3 src/topology/metric_space/contracting.lean
0.2885093167701864 src/data/set/basic.lean
0.2826086956521739 src/topology/maps.lean
0.27875 src/algebra/group_ring_action.lean
0.27435897435897433 src/data/equiv/local_equiv.lean
0.27166666666666667 src/algebra/group/with_one.lean
0.2709401709401709 src/data/list/perm.lean
0.2693181818181818 src/topology/continuous_on.lean
0.267 src/category_theory/conj.lean
0.2647058823529412 src/data/support.lean
0.26375 src/control/bifunctor.lean
0.26272727272727275 src/ring_theory/subring.lean
0.25820568927789933 src/data/list/basic.lean
0.25319148936170216 src/data/pnat/factors.lean
0.2519230769230769 src/algebra/order_functions.lean
0.2516 src/data/semiquot.lean
0.25105263157894736 src/data/nat/basic.lean
0.25 src/data/rel.lean
0.24625 src/data/list/tfae.lean
0.24603174603174602 src/topology/basic.lean
0.24333333333333332 src/meta/expr.lean
0.2414285714285714 src/data/equiv/ring.lean
0.236 src/algebra/group/units.lean
0.23500000000000001 src/order/zorn.lean
0.23247422680412372 src/set_theory/ordinal.lean
0.226875 src/analysis/ODE/gronwall.lean
0.22666666666666668 src/category_theory/category/default.lean
0.22375 src/data/list/zip.lean
0.22294117647058823 src/logic/embedding.lean
0.22285714285714284 src/topology/stone_cech.lean
0.22125 src/control/bitraversable/lemmas.lean
0.21982758620689655 src/tactic/norm_num.lean
0.21705426356589147 src/group_theory/submonoid.lean
0.21451612903225808 src/data/pnat/xgcd.lean
0.21363636363636365 src/algebra/ordered_group.lean
0.20823529411764707 src/data/nat/dist.lean
0.2065573770491803 src/algebra/group_power.lean
0.20473684210526316 src/data/option/basic.lean
0.20357142857142857 src/tactic/omega/int/dnf.lean
0.20285714285714285 src/tactic/omega/nat/dnf.lean
0.20041666666666666 src/control/monad/cont.lean
0.19594594594594594 src/order/bounded_lattice.lean
0.19466666666666665 src/algebra/group_with_zero.lean
0.1942857142857143 src/tactic/ext.lean
0.19333333333333333 src/data/erased.lean
0.193 src/algebra/continued_fractions/terminated_stable.lean
0.1917808219178082 src/topology/order.lean
0.18923076923076923 src/data/equiv/basic.lean
0.184 src/algebra/midpoint.lean
0.18125 src/control/basic.lean
0.18 src/control/traversable/lemmas.lean
0.17666666666666667 src/algebra/free_monoid.lean
0.17613636363636365 src/ring_theory/ideal_operations.lean
0.1732142857142857 src/algebra/group/prod.lean
0.17195767195767195 src/analysis/asymptotics.lean
0.1706451612903226 src/data/list/range.lean
0.16519999999999999 src/algebra/field.lean
0.161 src/algebra/group/hom.lean
0.158 src/data/list/forall2.lean
0.1578125 src/computability/reduce.lean
0.156 src/data/equiv/functor.lean
0.15409090909090908 src/algebra/commute.lean
0.15379310344827585 src/set_theory/surreal.lean
0.15035714285714286 src/group_theory/congruence.lean
0.14953488372093024 src/control/fold.lean
0.14936708860759496 src/group_theory/bundled_subgroup.lean
0.1492 src/algebra/group_with_zero_power.lean
0.14777777777777779 src/topology/homeomorph.lean
0.14431818181818182 src/set_theory/zfc.lean
0.1365079365079365 src/order/complete_lattice.lean
0.135 src/data/option/defs.lean
0.13304347826086957 src/data/bool.lean
0.13210526315789473 src/data/set/intervals/unordered_interval.lean
0.132 src/category_theory/action.lean
0.1288888888888889 src/algebra/char_zero.lean
0.12694444444444444 src/data/list/pairwise.lean
0.12545454545454546 src/data/seq/computation.lean
0.11894736842105262 src/algebra/semiconj.lean
0.11790697674418606 src/data/pnat/basic.lean
0.1175 test/local_cache.lean
0.11416666666666668 src/tactic/omega/nat/sub_elim.lean
0.11305555555555556 src/data/list/chain.lean
0.11 src/linear_algebra/direct_sum_module.lean
0.10923076923076923 src/order/boolean_algebra.lean
0.10651162790697674 src/order/galois_connection.lean
0.10200000000000001 src/tactic/finish.lean
0.09833333333333333 src/data/prod.lean
0.09666666666666666 src/tactic/omega/nat/neg_elim.lean
0.09142857142857143 src/algebra/ordered_field.lean
0.085625 src/order/filter/lift.lean
0.08235294117647059 docs/tutorial/category_theory/calculating_colimits_in_Top.lean
0.08028169014084507 src/order/basic.lean
0.07959999999999999 src/data/nat/gcd.lean
0.07681818181818181 src/data/list/nodup.lean
0.06706896551724138 src/algebra/group/basic.lean
0.06612244897959184 src/data/setoid.lean
0.06296296296296296 src/data/equiv/mul_add.lean
0.060240963855421686 src/data/set/function.lean
0.05482758620689655 src/order/fixed_points.lean
0.050740740740740746 src/algebra/continued_fractions/basic.lean
0.04717391304347826 src/logic/relation.lean
0.0408 src/deprecated/group.lean
0.03980392156862745 src/algebra/order.lean
0.039197080291970804 src/order/bounds.lean
0.02888888888888889 src/logic/function.lean
0.026095890410958906 src/logic/basic.lean
0.020483870967741936 src/data/list/defs.lean
0.01098901098901099 src/order/filter/extr.lean