profile sorted 2020-05-13

645.0 src/analysis/special_functions/trigonometric.lean
472.0 src/data/polynomial.lean
382.0 src/data/multiset.lean
367.0 src/analysis/special_functions/pow.lean
300.0 src/data/mv_polynomial.lean
290.0 src/category_theory/limits/shapes/binary_products.lean
284.0 src/analysis/normed_space/multilinear.lean
270.0 src/topology/metric_space/hausdorff_distance.lean
268.0 src/linear_algebra/basic.lean
254.0 src/data/dfinsupp.lean
240.0 src/analysis/calculus/deriv.lean
234.0 src/geometry/manifold/mfderiv.lean
224.0 src/category_theory/comma.lean
220.0 src/data/complex/exponential.lean
216.0 src/data/finset.lean
212.0 src/linear_algebra/basis.lean
211.0 src/data/padics/padic_numbers.lean
211.0 src/analysis/analytic/basic.lean
208.0 src/ring_theory/power_series.lean
205.0 src/analysis/calculus/times_cont_diff.lean
204.0 src/analysis/calculus/fderiv.lean
196.0 src/data/finsupp.lean
194.0 src/analysis/analytic/composition.lean
192.0 src/data/complex/basic.lean
187.0 src/data/real/ennreal.lean
186.0 src/category_theory/limits/over.lean
183.0 src/measure_theory/integration.lean
178.0 src/analysis/normed_space/basic.lean
170.0 src/measure_theory/outer_measure.lean
156.0 src/analysis/normed_space/real_inner_product.lean
147.0 src/topology/metric_space/basic.lean
144.0 src/ring_theory/localization.lean
144.0 src/data/matrix/basic.lean
138.0 src/topology/algebra/infinite_sum.lean
136.0 src/geometry/manifold/basic_smooth_bundle.lean
128.0 src/topology/metric_space/gromov_hausdorff.lean
123.0 src/topology/algebra/ordered.lean
123.0 src/combinatorics/composition.lean
121.0 src/analysis/normed_space/bounded_linear_maps.lean
118.0 src/data/list/basic.lean
117.0 src/analysis/complex/basic.lean
116.0 src/topology/instances/ennreal.lean
116.0 src/number_theory/quadratic_reciprocity.lean
114.0 src/number_theory/sum_four_squares.lean
114.0 src/data/padics/padic_integers.lean
114.0 src/category_theory/limits/limits.lean
112.0 src/group_theory/perm/sign.lean
108.0 src/measure_theory/measure_space.lean
106.0 src/data/monoid_algebra.lean
106.0 src/computability/turing_machine.lean
105.0 archive/sensitivity.lean
104.0 src/set_theory/ordinal_notation.lean
104.0 src/linear_algebra/multilinear.lean
103.0 src/linear_algebra/finsupp.lean
103.0 src/algebra/big_operators.lean
98.9 src/order/filter/basic.lean
98.1 src/data/zsqrtd/gaussian_int.lean
96.8 src/category_theory/adjunction/limits.lean
94.5 src/measure_theory/lebesgue_measure.lean
92.9 src/data/set/basic.lean
92.9 src/category_theory/limits/shapes/wide_pullbacks.lean
91.8 src/linear_algebra/quadratic_form.lean
91.0 src/computability/partrec_code.lean
90.8 src/data/matrix/notation.lean
90.2 src/topology/subset_properties.lean
90.2 src/set_theory/ordinal.lean
89.4 src/set_theory/cardinal.lean
89.3 src/analysis/convex/basic.lean
89.2 src/category_theory/limits/shapes/images.lean
89.1 src/category_theory/limits/shapes/pullbacks.lean
88.9 src/analysis/normed_space/operator_norm.lean
87.5 src/topology/algebra/module.lean
87.2 src/category_theory/graded_object.lean
85.9 src/data/fintype/basic.lean
85.6 src/data/seq/wseq.lean
82.7 src/data/int/basic.lean
82.7 src/category_theory/elements.lean
81.9 src/analysis/calculus/iterated_deriv.lean
80.9 src/data/real/pi.lean
78.9 src/algebra/lie_algebra.lean
78.3 src/topology/uniform_space/basic.lean
76.6 src/topology/bounded_continuous_function.lean
76.6 src/data/num/lemmas.lean
76.0 src/category_theory/limits/shapes/equalizers.lean
75.3 src/set_theory/cofinality.lean
74.1 src/analysis/special_functions/exp_log.lean
71.5 src/topology/metric_space/emetric_space.lean
69.6 src/topology/metric_space/gromov_hausdorff_realized.lean
68.3 src/algebra/homology/homology.lean
68.0 src/data/padics/hensel.lean
67.9 src/topology/metric_space/gluing.lean
67.4 src/algebra/category/Module/monoidal.lean
66.6 src/category_theory/limits/shapes/constructions/limits_of_products_and_equalizers.lean
63.9 src/measure_theory/probability_mass_function.lean
63.7 archive/cubing_a_cube.lean
63.2 src/data/real/basic.lean
62.5 src/linear_algebra/tensor_product.lean
61.5 src/category_theory/limits/cones.lean
61.1 src/data/real/hyperreal.lean
60.7 src/data/real/nnreal.lean
60.3 src/geometry/manifold/smooth_manifold_with_corners.lean
59.9 src/data/rat/basic.lean
59.3 src/computability/primrec.lean
59.0 src/data/zsqrtd/basic.lean
57.8 src/ring_theory/unique_factorization_domain.lean
57.5 src/data/padics/padic_norm.lean
57.3 src/geometry/manifold/real_instances.lean
57.3 src/data/finmap.lean
56.9 src/measure_theory/bochner_integration.lean
56.1 src/data/list/sigma.lean
55.2 src/algebra/module.lean
54.4 src/algebra/gcd_domain.lean
54.2 src/topology/category/UniformSpace.lean
54.2 src/group_theory/order_of_element.lean
53.7 src/topology/algebra/uniform_group.lean
53.1 src/group_theory/subgroup.lean
53.0 src/group_theory/free_group.lean
52.5 src/data/real/cau_seq.lean
52.4 src/topology/category/Top/adjunctions.lean
52.3 src/algebra/category/Group/biproducts.lean
52.0 src/ring_theory/fractional_ideal.lean
52.0 src/analysis/calculus/specific_functions.lean
51.7 src/analysis/specific_limits.lean
50.9 src/analysis/calculus/extend_deriv.lean
50.4 src/ring_theory/multiplicity.lean
50.1 src/measure_theory/borel_space.lean
50.1 src/algebra/category/Group/basic.lean
49.6 src/measure_theory/ae_eq_fun.lean
49.4 src/ring_theory/ideals.lean
49.2 src/linear_algebra/matrix.lean
48.8 src/data/set/lattice.lean
48.4 src/ring_theory/principal_ideal_domain.lean
48.3 src/linear_algebra/determinant.lean
48.2 src/topology/topological_fiber_bundle.lean
48.2 src/analysis/calculus/tangent_cone.lean
47.7 src/data/nat/basic.lean
47.7 src/computability/partrec.lean
47.1 src/analysis/normed_space/banach.lean
46.9 src/measure_theory/measurable_space.lean
46.5 src/data/pequiv.lean
46.3 src/data/seq/seq.lean
45.2 src/ring_theory/noetherian.lean
45.0 src/data/real/cardinality.lean
45.0 src/algebra/direct_limit.lean
44.9 src/order/complete_boolean_algebra.lean
44.7 src/category_theory/monad/algebra.lean
43.8 src/field_theory/minimal_polynomial.lean
43.2 src/algebra/category/CommRing/basic.lean
42.9 src/field_theory/splitting_field.lean
42.9 src/algebra/associated.lean
42.7 src/ring_theory/polynomial.lean
42.7 src/number_theory/dioph.lean
42.6 src/linear_algebra/bilinear_form.lean
42.6 src/category_theory/monoidal/of_has_finite_products.lean
42.4 src/topology/algebra/group.lean
42.4 src/data/holor.lean
42.2 src/measure_theory/giry_monad.lean
41.5 src/data/set/finite.lean
41.2 src/data/fintype/card.lean
41.1 src/order/filter/filter_product.lean
41.0 src/topology/metric_space/cau_seq_filter.lean
40.0 src/analysis/calculus/local_extr.lean
39.5 src/analysis/calculus/mean_value.lean
38.7 src/number_theory/pell.lean
37.9 src/analysis/normed_space/finite_dimension.lean
37.8 src/data/fin.lean
37.7 src/algebra/category/Module/basic.lean
37.6 src/algebra/pi_instances.lean
37.0 src/topology/instances/real.lean
36.9 src/ring_theory/integral_closure.lean
36.6 src/topology/uniform_space/separation.lean
36.5 src/algebraic_geometry/prime_spectrum.lean
34.9 src/category_theory/currying.lean
34.9 Try this: refine (eq.congr _ _).mp _
34.7 src/field_theory/finite.lean
34.6 src/algebra/category/CommRing/colimits.lean
34.3 src/category_theory/monad/limits.lean
34.2 src/data/zmod/basic.lean
34.1 src/linear_algebra/nonsingular_inverse.lean
33.5 src/algebra/category/Mon/basic.lean
33.3 src/topology/metric_space/closeds.lean
32.9 src/linear_algebra/dual.lean
32.8 src/data/analysis/topology.lean
32.7 src/topology/local_homeomorph.lean
32.6 src/order/lattice.lean
32.5 src/analysis/asymptotics.lean
32.1 src/data/hash_map.lean
31.7 src/measure_theory/l1_space.lean
31.7 src/data/list/perm.lean
31.6 src/ring_theory/algebra.lean
31.4 src/measure_theory/simple_func_dense.lean
31.0 src/topology/basic.lean
30.9 src/data/matrix/pequiv.lean
30.8 src/topology/constructions.lean
30.8 src/category_theory/yoneda.lean
30.7 src/topology/metric_space/isometry.lean
30.2 src/order/filter/partial.lean
30.0 src/data/set/intervals/basic.lean
29.9 src/category_theory/limits/functor_category.lean
29.0 src/data/analysis/filter.lean
28.9 src/analysis/calculus/inverse.lean
28.4 src/algebra/floor.lean
28.0 src/topology/sheaves/presheaf.lean
28.0 src/group_theory/submonoid.lean
27.9 src/group_theory/coset.lean
27.8 src/topology/metric_space/completion.lean
27.8 src/data/fin_enum.lean
27.7 src/category_theory/monad/adjunction.lean
27.5 src/data/pfun.lean
27.4 src/linear_algebra/finite_dimensional.lean
27.3 src/analysis/normed_space/mazur_ulam.lean
27.1 src/set_theory/pgame.lean
27.1 src/order/liminf_limsup.lean
26.7 src/category_theory/differential_object.lean
26.7 src/algebraic_geometry/presheafed_space.lean
26.6 src/data/real/cau_seq_completion.lean
26.5 src/topology/metric_space/baire.lean
26.3 src/group_theory/monoid_localization.lean
26.2 src/linear_algebra/linear_pmap.lean
26.0 src/category_theory/adjunction/basic.lean
25.7 src/computability/halting.lean
25.5 src/tactic/norm_num.lean
25.2 src/algebra/group_power.lean
24.8 src/topology/sheaves/presheaf_of_functions.lean
24.6 src/data/equiv/basic.lean
24.5 src/algebra/category/Group/colimits.lean
24.3 src/ring_theory/adjoin_root.lean
24.0 src/data/equiv/denumerable.lean
23.9 src/analysis/complex/polynomial.lean
23.7 src/topology/continuous_on.lean
23.7 src/order/filter/bases.lean
23.5 src/group_theory/sylow.lean
23.2 src/data/equiv/list.lean
23.0 src/category_theory/products/basic.lean
22.9 src/topology/algebra/multilinear.lean
22.7 src/data/int/parity.lean
22.5 src/tactic/linarith.lean
22.1 src/analysis/normed_space/hahn_banach.lean
22.0 src/topology/uniform_space/cauchy.lean
21.8 src/geometry/manifold/manifold.lean
21.7 src/topology/uniform_space/uniform_embedding.lean
21.6 test/transport/basic.lean
21.4 src/algebra/category/Mon/colimits.lean
21.2 src/algebraic_geometry/stalks.lean
21.1 src/category_theory/limits/shapes/constructions/pullbacks.lean
21.0 src/topology/category/Top/opens.lean
21.0 src/topology/algebra/uniform_ring.lean
21.0 src/data/set/countable.lean
21.0 src/data/nat/multiplicity.lean
20.9 src/algebra/ring.lean
20.8 src/data/rat/cast.lean
20.8 src/algebra/ordered_ring.lean
20.6 src/tactic/ring2.lean
20.6 src/ring_theory/integral_domain.lean
20.4 src/measure_theory/set_integral.lean
20.2 src/category_theory/limits/types.lean
20.1 src/data/vector2.lean
20.0 src/tactic/ring_exp.lean
19.9 src/topology/uniform_space/uniform_convergence.lean
19.9 src/control/traversable/instances.lean
19.8 src/category_theory/monoidal/category.lean
19.4 src/algebra/quadratic_discriminant.lean
19.2 src/analysis/convex/specific_functions.lean
19.1 src/data/indicator_function.lean
19.1 src/analysis/convex/cone.lean
19.0 src/order/conditionally_complete_lattice.lean
18.8 src/topology/uniform_space/completion.lean
18.8 src/algebra/ordered_group.lean
18.6 src/data/list/min_max.lean
18.5 src/category_theory/limits/connected.lean
18.4 src/group_theory/free_abelian_group.lean
18.3 src/linear_algebra/dimension.lean
18.2 src/set_theory/game/short.lean
18.2 src/algebra/continued_fractions/convergents_equiv.lean
18.0 src/algebra/pointwise.lean
17.9 src/number_theory/bernoulli.lean
17.9 src/data/list/sort.lean
17.4 src/field_theory/mv_polynomial.lean
17.3 archive/imo1988_q6.lean
17.2 src/order/complete_lattice.lean
17.2 src/data/nat/prime.lean
16.8 src/ring_theory/free_comm_ring.lean
16.8 src/category_theory/single_obj.lean
16.7 src/topology/category/TopCommRing.lean
16.6 src/data/nat/modeq.lean
16.3 src/tactic/ring.lean
16.2 src/algebra/classical_lie_algebras.lean
16.1 src/category_theory/equivalence.lean
16.0 src/topology/algebra/monoid.lean
15.8 src/topology/separation.lean
15.8 src/category_theory/opposites.lean
15.6 src/data/equiv/encodable.lean
15.6 src/category_theory/whiskering.lean
15.6 src/analysis/mean_inequalities.lean
15.5 src/ring_theory/ideal_operations.lean
15.5 src/ring_theory/algebra_operations.lean
15.2 src/category_theory/limits/shapes/constructions/equalizers.lean
14.7 src/category_theory/discrete_category.lean
14.6 src/algebra/group_with_zero.lean
14.5 src/order/bounded_lattice.lean
14.3 src/data/int/gcd.lean
14.3 src/category_theory/adjunction/fully_faithful.lean
14.1 src/data/rat/order.lean
14.1 src/category_theory/limits/shapes/zero.lean
14.1 src/algebra/geom_sum.lean
14.0 src/topology/order.lean
14.0 src/category_theory/pempty.lean
13.9 src/data/nat/parity.lean
13.8 src/data/seq/computation.lean
13.5 src/algebra/invertible.lean
13.5 src/algebra/category/Group/adjunctions.lean
13.4 src/linear_algebra/linear_action.lean
13.3 src/topology/list.lean
13.3 src/data/pnat/xgcd.lean
13.3 src/data/array/lemmas.lean
13.1 src/algebra/order_functions.lean
13.1 src/algebra/euclidean_domain.lean
13.0 src/topology/maps.lean
13.0 src/topology/instances/nnreal.lean
12.9 src/data/seq/parallel.lean
12.8 src/data/nat/enat.lean
12.8 src/data/int/modeq.lean
12.8 src/category_theory/limits/shapes/kernels.lean
12.8 src/algebra/field_power.lean
12.7 src/set_theory/zfc.lean
12.7 src/set_theory/game/domineering.lean
12.7 src/data/list/alist.lean
12.6 src/order/order_iso.lean
12.4 src/category_theory/const.lean
12.4 src/algebra/char_p.lean
12.2 src/set_theory/lists.lean
12.0 src/data/rel.lean
11.9 src/linear_algebra/special_linear_group.lean
11.9 src/data/pnat/factors.lean
11.8 src/topology/dense_embedding.lean
11.8 src/topology/algebra/open_subgroup.lean
11.8 src/group_theory/bundled_subgroup.lean
11.7 src/topology/metric_space/contracting.lean
11.5 src/category_theory/limits/shapes/biproducts.lean
11.3 src/tactic/abel.lean
10.9 src/topology/algebra/group_completion.lean
10.8 src/topology/sheaves/stalks.lean
10.7 src/data/list/rotate.lean
10.7 src/data/equiv/local_equiv.lean
10.7 src/category_theory/sums/associator.lean
10.7 src/algebra/category/Group/limits.lean
10.6 src/measure_theory/decomposition.lean
10.6 src/category_theory/category/Groupoid.lean
10.6 src/analysis/convex/topology.lean
10.4 src/algebra/category/CommRing/limits.lean
10.3 src/algebra/archimedean.lean
10.1 src/topology/algebra/polynomial.lean
10.1 src/computability/reduce.lean
10.1 src/category_theory/sums/basic.lean
9.81 src/field_theory/perfect_closure.lean
9.62 src/data/real/ereal.lean
9.56 src/order/filter/pointwise.lean
9.53 src/data/list/intervals.lean
9.51 src/topology/metric_space/lipschitz.lean
9.5 src/topology/metric_space/premetric_space.lean
9.47 src/topology/metric_space/antilipschitz.lean
9.47 src/group_theory/perm/cycles.lean
9.43 src/data/real/irrational.lean
9.25 src/topology/compact_open.lean
9.13 src/category_theory/natural_isomorphism.lean
9.08 src/data/set/disjointed.lean
9.0 src/topology/category/Top/open_nhds.lean
8.91 src/category_theory/limits/shapes/products.lean
8.91 src/algebra/direct_sum.lean
8.73 src/data/equiv/transfer_instance.lean
8.5 src/ring_theory/euclidean_domain.lean
8.5 src/category_theory/types.lean
8.42 src/group_theory/congruence.lean
8.4 src/analysis/normed_space/point_reflection.lean
8.39 src/topology/opens.lean
8.08 src/analysis/calculus/darboux.lean
8.04 src/category_theory/monoidal/functor.lean
7.99 test/monotonicity.lean
7.97 src/category_theory/limits/shapes/regular_mono.lean
7.96 src/linear_algebra/sesquilinear_form.lean
7.95 src/group_theory/group_action.lean
7.56 src/algebra/free.lean
7.51 src/data/list/func.lean
7.4 src/topology/bases.lean
7.29 src/data/nat/pairing.lean
7.22 src/topology/instances/complex.lean
7.13 src/data/set/enumerate.lean
7.11 src/algebra/continued_fractions/translations.lean
7.05 src/control/bitraversable/instances.lean
6.97 src/algebra/category/CommRing/adjunctions.lean
6.96 src/category_theory/core.lean
6.93 src/tactic/omega/eq_elim.lean
6.93 src/category_theory/reflect_isomorphisms.lean
6.91 src/category_theory/limits/preserves.lean
6.9 src/analysis/normed_space/riesz_lemma.lean
6.87 src/category_theory/limits/shapes/terminal.lean
6.85 src/data/nat/sqrt.lean
6.82 src/category_theory/limits/shapes/strong_epi.lean
6.8 src/set_theory/game/state.lean
6.7 src/topology/uniform_space/absolute_value.lean
6.67 src/algebra/category/Group/images.lean
6.58 src/order/zorn.lean
6.43 src/control/fold.lean
6.29 src/data/semiquot.lean
6.16 src/tactic/omega/coeffs.lean
6.14 src/data/buffer/basic.lean
6.03 src/data/nat/totient.lean
6.03 docs/tutorial/Zmod37.lean
5.99 src/algebra/category/Group/Z_Module_equivalence.lean
5.97 src/data/nat/gcd.lean
5.97 src/category_theory/connected.lean
5.93 src/category_theory/eq_to_hom.lean
5.87 src/linear_algebra/finsupp_vector_space.lean
5.7 src/order/basic.lean
5.55 src/category_theory/products/associator.lean
5.54 src/topology/sequences.lean
5.52 src/algebra/category/Group/zero.lean
5.5 src/ring_theory/adjoin.lean
5.5 src/data/nat/cast.lean
5.49 src/control/traversable/equiv.lean
5.37 src/order/bounds.lean
5.29 src/data/list/range.lean
5.12 src/algebra/ordered_field.lean
5.07 src/data/pnat/basic.lean
5.07 src/category_theory/functor_category.lean
5.0 src/data/set/function.lean
4.98 src/category_theory/limits/creates.lean
4.95 src/category_theory/quotient.lean
4.92 src/order/pilex.lean
4.89 src/data/lazy_list2.lean
4.89 src/algebra/group/with_one.lean
4.85 src/algebra/group/prod.lean
4.81 src/control/monad/cont.lean
4.81 src/category_theory/fully_faithful.lean
4.79 src/group_theory/quotient_group.lean
4.74 src/data/list/forall2.lean
4.68 src/topology/stone_cech.lean
4.59 src/data/list/bag_inter.lean
4.58 src/order/galois_connection.lean
4.57 src/data/list/pairwise.lean
4.5 src/data/support.lean
4.46 src/set_theory/surreal.lean
4.36 src/order/lexicographic.lean
4.3 src/tactic/core.lean
4.26 src/category_theory/isomorphism.lean
4.19 src/topology/algebra/ring.lean
4.19 src/data/pnat/intervals.lean
4.13 src/algebra/field.lean
4.11 src/order/filter/lift.lean
4.08 src/category_theory/category/default.lean
4.07 src/data/list/chain.lean
3.89 src/data/option/basic.lean
3.89 src/algebra/group/basic.lean
3.84 src/data/finsupp/pointwise.lean
3.83 src/data/nat/choose.lean
3.81 src/logic/basic.lean
3.79 src/logic/embedding.lean
3.76 test/local_cache.lean
3.75 src/control/applicative.lean
3.73 src/algebra/group_with_zero_power.lean
3.66 src/field_theory/subfield.lean
3.63 src/analysis/ODE/gronwall.lean
3.58 src/data/list/zip.lean
3.58 src/category_theory/epi_mono.lean
3.54 test/apply.lean
3.54 src/group_theory/abelianization.lean
3.54 src/data/nat/dist.lean
3.43 src/ring_theory/algebraic.lean
3.42 src/measure_theory/indicator_function.lean
3.41 src/data/fp/basic.lean
3.39 src/data/equiv/fin.lean
3.39 src/algebra/commute.lean
3.38 src/number_theory/sum_two_squares.lean
3.38 src/data/list/nodup.lean
3.38 src/data/equiv/ring.lean
3.35 test/ring_exp.lean
3.32 src/category_theory/hom_functor.lean
3.27 src/data/nat/fib.lean
3.24 src/data/setoid.lean
3.22 src/algebra/group/hom.lean
3.18 src/data/string/basic.lean
3.17 src/tactic/monotonicity/interactive.lean
3.14 src/category_theory/limits/concrete_category.lean
3.1 src/set_theory/schroeder_bernstein.lean
3.06 src/data/bool.lean
2.9 src/control/basic.lean
2.89 src/ring_theory/subring.lean
2.85 src/tactic/tauto.lean
2.85 src/tactic/omega/int/dnf.lean
2.84 src/tactic/omega/nat/dnf.lean
2.76 src/algebra/midpoint.lean
2.76 archive/examples/prop_encodable.lean
2.75 test/equiv_rw.lean
2.74 src/topology/uniform_space/compare_reals.lean
2.67 src/category_theory/conj.lean
2.66 src/topology/homeomorph.lean
2.65 src/algebra/free_monoid.lean
2.61 src/measure_theory/category/Meas.lean
2.56 src/data/list/of_fn.lean
2.52 src/control/traversable/lemmas.lean
2.51 src/data/set/intervals/unordered_interval.lean
2.5 src/order/copy.lean
2.47 src/algebra/continued_fractions/continuants_recurrence.lean
2.45 src/tactic/norm_cast.lean
2.41 src/category_theory/monoidal/functorial.lean
2.33 src/category_theory/groupoid.lean
2.29 src/data/equiv/nat.lean
2.26 src/algebra/semiconj.lean
2.24 src/tactic/interactive.lean
2.24 src/category_theory/category/Rel.lean
2.23 src/algebra/group_ring_action.lean
2.18 src/tactic/omega/nat/main.lean
2.17 src/logic/relation.lean
2.11 src/control/bifunctor.lean
2.03 src/algebra/order.lean
1.99 src/category_theory/concrete_category/bundled_hom.lean
1.97 src/data/list/tfae.lean
1.94 test/ext.lean
1.93 src/algebra/continued_fractions/terminated_stable.lean
1.9 src/tactic/monotonicity/basic.lean
1.86 src/control/traversable/derive.lean
1.86 src/category_theory/limits/opposites.lean
1.77 src/control/bitraversable/lemmas.lean
1.76 src/topology/category/Top/limits.lean
1.7 src/data/equiv/mul_add.lean
1.7 src/category_theory/endomorphism.lean
1.6 src/category_theory/limits/lattice.lean
1.59 src/order/fixed_points.lean
1.58 src/tactic/omega/int/main.lean
1.58 src/category_theory/isomorphism_classes.lean
1.56 src/logic/function.lean
1.56 src/data/equiv/functor.lean
1.55 test/finish4.lean
1.46 src/meta/expr.lean
1.43 src/linear_algebra/direct_sum_module.lean
1.42 src/order/boolean_algebra.lean
1.4 docs/tutorial/category_theory/calculating_colimits_in_Top.lean
1.37 src/tactic/omega/nat/sub_elim.lean
1.37 src/algebra/continued_fractions/basic.lean
1.36 src/tactic/ext.lean
1.35 src/data/rat/floor.lean
1.35 src/control/monad/writer.lean
1.32 src/category_theory/action.lean
1.29 src/data/list/antidiagonal.lean
1.29 src/data/dlist/instances.lean
1.28 src/algebra/group/conj.lean
1.27 src/data/list/defs.lean
1.24 src/category_theory/limits/shapes/finite_products.lean
1.18 src/data/prod.lean
1.18 src/algebra/group/units.lean
1.17 src/control/equiv_functor/instances.lean
1.16 src/tactic/omega/nat/neg_elim.lean
1.16 src/data/erased.lean
1.16 src/algebra/char_zero.lean
1.11 src/tactic/simps.lean
1.09 src/tactic/suggest.lean
1.09 src/category_theory/full_subcategory.lean
1.08 src/data/option/defs.lean
1.02 src/tactic/finish.lean
1.02 src/deprecated/group.lean
1.0 src/order/filter/extr.lean