13.284117 s: Algebra.forget₂_Ring_preserves_limits_aux
12.172984 s: Algebra.forget₂_Ring_preserves_limits_aux.equations._eqn_1
9.759439 s: to_euclidean
9.644809 s: smooth_bump_covering.exists_immersion_findim
9.346480 s: to_euclidean.equations._eqn_1
8.179359 s: CommGroup.category_theory.forget₂.category_theory.creates_limit._proof_7
7.952717 s: AddCommMon.category_theory.forget₂.category_theory.creates_limit._proof_6
7.876578 s: SemiRing.limit_π_ring_hom.equations._eqn_1
7.872092 s: SemiRing.limit_π_ring_hom
7.626054 s: AddCommGroup.category_theory.forget₂.category_theory.creates_limit._proof_7
7.372604 s: CommMon.category_theory.forget₂.category_theory.creates_limit._proof_6
5.510193 s: SemiRing.forget₂_AddCommMon_preserves_limits_aux
5.177408 s: SemiRing.forget₂_AddCommMon_preserves_limits_aux.equations._eqn_1
4.339591 s: AddCommMon.category_theory.forget₂.category_theory.creates_limit
4.259126 s: AddCommGroup.category_theory.forget₂.category_theory.creates_limit
4.167444 s: CommMon.category_theory.forget₂.category_theory.creates_limit
4.081465 s: CommGroup.category_theory.forget₂.category_theory.creates_limit.equations._eqn_1
4.003845 s: CommGroup.category_theory.forget₂.category_theory.creates_limit
3.984336 s: AddCommMon.category_theory.forget₂.category_theory.creates_limit.equations._eqn_1
3.955816 s: euclidean.exists_pos_lt_subset_ball
3.845440 s: CommMon.category_theory.forget₂.category_theory.creates_limit.equations._eqn_1
3.802986 s: SemiRing.forget₂_Mon_preserves_limits_aux
3.800642 s: AddCommGroup.category_theory.forget₂.category_theory.creates_limit.equations._eqn_1
3.797885 s: euclidean.compact_ball
3.788635 s: SemiRing.forget₂_Mon_preserves_limits_aux.equations._eqn_1
3.229404 s: Ring.forget₂_AddCommGroup_preserves_limits_aux
3.145671 s: Ring.forget₂_AddCommGroup_preserves_limits_aux.equations._eqn_1
2.969988 s: matrix.rank_diagonal
2.803658 s: Module.forget₂_AddCommGroup_preserves_limits_aux.equations._eqn_1
2.659098 s: AddGroup.category_theory.forget₂.category_theory.creates_limit._proof_6
2.539379 s: lift_of_splits
2.538416 s: CommGroup.forget₂_CommMon_preserves_limits_aux.equations._eqn_1
2.536361 s: CommGroup.forget₂_CommMon_preserves_limits_aux
2.502885 s: Module.forget₂_AddCommGroup_preserves_limits_aux
2.264196 s: Group.category_theory.forget₂.category_theory.creates_limit._proof_6
2.228118 s: AddCommGroup.forget₂_AddCommMon_preserves_limits_aux.equations._eqn_1
2.121582 s: AddCommGroup.forget₂_AddCommMon_preserves_limits_aux
1.970376 s: real.tendsto_sum_pi_div_four
1.955642 s: is_max_on.of_is_local_max_of_convex_univ
1.893920 s: free_algebra.is_basis_free_monoid
1.857191 s: concave_on.le_on_segment
1.820432 s: is_max_on.of_is_local_max_on_of_concave_on
1.780909 s: formal_multilinear_series.radius_right_inv_pos_of_radius_pos
1.759308 s: concave_on.le_on_segment'
1.668602 s: real.is_cau_seq_iff_lift
1.657865 s: liouville.irrational
1.643970 s: real.integral_sin_pow_div_tendsto_one
1.616896 s: urysohns.CU.approx_le_succ
1.577300 s: monoid_algebra.ring.equations._eqn_1
1.573118 s: field.direct_limit.nontrivial.equations._eqn_1
1.572276 s: matrix.ker_diagonal_to_lin'
1.516290 s: real.abs_log_sub_add_sum_range_le
1.486407 s: real.has_sum_pow_div_log_of_abs_lt_1
1.431125 s: gaussian_int.to_complex_div_re
1.422002 s: rat.uniform_space_eq
1.404647 s: AddGroup.category_theory.forget₂.category_theory.creates_limit.equations._eqn_1
1.401459 s: algebraic_closure.of_step_succ
1.339816 s: AddGroup.category_theory.forget₂.category_theory.creates_limit
1.321625 s: concave_on_log_Ioi
1.318128 s: Group.category_theory.forget₂.category_theory.creates_limit.equations._eqn_1
1.300745 s: concave_on_log_Iio
1.292922 s: monoid_algebra.ring
1.292860 s: CommRing.forget₂_CommSemiRing_preserves_limits_aux
1.287143 s: liouville.exists_pos_real_of_irrational_root
1.257676 s: CommRing.forget₂_CommSemiRing_preserves_limits_aux.equations._eqn_1
1.223202 s: function.injective.linear_ordered_field
1.215857 s: field.direct_limit.nontrivial
1.202237 s: Group.category_theory.forget₂.category_theory.creates_limit
1.169045 s: algebraic_closure.exists_root
1.152706 s: det_eq_sign_char_poly_coeff
1.108708 s: hyperreal.coe_abs
1.091663 s: matrix.is_skew_adjoint_bracket
1.085177 s: function.injective.linear_ordered_comm_ring._proof_12
1.080033 s: alg_hom.restrict_normal_aux._proof_2
1.075912 s: tendsto_at_top_of_geom_le
1.066413 s: real.tendsto_mul_exp_add_div_pow_at_top
1.062084 s: skew_adjoint_matrices_lie_subalgebra_equiv_transpose._proof_1
1.057650 s: gaussian_int.norm_sq_div_sub_div_lt_one
1.041303 s: function.injective.linear_ordered_comm_ring._proof_13
1.037521 s: CommRing.is_limit_lifted_cone._proof_1
1.036637 s: CommRing.is_limit_lifted_cone
1.016141 s: stereo_inv_fun_aux_mem
1.015585 s: real.of_near
1.009085 s: CommRing.category_theory.forget₂.category_theory.creates_limit
0.994724 s: circle_deg1_lift.tendsto_translation_number_of_dist_bounded_aux
0.992269 s: alg_hom.restrict_normal_aux._proof_3
0.988363 s: circle_deg1_lift.transnum_aux_seq_dist_lt
0.987472 s: function.injective.linear_ordered_comm_ring._proof_14
0.981355 s: CommRing.is_limit_lifted_cone.equations._eqn_1
0.974025 s: is_R_or_C.abs_re_div_abs_le_one
0.969633 s: function.injective.linear_ordered_comm_ring._proof_15
0.968095 s: function.injective.linear_ordered_comm_ring._proof_7
0.963237 s: real.complete_space.equations._eqn_1
0.958353 s: function.injective.linear_ordered_comm_ring._proof_2
0.944494 s: rat.uniform_continuous_abs
0.942960 s: dense_embedding_of_rat
0.937241 s: function.injective.linear_ordered_comm_ring._proof_10
0.932848 s: gaussian_int.to_complex_div_im
0.930295 s: function.injective.linear_ordered_comm_ring._proof_9
0.930061 s: real.cau_seq_converges
0.914906 s: complex.abs_re_div_abs_le_one
0.912126 s: function.injective.linear_ordered_comm_ring._proof_3
0.901310 s: continuous_equiv_fun_basis
0.897142 s: function.injective.linear_ordered_comm_ring._proof_1
0.893755 s: bounded_continuous_function.add_comm_group._proof_1
0.889295 s: function.injective.linear_ordered_comm_ring._proof_5
0.876498 s: CommRing.category_theory.forget₂.category_theory.creates_limit.equations._eqn_1
0.875604 s: function.injective.linear_ordered_comm_ring._proof_6
0.871155 s: function.injective.linear_ordered_comm_ring._proof_8
0.871007 s: function.injective.linear_ordered_comm_ring._proof_20
0.870662 s: linear_map.findim_linear_map
0.863541 s: has_ftaylor_series_up_to_on_pi
0.861685 s: function.injective.linear_ordered_comm_ring._proof_11
0.854350 s: ideal.module_pi._proof_4
0.851926 s: real.log_inv
0.847999 s: real.log_div
0.822495 s: function.injective.linear_ordered_comm_ring._proof_4
0.822455 s: is_R_or_C.abs_im_div_abs_le_one
0.821069 s: abs_real_inner_div_norm_mul_norm_le_one
0.813335 s: complex.exp_add
0.812005 s: function.injective.linear_ordered_field.equations._eqn_1
0.807336 s: intermediate_field.adjoin_root_equiv_adjoin._proof_6
0.805249 s: integral_closure.fraction_map_of_algebraic._match_2.equations._eqn_1
0.802206 s: real.exp_approx_succ
0.800209 s: real.exists_sup
0.797350 s: complex.exp_bound
0.796009 s: discrim_lt_zero
0.789932 s: quaternion.norm_sq_inv
0.786664 s: real.subgroup_dense_of_no_min
0.784317 s: matrix.findim_matrix
0.768259 s: ideal.module_pi._proof_2
0.763217 s: matrix.finite_dimensional
0.762248 s: normal.of_is_splitting_field
0.758677 s: alg_hom.restrict_normal_aux._proof_5
0.754248 s: alg_hom.restrict_normal_aux._proof_4
0.749857 s: adjoin_root.equiv._proof_4
0.749719 s: real.uniform_continuous_inv
0.743071 s: real.abs.cau_seq.is_complete.equations._eqn_1
0.742980 s: Ring.sections_subring.equations._eqn_1
0.740508 s: CommRing.lifted_cone.equations._eqn_1
0.737734 s: euclidean_geometry.exists_unique_dist_eq_of_insert
0.734158 s: alg_hom.restrict_normal_aux._proof_6
0.732575 s: Algebra.forget₂_Module_preserves_limits_aux._proof_1
0.730506 s: Ring.category_theory.forget₂.category_theory.creates_limit._proof_8
0.729469 s: real.sin_eq_zero_iff
0.725159 s: polynomial.is_primitive.dvd_of_fraction_map_dvd_fraction_map
0.721412 s: real.uniform_continuous_mul
0.720554 s: complex.lim_aux.equations._eqn_1
0.715666 s: matrix.finite_dimensional.equations._eqn_1
0.713755 s: finite_field.char_poly_pow_card
0.712755 s: circle_deg1_lift.tendsto_translation_number₀'
0.697353 s: is_galois.of_separable_splitting_field_aux
0.694141 s: complex.is_cau_abs_exp
0.692032 s: ideal.module_pi._proof_3
0.691565 s: one_le_pow_mul_abs_eval_div
0.689711 s: polynomial.exists_multiset_of_splits
0.686344 s: real.exists_extension_norm_eq
0.684986 s: is_R_or_C.abs_abs_sub_le_abs_sub
0.683953 s: map_le_line_map_iff_slope_le_slope_right
0.682946 s: min_eq_half_add_sub_abs_sub
0.681817 s: real.add_one_le_exp_of_nonneg
0.679855 s: real.complete_space
0.678961 s: integral_closure.fraction_map_of_algebraic._match_1.equations._eqn_1
0.671846 s: stereo_left_inv
0.671273 s: integral_closure.fraction_map_of_algebraic._match_3.equations._eqn_1
0.669882 s: finite_dimensional.findim_linear_map
0.668895 s: Algebra.limit_π_alg_hom
0.668759 s: integral_closure.fraction_map_of_algebraic._match_2
0.668144 s: real.is_conjugate_exponent.symm
0.667310 s: polynomial.roots_map
0.665200 s: intermediate_field.findim_fixed_field_eq_card
0.659742 s: times_cont_diff_bump
0.659021 s: real.uniform_continuous_add
0.654051 s: complex.abs_im_div_abs_le_one
0.649097 s: integral_inv_one_add_sq
0.648469 s: exists_extension_norm_eq
0.646483 s: CommRing.limit_comm_ring.equations._eqn_1
0.644516 s: complex.lim_abs
0.643018 s: measure_theory.hahn_decomposition
0.638951 s: is_primitive_root.minpoly_eq_pow
0.638583 s: complex.lim_eq_lim_im_add_lim_re
0.638228 s: algebraic_closure.step.scalar_tower
0.631322 s: real.abs.cau_seq.is_complete
0.630791 s: ideal.module_pi._proof_7
0.625399 s: complex.lim_conj
0.625184 s: ideal.module_pi._proof_1
0.619488 s: complex.lim_re
0.618873 s: complex.lim_im
0.618863 s: intermediate_field.adjoin_root_equiv_adjoin._proof_4
0.617627 s: ideal.module_pi._proof_5
0.616021 s: smooth_bump_function
0.615990 s: complex.lim_aux
0.613173 s: convex.mem_Ioo
0.613014 s: intermediate_field.lifts.lift_of_splits._proof_5
0.602037 s: multilinear_map.mk_continuous_multilinear._proof_7
0.601474 s: Module.monoidal_category.pentagon
0.600550 s: complex.is_cau_exp
0.599738 s: max_eq_half_add_add_abs_sub
0.599186 s: linear_map.finite_dimensional.equations._eqn_1
0.594764 s: integral_closure.fraction_map_of_algebraic._match_1
0.593907 s: witt_vector.poly_eq_of_witt_polynomial_bind_eq'
0.592401 s: CommGroup.has_forget_to_CommMon.equations._eqn_1
0.590106 s: complex.abs_abs_sub_le_abs_sub
0.589263 s: solvable_by_rad.induction2
0.583780 s: Gromov_Hausdorff.GH_dist_le_of_approx_subsets
0.582140 s: is_basis.isometry_euclidean_of_orthonormal.equations._eqn_1
0.581377 s: is_galois.of_separable_splitting_field
0.580149 s: complex.equiv_lim_aux
0.579521 s: ideal.module_pi._proof_6
0.572951 s: polynomial.gal.map_roots._proof_1
0.572278 s: polynomial.splitting_field_aux.adjoin_roots
0.571348 s: CommGroup.has_forget_to_CommMon
0.571225 s: skew_adjoint_matrices_lie_subalgebra_equiv._proof_1
0.565096 s: convex.mem_Ioc
0.564930 s: witt_vector.map_frobenius_poly
0.563780 s: function.injective.ordered_comm_ring
0.562857 s: Ring.sections_subring
0.561291 s: convex.mem_Icc
0.560003 s: power_basis.equiv_adjoin_simple_aeval
0.555430 s: ideal.integral_closure.comap_lt_comap
0.552750 s: function.injective.ordered_comm_ring.equations._eqn_1
0.552569 s: field.primitive_element_inf_aux
0.550001 s: ideal.integral_closure.is_maximal_of_is_maximal_comap
0.549805 s: intermediate_field.adjoin_root_equiv_adjoin._proof_5
0.549741 s: power_basis.equiv_adjoin_simple
0.546810 s: CommRing.lifted_cone
0.543588 s: generalized_continued_fraction.comp_exact_value_correctness_of_stream_eq_some
0.541951 s: alg_hom.restrict_normal_aux._proof_1
0.541913 s: fpow_strict_mono
0.540945 s: maps_to_tangent_cone_pi
0.538620 s: module.End.exists_eigenvalue
0.537907 s: discrim_le_zero
0.537398 s: Module.hexagon_reverse
0.537034 s: ideal.integral_closure.comap_ne_bot
0.535409 s: Gromov_Hausdorff.second_countable
0.533672 s: intermediate_field.lifts.lift_of_splits.equations._eqn_1
0.532254 s: Gromov_Hausdorff.second_countable.equations._eqn_1
0.531377 s: polynomial.map_dvd_map'
0.529819 s: polynomial.is_unit_or_eq_zero_of_is_unit_integer_normalization_prim_part
0.528628 s: uniformity_basis_dist_pow_of_lt_1
0.524922 s: power_basis.equiv_adjoin_simple_gen
0.524588 s: convex.mem_Ico
0.521246 s: affine.simplex.findim_direction_altitude
0.518478 s: matrix.ring.equations._eqn_1
0.518090 s: function.injective.linear_ordered_comm_ring
0.516995 s: approximates_linear_on.surj_on_closed_ball_of_nonlinear_right_inverse
0.516774 s: pythagorean_triple.is_primitive_classified_of_coprime_of_odd_of_pos
0.516387 s: convex_cone.to_ordered_semimodule
0.516379 s: map_le_line_map_iff_slope_le_slope
0.516247 s: linear_recurrence.sol_space_dim
0.515595 s: power_basis.equiv_adjoin_simple._proof_4
0.511478 s: CommRing.limit_comm_ring
0.511122 s: fderiv_measurable_aux.D_subset_differentiable_set
0.508295 s: polynomial.gal.restrict_prod_injective
0.507438 s: Algebra.limit_π_alg_hom.equations._eqn_1
0.503890 s: intermediate_field.adjoin_root_equiv_adjoin._proof_3
0.503407 s: has_fpower_series_on_ball.tendsto_uniformly_on
0.501187 s: midpoint_le_left
-6.469990 s: bounded_continuous_function.add_comm_group._proof_6
-6.594427 s: bounded_continuous_function.add_comm_group._proof_4
-6.598675 s: bounded_continuous_function.add_comm_group._proof_5