2020-05-13

https://tqft.net/lean/mathlib/437fdaf891cd362884def00c5ab672e17c5373b9.log

254 decl post-processing of complete_lattice took 254s
238 decl post-processing of to_mul_equiv took 238s
194 decl post-processing of semilattice_sup_top took 194s
124 decl post-processing of of_mul_equiv took 124s
122 decl post-processing of correspondence took 122s
120 decl post-processing of lift_eq_iff took 120s
114 decl post-processing of eq_of_eq took 114s
99.8 decl post-processing of measurable_inv took 99.8s
95.5 decl post-processing of quotient_ker_equiv_range took 95.5s
94.6 decl post-processing of map took 94.6s
91.3 decl post-processing of exists_of_sec_mk' took 91.3s
87 decl post-processing of lift took 87s
85.2 decl post-processing of comm_group took 85.2s
84.8 decl post-processing of map took 84.8s
82.4 decl post-processing of lift_surjective_iff took 82.4s
80.5 decl post-processing of lift_injective_iff took 80.5s
78.8 decl post-processing of semilattice_inf_top took 78.8s
78.3 decl post-processing of pointwise_mul took 78.3s
76.2 decl post-processing of lift_mul_left took 76.2s
75 decl post-processing of group took 75s
74.3 decl post-processing of lift_left_inverse took 74.3s
69.7 decl post-processing of lift_of_comp took 69.7s
69.2 decl post-processing of epic_of_localization_map took 69.2s
69.1 decl post-processing of CommMon_iso_to_mul_equiv took 69.1s
69 decl post-processing of mul_equiv_of_localizations_apply took 69s
65.6 decl post-processing of quotient_quotient_equiv_quotient took 65.6s
64.8 decl post-processing of map_eq took 64.8s
63.5 decl post-processing of eq_locus took 63.5s
63.5 decl post-processing of measurable.inv took 63.5s
61.3 decl post-processing of prod_equiv took 61.3s
61.1 decl post-processing of lift_eq took 61.1s
60.5 decl post-processing of lift_mul_right took 60.5s
58.1 decl post-processing of complete_lattice took 58.1s
56.6 decl post-processing of lift_unique took 56.6s
55.7 decl post-processing of has_bot took 55.7s
55.2 decl post-processing of mul_equiv.to_CommMon_iso_inv took 55.2s
51.9 decl post-processing of mk'_mul_eq_mk'_of_mul took 51.9s
51.9 decl post-processing of mem_sup took 51.9s
51.4 decl post-processing of mul_ker took 51.4s
50.9 decl post-processing of partial_order took 50.9s
49.5 decl post-processing of lift_comp took 49.5s
49.2 decl post-processing of comap took 49.2s
48.9 decl post-processing of map_spec took 48.9s
48.5 decl post-processing of comm_group took 48.5s
48.4 decl post-processing of is_submonoid_Union_of_directed took 48.4s
48.4 decl post-processing of mul_inv took 48.4s
48.3 decl post-processing of subtype.comm_monoid took 48.3s
47.8 decl post-processing of mk'_self' took 47.8s
47.3 decl post-processing of homeomorph.mul_right took 47.3s
47.1 decl post-processing of subtype.group took 47.1s
47 decl post-processing of sec_spec' took 47s
46.8 decl post-processing of subgroup_congr took 46.8s
46.6 decl post-processing of mk'_spec took 46.6s
46.5 decl post-processing of congr took 46.5s
46.2 decl post-processing of map_mul_right took 46.2s
45.6 decl post-processing of is_submonoid.inter took 45.6s
45.1 decl post-processing of measurable.of_inv took 45.1s
44.8 decl post-processing of comp_eq_of_eq took 44.8s
44.7 decl post-processing of mul_equiv_iso_Mon_iso took 44.7s
44.6 decl post-processing of homeomorph.mul_left took 44.6s
42.4 decl post-processing of closure_le took 42.4s
42.3 decl post-processing of mul_mk'_one_eq_mk' took 42.3s
42.2 decl post-processing of map_mul_left took 42.2s
42 decl post-processing of subtype.comm_group took 42s
41.4 decl post-processing of of_mul_equiv_id took 41.4s
41.4 decl post-processing of Group_iso_to_mul_equiv took 41.4s
41.3 decl post-processing of mul_inv_left took 41.3s
41.2 decl post-processing of quotient_ker_equiv_of_surjective took 41.2s
41.1 decl post-processing of has_top took 41.1s
41 decl post-processing of prod_cancels_of_partition_cancels took 41s
39.9 decl post-processing of continuous_on.mul took 39.9s
39.6 decl post-processing of pi took 39.6s
39.1 decl post-processing of symm took 39.1s
38.9 decl post-processing of lift_spec took 38.9s
38.5 decl post-processing of map_mk' took 38.5s
38.3 decl post-processing of ker_lift took 38.3s
38.1 decl post-processing of to_mul_equiv_id took 38.1s
37.9 decl post-processing of has_top took 37.9s
37.2 decl post-processing of tendsto_mul took 37.2s
36.6 decl post-processing of lift_id took 36.6s
36.4 decl post-processing of inv took 36.4s
36.1 decl post-processing of submonoid took 36.1s
36 decl post-processing of tendsto.mul_mul took 36s
36 decl post-processing of mul_left took 36s
36 decl post-processing of lift_spec_mul took 36s
35.7 decl post-processing of mk'_eq_of_eq took 35.7s
35.7 decl post-processing of finset.measurable_prod took 35.7s
35.7 decl post-processing of subtype.monoid took 35.7s
35.6 decl post-processing of prod_mono_right took 35.6s
35.6 decl post-processing of mul_equiv_of_mul_equiv_eq_map_apply took 35.6s
35.5 decl post-processing of mk' took 35.5s
35.4 decl post-processing of mk'_self took 35.4s
35.3 decl post-processing of trans took 35.3s
35.3 decl post-processing of mul_equiv_iso_CommMon_iso took 35.3s
35 decl post-processing of r' took 35s
34.8 decl post-processing of pointwise_mul_ne_bot took 34.8s
34.6 decl post-processing of Mon_iso_to_mul_equiv took 34.6s
34.3 decl post-processing of complete_lattice took 34.3s
34.3 decl post-processing of sec took 34.3s
34.1 decl post-processing of mk'_surjective took 34.1s
33.7 decl post-processing of submonoid_congr took 33.7s
33.5 decl post-processing of measurable.mul took 33.5s
33.3 decl post-processing of mk'_mul_cancel_left took 33.3s
32.9 decl post-processing of inr took 32.9s
32.9 decl post-processing of map_id took 32.9s
32.8 decl post-processing of has_inf took 32.8s
32.7 elaboration of prime_sum_four_squares took 32.7s
32.2 decl post-processing of comap took 32.2s
32 decl post-processing of mul_equiv.to_CommGroup_iso took 32s
31.6 decl post-processing of gi took 31.6s
31.5 decl post-processing of tendsto_multiset_prod took 31.5s
30.9 decl post-processing of prod_eq_one took 30.9s
30.8 decl post-processing of prod took 30.8s
30.6 decl post-processing of mul_equiv_of_mul_equiv_eq_map took 30.6s
30.5 decl post-processing of bot_prod_bot took 30.5s
30.5 decl post-processing of inv_inj took 30.5s
30.4 decl post-processing of map_comp_map took 30.4s
30.4 decl post-processing of ext took 30.4s
29.9 decl post-processing of prod_filter_ne_one took 29.9s
29.9 decl post-processing of lift_mk' took 29.9s
29.8 decl post-processing of mul_equiv.to_CommMon_iso took 29.8s
29.7 decl post-processing of lift took 29.7s
29.4 decl post-processing of tendsto_list_prod took 29.4s
29.4 decl post-processing of prod took 29.4s
29.4 decl post-processing of monoid took 29.4s
29.1 decl post-processing of mul_mk'_eq_mk'_of_mul took 29.1s
28.9 decl post-processing of localization.inhabited took 28.9s
28.6 decl post-processing of prod_mono took 28.6s
28.4 decl post-processing of pointwise_mul_assoc took 28.4s
28.1 decl post-processing of category_theory.bundled_hom.parent_projection took 28.1s
28 decl post-processing of to_group took 28s
28 decl post-processing of mul_equiv_of_localizations_symm_apply took 28s
27.8 decl post-processing of map_comp took 27.8s
27.8 decl post-processing of pointwise_mul_le_mul took 27.8s
27.7 decl post-processing of group took 27.7s
27.7 decl post-processing of mul_right took 27.7s
27.7 decl post-processing of is_open_map_mul_left took 27.7s
27.7 decl post-processing of lift_comp_mk' took 27.7s
27.5 decl post-processing of mem_ker took 27.5s
27.3 decl post-processing of quotient.inhabited took 27.3s
27.3 decl post-processing of is_submonoid.coe_one took 27.3s
27.2 decl post-processing of monoid took 27.2s
27.1 decl post-processing of map_closure took 27.1s
26.9 decl post-processing of r_iff_exists took 26.9s
26.6 decl post-processing of homeomorph.inv took 26.6s
26.6 decl post-processing of filter.tendsto.inv took 26.6s
26.5 decl post-processing of ext took 26.5s
26.2 decl post-processing of prod took 26.2s
26.2 decl post-processing of ext took 26.2s
26 decl post-processing of has_forget_to_Mon took 26s
25.9 decl post-processing of to_mul_equiv_of_mul_equiv_apply took 25.9s
25.8 decl post-processing of comap_mul_comap_le took 25.8s
25.4 decl post-processing of is_submonoid.mem_nhds_one took 25.4s
25.2 decl post-processing of mul_equiv_of_mul_equiv_eq took 25.2s
25.2 decl post-processing of to_comm_group took 25.2s
25.2 decl post-processing of prod_finset_sum_index took 25.2s
25.1 decl post-processing of bundled_hom took 25.1s
25.1 elaboration: tactic execution took 25.1s
24.8 decl post-processing of symm_of_mul_equiv_apply took 24.8s
24.8 decl post-processing of nhds_one_symm took 24.8s
24 decl post-processing of coe_range took 24s
24 decl post-processing of continuous_group took 24s
23.9 decl post-processing of map took 23.9s
23.9 decl post-processing of map_apply took 23.9s
23.8 decl post-processing of lift_on_beta took 23.8s
23.7 decl post-processing of inhabited took 23.7s
23.6 decl post-processing of tendsto_finset_prod took 23.6s
23.4 decl post-processing of mk'_spec' took 23.4s
23.4 decl post-processing of coe_mul took 23.4s
23.4 decl post-processing of sup_def took 23.4s
23.4 decl post-processing of ext'_iff took 23.4s
23.3 decl post-processing of nonempty_of_prod_ne_one took 23.3s
23 decl post-processing of CommGroup_iso_to_mul_equiv took 23s
22.9 decl post-processing of prod_map_range_index took 22.9s
22.9 decl post-processing of monoid_hom.apply took 22.9s
22.8 decl post-processing of continuous_within_at.inv took 22.8s
22.7 decl post-processing of is_closed_map_mul_left took 22.7s
22.6 decl post-processing of range_top_iff_surjective took 22.6s
22.5 decl post-processing of mul_equiv_of_mul_equiv took 22.5s
22.5 decl post-processing of measurable_inv_iff took 22.5s
22.5 decl post-processing of lift_on took 22.5s
22.5 decl post-processing of ker took 22.5s
22.4 decl post-processing of ext took 22.4s
22.3 decl post-processing of to_mul_equiv_of_mul_equiv took 22.3s
22.3 decl post-processing of of took 22.3s
22.2 decl post-processing of prod_mono_left took 22.2s
22.2 decl post-processing of to_mul_equiv_comp took 22.2s
22.2 decl post-processing of coe_eq took 22.2s
22.2 decl post-processing of prod_comm took 22.2s
22 decl post-processing of prod_subtype_domain_index took 22s
21.7 decl post-processing of mk'_mul took 21.7s
21.7 decl post-processing of comp_mul_equiv_symm_comap_apply took 21.7s
21.7 decl post-processing of continuous_inv took 21.7s
21.7 decl post-processing of is_unit_comp took 21.7s
21.6 decl post-processing of has_coe_to_sort took 21.6s
21.5 decl post-processing of eq_iff_eq took 21.5s
21.5 decl post-processing of r_eq_r' took 21.5s
21.5 decl post-processing of continuous.inv took 21.5s
21.4 decl post-processing of is_subgroup_Union_of_directed took 21.4s
21.4 decl post-processing of unique took 21.4s
21.4 decl post-processing of prod_neg_index took 21.4s
21.3 decl post-processing of inl took 21.3s
21.3 decl post-processing of one_apply took 21.3s
21 decl post-processing of pointwise_mul_monoid took 21s
20.9 decl post-processing of prod_ite_eq' took 20.9s
20.8 decl post-processing of pointwise_mul_finite took 20.8s
20.8 decl post-processing of comm_group took 20.8s
20.7 decl post-processing of prod_add_index took 20.7s
20.5 decl post-processing of to_comm_monoid took 20.5s
20.5 decl post-processing of powers.is_submonoid took 20.5s
20.5 decl post-processing of measurable_mul took 20.5s
20.5 decl post-processing of comp_mul_equiv_symm_map_apply took 20.5s
20.4 decl post-processing of continuous_on.inv took 20.4s
20.4 decl post-processing of to_mul_equiv_of_mul_equiv_of_mul_equiv_apply took 20.4s
20.4 decl post-processing of coe_top took 20.4s
20.3 decl post-processing of lift_mk'_spec took 20.3s
20.3 decl post-processing of prod_sum_index took 20.3s
20.2 decl post-processing of map_pointwise_one took 20.2s
20 elaboration of cones_equiv took 20s
20 decl post-processing of con_gen_eq took 20s
19.9 decl post-processing of prod_bij took 19.9s
19.8 decl post-processing of induction_on₂ took 19.8s
19.8 decl post-processing of mk'_one took 19.8s
19.6 decl post-processing of has_Inf took 19.6s
19.6 decl post-processing of left_coset_equiv_subgroup took 19.6s
19.5 decl post-processing of open_subgroup.has_coe took 19.5s
19.5 decl post-processing of coe_inf took 19.5s
19.3 decl post-processing of has_bot took 19.3s
19.2 decl post-processing of has_mul took 19.2s
19.1 decl post-processing of is_group_hom_finset_prod took 19.1s
19.1 decl post-processing of category_theory.category took 19.1s
19.1 decl post-processing of prod_bij_ne_one took 19.1s
19 decl post-processing of coe_bot took 19s
19 elaboration of linear_independent_iff_not_smul_mem_span took 19s
18.9 decl post-processing of has_coe_t took 18.9s
18.8 decl post-processing of prod_inv_distrib took 18.8s
18.8 decl post-processing of con_gen_idem took 18.8s
18.7 decl post-processing of preimage took 18.7s
18.7 decl post-processing of prod.topological_monoid took 18.7s
18.7 decl post-processing of has_Inf took 18.7s
18.6 decl post-processing of continuous_at.mul took 18.6s
18.6 decl post-processing of Inf_to_setoid took 18.6s
18.5 elaboration of adj₁ took 18.5s
18.5 decl post-processing of sec_spec took 18.5s
18.4 decl post-processing of list_prod_mem took 18.4s
18.4 decl post-processing of to_fun_inj took 18.4s
18.4 elaboration of exists_norm_eq_infi_of_complete_convex took 18.4s
18.2 decl post-processing of quotient took 18.2s
18.2 decl post-processing of con_gen_le took 18.2s
18 decl post-processing of list_prod_apply took 18s
18 decl post-processing of prod_piecewise took 18s
17.9 decl post-processing of injective_mul took 17.9s
17.9 elaboration of prod_functor took 17.9s
17.7 decl post-processing of mk'_mul_cancel_right took 17.7s
17.7 decl post-processing of top_prod took 17.7s
17.7 decl post-processing of comap_inf took 17.7s
17.6 decl post-processing of to_hom_units took 17.6s
17.5 decl post-processing of is_submonoid took 17.5s
17.4 decl post-processing of ext_iff took 17.4s
17.4 decl post-processing of is_open_pointwise_mul_left took 17.4s
17.4 decl post-processing of category_theory.bundled_hom.parent_projection took 17.4s
17.4 decl post-processing of comm_monoid took 17.4s
17.3 decl post-processing of subset_closure took 17.3s
17.2 decl post-processing of closure_empty took 17.2s
17.2 decl post-processing of is_open_map_mul_right took 17.2s
17.1 decl post-processing of subtype took 17.1s
17.1 decl post-processing of range_inl' took 17.1s
17.1 decl post-processing of exists_nhds_split took 17.1s
17.1 decl post-processing of has_coe_to_sort took 17.1s
17.1 decl post-processing of inv_unique took 17.1s
17.1 decl post-processing of category_theory.category took 17.1s
16.9 elaboration of has_sum.has_sum_ne_zero took 16.9s
16.8 decl post-processing of to_monoid took 16.8s
16.7 decl post-processing of inhabited took 16.7s
16.7 decl post-processing of range_subtype took 16.7s
16.6 decl post-processing of has_mem took 16.6s
16.6 decl post-processing of eq' took 16.6s
16.5 decl post-processing of map_map took 16.5s
16.4 decl post-processing of comm_monoid took 16.4s
16.4 decl post-processing of left_rel took 16.4s
16.4 decl post-processing of Inf_def took 16.4s
16.3 decl post-processing of mem_pointwise_mul took 16.3s
16.3 decl post-processing of image.is_submonoid took 16.3s
16.3 decl post-processing of category_theory.concrete_category took 16.3s
16.3 decl post-processing of group took 16.3s
16.3 decl post-processing of coe_one took 16.3s
16.2 decl post-processing of unique took 16.2s
16.2 decl post-processing of to_submonoid_inj took 16.2s
16.2 decl post-processing of inf_iff_and took 16.2s
16.2 decl post-processing of ext' took 16.2s
16.2 decl post-processing of le_iff took 16.2s
16 decl post-processing of continuous_at.inv took 16s
15.9 decl post-processing of mul_equiv.to_Group_iso took 15.9s
15.9 decl post-processing of multiset_prod_apply took 15.9s
15.8 decl post-processing of eq_mk'_iff_mul_eq took 15.8s
15.8 decl post-processing of mul_inv_right took 15.8s
15.8 decl post-processing of map_range took 15.8s
15.8 decl post-processing of continuous_mul_right took 15.8s
15.8 decl post-processing of one_apply took 15.8s
15.8 decl post-processing of prod_powerset_insert took 15.8s
15.7 decl post-processing of has_le took 15.7s
15.7 decl post-processing of r took 15.7s
15.6 elaboration of cpow took 15.6s
15.6 decl post-processing of prod_attach took 15.6s
15.5 elaboration of tangent_bundle_core took 15.5s
15.4 decl post-processing of rang_top_of_surjective took 15.4s
15.4 elaboration: tactic execution took 15.4s
15.4 decl post-processing of prod_of_fn took 15.4s
15.4 decl post-processing of con_gen_mono took 15.4s
15.3 decl post-processing of lift took 15.3s
15.3 elaboration of category_theory.reflective took 15.3s
15.3 decl post-processing of refl took 15.3s
15.3 decl post-processing of continuous_within_at.mul took 15.3s
15.2 decl post-processing of normal_iff_eq_cosets took 15.2s
15.2 decl post-processing of prod took 15.2s
15.1 decl post-processing of injective_ker_lift took 15.1s
15 decl post-processing of prod_equiv took 15s
15 elaboration: tactic execution took 15s
14.9 decl post-processing of has_inf took 14.9s
14.9 decl post-processing of monoid took 14.9s
14.9 decl post-processing of inv_mem_iff took 14.9s
14.9 decl post-processing of mul_equiv_of_mul_equiv_mk' took 14.9s
14.7 decl post-processing of pointwise_mul_semigroup took 14.7s
14.7 decl post-processing of prod_single_index took 14.7s
14.7 decl post-processing of monoid took 14.7s
14.6 decl post-processing of ker_lift_range_eq took 14.6s
14.6 decl post-processing of preimage.is_submonoid took 14.6s
14.5 decl post-processing of mk'_sec took 14.5s
14.4 decl post-processing of coe_prod took 14.4s
14.4 decl post-processing of prod_subtype_domain_index took 14.4s
14.4 decl post-processing of comap_comap took 14.4s
14.4 decl post-processing of inhabited took 14.4s
14.3 decl post-processing of ker_eq_lift_of_injective took 14.3s
14.3 decl post-processing of quotient_group.open_coe took 14.3s
14.3 decl post-processing of union_pointwise_mul took 14.3s
14.3 decl post-processing of mul_equiv_of_to_mul_equiv took 14.3s
14.2 decl post-processing of exists_nhds_split_inv took 14.2s
14.2 decl post-processing of continuous_mul_left took 14.2s
14.1 decl post-processing of eq_on_closure took 14.1s
14.1 decl post-processing of mem_closure_union_iff took 14.1s
14 decl post-processing of closure_univ took 14s
14 decl post-processing of pointwise_mul_one took 14s
14 decl post-processing of nhds_pointwise_mul took 14s
13.9 decl post-processing of snd took 13.9s
13.8 decl post-processing of mul_mem_pointwise_mul took 13.8s
13.7 decl post-processing of exists_list_of_mem_closure took 13.7s
13.7 decl post-processing of con_gen took 13.7s
13.7 decl post-processing of snd.is_monoid_hom took 13.7s
13.6 decl post-processing of singleton.is_monoid_hom took 13.6s
13.6 decl post-processing of prod_extend_by_one took 13.6s
13.5 decl post-processing of is_group_hom took 13.5s
13.4 decl post-processing of mem_pointwise_mul took 13.4s
13.4 decl post-processing of eq_of_eq_on_dense took 13.4s
13.4 decl post-processing of symm took 13.4s
13.4 decl post-processing of multiset_prod_mem took 13.4s
13.3 decl post-processing of is_group_hom took 13.3s
13.2 decl post-processing of of took 13.2s
13.2 decl post-processing of induction_on took 13.2s
13.2 elaboration of comm_ring took 13.2s
13.2 decl post-processing of top_prod_top took 13.2s
13.2 decl post-processing of subtype_val.is_monoid_hom took 13.2s
13.1 decl post-processing of comm_group took 13.1s
13.1 decl post-processing of mem_top took 13.1s
13 decl post-processing of left_coset_equiv took 13s
13 decl post-processing of continuous.mul took 13s
13 decl post-processing of mem_prod took 13s
12.9 decl post-processing of nonempty.pointwise_mul took 12.9s
12.9 decl post-processing of top_prod took 12.9s
12.8 decl post-processing of nhds_is_mul_hom took 12.8s
12.8 decl post-processing of pointwise_mul_monoid took 12.8s
12.8 elaboration: tactic execution took 12.8s
12.8 decl post-processing of eq took 12.8s
12.7 decl post-processing of pointwise_one_mul took 12.7s
12.7 decl post-processing of continuous_finset_prod took 12.7s
12.7 decl post-processing of has_mul took 12.7s
12.7 decl post-processing of gclosure_preimage_le took 12.7s
12.7 decl post-processing of ker_mk took 12.7s
12.7 decl post-processing of is_open_pointwise_mul_right took 12.7s
12.7 decl post-processing of coe_mrange took 12.7s
12.6 decl post-processing of continuous_subgroup took 12.6s
12.4 decl post-processing of comap_ker took 12.4s
12.4 decl post-processing of monoid_hom.apply_apply took 12.4s
12.3 decl post-processing of of_mul_equiv_eq took 12.3s
12.3 decl post-processing of coe_inf took 12.3s
12.2 decl post-processing of mul_equiv_of_to_mul_equiv_apply took 12.2s
12.2 decl post-processing of continuous_multiset_prod took 12.2s
12.1 decl post-processing of ker took 12.1s
12 decl post-processing of mem_range took 12s
11.9 decl post-processing of mul_ker_mk_eq took 11.9s
11.9 decl post-processing of is_subgroup.Inter took 11.9s
11.9 decl post-processing of mem_comap took 11.9s
11.9 decl post-processing of ext' took 11.9s
11.9 decl post-processing of has_forget_to_CommMon took 11.9s
11.8 decl post-processing of to_mul_equiv_eq_iff_eq took 11.8s
11.8 elaboration of change_origin_radius took 11.8s
11.8 decl post-processing of continuous_list_prod took 11.8s
11.7 decl post-processing of prod_ite took 11.7s
11.7 decl post-processing of prod_filter took 11.7s
11.7 decl post-processing of mul_equiv_iso_Group_iso took 11.7s
11.7 decl post-processing of of took 11.7s
11.7 decl post-processing of univ.is_submonoid took 11.7s
11.7 decl post-processing of group_equiv_quotient_times_subgroup took 11.7s
11.7 decl post-processing of prod_top took 11.7s
11.6 elaboration of map_right_comp took 11.6s
11.6 decl post-processing of CommGroup took 11.6s
11.6 decl post-processing of mem_inf took 11.6s
11.5 elaboration of mem_support_single took 11.5s
11.5 decl post-processing of decidable_eq took 11.5s
11.5 decl post-processing of coe_mul took 11.5s
11.5 decl post-processing of coe_mul took 11.5s
11.5 decl post-processing of eq took 11.5s
11.4 elaboration of map_left_comp took 11.4s
11.4 decl post-processing of category_theory.concrete_category took 11.4s
11.4 decl post-processing of range.is_submonoid took 11.4s
11.3 decl post-processing of coe_inf took 11.3s
11.2 decl post-processing of has_coe_to_fun took 11.2s
11.2 elaboration of sum_mul_div_add_sum_mul_div_eq_mul took 11.2s
11.1 decl post-processing of to_setoid_inj took 11.1s
11.1 decl post-processing of image_pointwise_mul took 11.1s
11.1 decl post-processing of map took 11.1s
11 decl post-processing of symm_to_mul_equiv_apply took 11s
11 decl post-processing of ext_iff took 11s
11 elaboration of pentagon took 11s
10.9 decl post-processing of prod_zero_index took 10.9s
10.9 decl post-processing of prod_range_mul_prod_Ico took 10.9s
10.9 decl post-processing of prod_hom_rel took 10.9s
10.9 decl post-processing of pointwise_inv took 10.9s
10.8 decl post-processing of ker_rel took 10.8s
10.8 decl post-processing of has_Inf took 10.8s
10.8 decl post-processing of mul_equiv_iso_CommGroup_iso took 10.8s
10.8 decl post-processing of mem_bot took 10.8s
10.7 decl post-processing of prod_ite_eq took 10.7s
10.7 elaboration of cpow_nat_cast took 10.7s
10.7 decl post-processing of prod_subset took 10.7s
10.7 decl post-processing of mul_mem_cancel_left took 10.7s
10.7 decl post-processing of closure_subset took 10.7s
10.7 decl post-processing of comm_group_instance took 10.7s
10.7 elaboration of lmap_domain_disjoint_ker took 10.7s
10.6 decl post-processing of category_theory.category took 10.6s
10.6 decl post-processing of filter.tendsto.mul took 10.6s
10.6 elaboration of linear_independent_iff_not_mem_span took 10.6s
10.5 decl post-processing of has_coe took 10.5s
10.5 decl post-processing of exists_nhds_split4 took 10.5s
10.4 elaboration of simple_func_sequence_tendsto took 10.4s
10.4 decl post-processing of set_inclusion.is_monoid_hom took 10.4s
10.4 elaboration: tactic execution took 10.4s
10.4 elaboration of cpow_one took 10.4s
10.3 decl post-processing of finset.range_prod_eq_univ_prod took 10.3s
10.2 decl post-processing of pointwise_mul_union took 10.2s
10.2 decl post-processing of prod_add_index took 10.2s
10.2 decl post-processing of mk' took 10.2s
10.1 decl post-processing of gi took 10.1s
10.1 decl post-processing of subtype_mk.is_monoid_hom took 10.1s
10.1 decl post-processing of closure took 10.1s
10.1 decl post-processing of fst took 10.1s
10.1 decl post-processing of Mon took 10.1s
10 elaboration of cones_equiv_inverse took 10s
9.97 elaboration of groupoid_of_elements took 9.97s
9.95 decl post-processing of localization took 9.95s
9.93 elaboration: tactic execution took 9.93s
9.93 decl post-processing of is_submonoid.Inter took 9.93s
9.91 decl post-processing of map_pointwise_mul took 9.91s
9.91 decl post-processing of apply_symm_apply took 9.91s
9.74 decl post-processing of con_gen_of_con took 9.74s
9.72 decl post-processing of is_subgroup.coe_inv took 9.72s
9.7 decl post-processing of mul_def took 9.7s
9.69 decl post-processing of Sup_eq_con_gen took 9.69s
9.59 decl post-processing of category_theory.category took 9.59s
9.55 decl post-processing of list_prod_mem took 9.55s
9.53 decl post-processing of mul took 9.53s
9.51 decl post-processing of continuous_mul took 9.51s
9.49 elaboration of linear_independent_unique took 9.49s
9.49 decl post-processing of closure_eq took 9.49s
9.47 decl post-processing of le_def took 9.47s
9.43 decl post-processing of mk'_eq_iff_mk'_eq took 9.43s
9.4 decl post-processing of mul_equiv.to_Mon_iso_hom took 9.4s
9.33 decl post-processing of mem_supr_of_directed took 9.33s
9.29 decl post-processing of inv took 9.29s
9.21 decl post-processing of closure_induction took 9.21s
9.17 elaboration of wide_span took 9.17s
9.15 decl post-processing of of took 9.15s
9.12 elaboration: tactic execution took 9.12s
9.1 decl post-processing of has_one took 9.1s
9.1 decl post-processing of is_subgroup took 9.1s
9.1 decl post-processing of mk'_eq_iff_eq took 9.1s
9.07 decl post-processing of to_mul_equiv_of_mul_equiv_of_mul_equiv took 9.07s
9.05 decl post-processing of has_one took 9.05s
9.04 decl post-processing of mul_mem_cancel_right took 9.04s
9.04 decl post-processing of mul_equiv_of_localizations took 9.04s
9 decl post-processing of empty_pointwise_mul took 9s
8.98 elaboration of monoidal_of_has_finite_coproducts took 8.98s
8.93 decl post-processing of Sup_def took 8.93s
8.85 decl post-processing of prod.topological_group took 8.85s
8.85 elaboration: tactic execution took 8.85s
8.84 elaboration of to_smooth_manifold took 8.84s
8.79 decl post-processing of inhabited took 8.79s
8.79 decl post-processing of le_iff took 8.79s
8.77 elaboration: tactic execution took 8.77s
8.77 decl post-processing of comap_infi took 8.77s
8.75 decl post-processing of map_of_surjective took 8.75s
8.71 decl post-processing of mul_equiv.to_Mon_iso took 8.71s
8.69 decl post-processing of prod_single_index took 8.69s
8.69 decl post-processing of lift_right took 8.69s
8.64 decl post-processing of semigroup took 8.64s
8.62 elaboration of glue_dist_triangle took 8.62s
8.6 decl post-processing of pointwise_mul_eq_Union_mul_left took 8.6s
8.59 decl post-processing of pointwise_mul_eq_image took 8.59s
8.59 decl post-processing of ext took 8.59s
8.55 decl post-processing of partial_order took 8.55s
8.52 decl post-processing of prod_eq_single took 8.52s
8.49 decl post-processing of closure_eq_of_le took 8.49s
8.48 decl post-processing of comap took 8.48s
8.46 decl post-processing of cod_restrict took 8.46s
8.46 elaboration of unique_mdiff_on.smooth_bundle_preimage took 8.46s
8.46 decl post-processing of is_submonoid.coe_mul took 8.46s
8.45 elaboration of mem_nhds_unbounded took 8.45s
8.44 elaboration: tactic execution took 8.44s
8.42 decl post-processing of subtype took 8.42s
8.41 elaboration of unique_mdiff_on.unique_mdiff_on_preimage took 8.41s
8.39 decl post-processing of prod_mk_prod took 8.39s
8.36 elaboration of exists_approx_preimage_norm_le took 8.36s
8.32 decl post-processing of prod_zero_index took 8.32s
8.31 elaboration of sum_Ico_eq_card_lt took 8.31s
8.31 elaboration of tangent_bundle_model_space_chart_at took 8.31s
8.29 elaboration of comma_equivalence took 8.29s
8.29 decl post-processing of mul_equiv.to_CommMon_iso_hom took 8.29s
8.24 elaboration of currying took 8.24s
8.24 decl post-processing of le_def took 8.24s
8.23 decl post-processing of eq took 8.23s
8.23 decl post-processing of is_monoid_hom.of_mul took 8.23s
8.2 decl post-processing of finset_prod_apply took 8.2s
8.15 elaboration of exists_of_linear_independent_of_finite_span took 8.15s
8.15 elaboration of iterated_slice_equiv took 8.15s
8.13 decl post-processing of inr_apply took 8.13s
8.12 decl post-processing of singleton.is_mul_hom took 8.12s
8.11 decl post-processing of coe_map took 8.11s
8.09 decl post-processing of has_forget_to_Group took 8.09s
8.09 decl post-processing of eq_of_eq_on_top took 8.09s
8.08 decl post-processing of prod_congr took 8.08s
8.05 elaboration of ext_abs_arg took 8.05s
8.02 decl post-processing of map_bot took 8.02s
8.02 decl post-processing of to_mul_equiv_eq took 8.02s
8.02 elaboration of map_sum_finset_aux took 8.02s
7.98 decl post-processing of range took 7.98s
7.96 elaboration of single took 7.96s
7.93 elaboration of exists_extension_norm_eq took 7.93s
7.93 elaboration of of_inj took 7.93s
7.93 decl post-processing of mem_Sup_of_directed_on took 7.93s
7.91 decl post-processing of gc_map_comap took 7.91s
7.88 elaboration: tactic execution took 7.88s
7.87 elaboration of arg_real_mul took 7.87s
7.86 decl post-processing of range_inl_sup_range_inr took 7.86s
7.85 decl post-processing of category_theory.bundled_hom.parent_projection took 7.85s
7.84 decl post-processing of monoid_hom.map_multiset_prod took 7.84s
7.83 elaboration of arg_cos_add_sin_mul_I took 7.83s
7.82 decl post-processing of prod_sum_index took 7.82s
7.82 decl post-processing of coe_one took 7.82s
7.81 decl post-processing of prod_hom took 7.81s
7.79 elaboration of map_right_id took 7.79s
7.79 decl post-processing of mul took 7.79s
7.78 elaboration of mv_polynomial took 7.78s
7.78 decl post-processing of prod_ite_eq' took 7.78s
7.77 elaboration of to_comma took 7.77s
7.77 elaboration of cones_inv took 7.77s
7.76 decl post-processing of closure.is_submonoid took 7.76s
7.75 decl post-processing of inv_iff_ker' took 7.75s
7.71 elaboration of euclidean_domain.to_principal_ideal_domain took 7.71s
7.7 decl post-processing of Group took 7.7s
7.68 decl post-processing of map_sup took 7.68s
7.66 elaboration of cau_seq.cauchy_seq took 7.66s
7.66 decl post-processing of ker_lift_mk took 7.66s
7.66 elaboration of map_left_id took 7.66s
7.64 elaboration of comap_comp took 7.64s
7.62 decl post-processing of mk'_eq_iff_eq_mul took 7.62s
7.62 decl post-processing of prod_neg_index took 7.62s
7.62 decl post-processing of coe_one took 7.62s
7.6 decl post-processing of inhabited took 7.6s
7.6 elaboration of has_add took 7.6s
7.55 decl post-processing of coe_Inf took 7.55s
7.55 elaboration of has_fderiv_at_boundary_of_tendsto_fderiv_aux took 7.55s
7.55 decl post-processing of coe_inv took 7.55s
7.54 elaboration of prod.pentagon took 7.54s
7.53 decl post-processing of pointwise_mul_empty took 7.53s
7.53 elaboration: tactic execution took 7.53s
7.52 decl post-processing of closure_union took 7.52s
7.51 decl post-processing of prod_update_of_not_mem took 7.51s
7.51 decl post-processing of fst.is_group_hom took 7.51s
7.49 decl post-processing of lift_comp_of took 7.49s
7.47 decl post-processing of prod_pair took 7.47s
7.46 decl post-processing of is_subgroup.prod took 7.46s
7.41 decl post-processing of lift_mk took 7.41s
7.37 decl post-processing of univ_pointwise_mul_univ took 7.37s
7.37 elaboration: tactic execution took 7.37s
7.36 elaboration of wide_cospan took 7.36s
7.32 decl post-processing of perm.prod_eq took 7.32s
7.29 elaboration of splits_C took 7.29s
7.29 elaboration of GH_dist_le_of_approx_subsets took 7.29s
7.28 elaboration of raise_cone took 7.28s
7.27 decl post-processing of fst_prod took 7.27s
7.24 decl post-processing of coe_subtype took 7.24s
7.18 decl post-processing of one_mem took 7.18s
7.18 decl post-processing of mem_pointwise_one took 7.18s
7.18 decl post-processing of has_mem took 7.18s
7.14 decl post-processing of closure_mono took 7.14s
7.13 decl post-processing of mem_bot took 7.13s
7.12 decl post-processing of coe_inv took 7.12s
7.08 decl post-processing of prod_sum_elim took 7.08s
7.06 decl post-processing of is_closed took 7.06s
7.05 elaboration of comp took 7.05s
7.04 decl post-processing of mul_mem took 7.04s
7.02 elaboration of cones_iso took 7.02s
7.02 elaboration of has_ftaylor_series_up_to_on_succ_iff_right took 7.02s
7.02 decl post-processing of eq_class_eq_left_coset took 7.02s
7 elaboration: tactic execution took 7s
7 elaboration of has_mfderiv_within_at.comp took 7s
6.99 decl post-processing of finset.prod_attach_univ took 6.99s
6.97 decl post-processing of prod_comm took 6.97s
6.95 elaboration of has_sum_sum took 6.95s
6.9 elaboration: tactic execution took 6.9s
6.89 decl post-processing of quotient_group.quotient.topological_space took 6.89s
6.89 elaboration of map_domain_comap_domain took 6.89s
6.88 decl post-processing of comm_monoid took 6.88s
6.87 decl post-processing of map_map took 6.87s
6.87 decl post-processing of prod_apply_ite took 6.87s
6.87 elaboration: tactic execution took 6.87s
6.83 decl post-processing of coe_top took 6.83s
6.82 elaboration of second_countable took 6.82s
6.82 decl post-processing of inhabited took 6.82s
6.8 elaboration: tactic execution took 6.8s
6.79 elaboration of has_mul took 6.79s
6.79 elaboration of comap_eq took 6.79s
6.79 decl post-processing of coe_coe took 6.79s
6.74 elaboration: tactic execution took 6.74s
6.73 decl post-processing of closure_Union took 6.73s
6.73 decl post-processing of comap_quotient_equiv took 6.73s
6.67 elaboration of is_closed_iff took 6.67s
6.67 elaboration: tactic execution took 6.67s
6.67 decl post-processing of lift_eval_of took 6.67s
6.66 elaboration of topological_space.second_countable_topology took 6.66s
6.66 decl post-processing of to_submonoid took 6.66s
6.65 decl post-processing of inv.is_group_hom took 6.65s
6.65 decl post-processing of ker_apply_eq_preimage took 6.65s
6.63 decl post-processing of is_unit.lift_right_inv_mul took 6.63s
6.61 elaboration of totally_bounded took 6.61s
6.61 decl post-processing of mul_mem took 6.61s
6.6 decl post-processing of lift_apply_mk' took 6.6s
6.59 elaboration of coprod.pentagon took 6.59s
6.58 decl post-processing of mul_mem_pointwise_mul took 6.58s
6.57 decl post-processing of is_group_hom.mk' took 6.57s
6.56 decl post-processing of pointwise_mul_eq_Union_mul_right took 6.56s
6.55 decl post-processing of coe_prod_map took 6.55s
6.54 decl post-processing of is_unit.lift_right took 6.54s
6.52 elaboration: tactic execution took 6.52s
6.51 elaboration of X_pow_dvd_iff took 6.51s
6.51 elaboration: tactic execution took 6.51s
6.5 elaboration of norm_eq_infi_iff_inner_le_zero took 6.5s
6.5 elaboration of closed_candidates_b took 6.5s
6.49 decl post-processing of category_theory.concrete_category took 6.49s
6.48 decl post-processing of inhabited took 6.48s
6.39 elaboration of monoidal_of_has_finite_products took 6.39s
6.38 elaboration of exists_bound_of_continuous took 6.38s
6.38 elaboration: tactic execution took 6.38s
6.35 elaboration of colim_coyoneda took 6.35s
6.34 elaboration of exp_eq_one_iff took 6.34s
6.33 elaboration of category_theory.category took 6.33s
6.33 decl post-processing of coe_snd took 6.33s
6.29 decl post-processing of lift_unique took 6.29s
6.29 decl post-processing of category_theory.concrete_category took 6.29s
6.28 elaboration: tactic execution took 6.28s
6.28 elaboration: tactic execution took 6.28s
6.28 elaboration: tactic execution took 6.28s
6.26 elaboration of prod_add took 6.26s
6.26 decl post-processing of of_submonoid took 6.26s
6.25 elaboration: tactic execution took 6.25s
6.25 decl post-processing of lift took 6.25s
6.25 decl post-processing of refl took 6.25s
6.24 decl post-processing of to_is_monoid_hom took 6.24s
6.23 elaboration of pure took 6.23s
6.23 decl post-processing of ext'_iff took 6.23s
6.22 decl post-processing of monoid took 6.22s
6.21 decl post-processing of nhds_translation_mul_inv took 6.21s
6.21 decl post-processing of prod_map_domain_index took 6.21s
6.19 elaboration of has_colimit_pair took 6.19s
6.19 decl post-processing of closure_singleton took 6.19s
6.17 decl post-processing of mem_mrange took 6.17s
6.14 decl post-processing of preimage_pointwise_mul_preimage_subset took 6.14s
6.13 decl post-processing of comap_top took 6.13s
6.1 decl post-processing of ext'_iff took 6.1s
6.09 elaboration of continuous_equiv_fun_basis took 6.09s
6.08 decl post-processing of coe_coe took 6.08s
6.07 elaboration of norm_nonarchimedean took 6.07s
6.07 elaboration of diagram_iso_cospan took 6.07s
6.06 elaboration: tactic execution took 6.06s
6.05 decl post-processing of ext took 6.05s
6.04 decl post-processing of subgroup.of took 6.04s
6.03 decl post-processing of exists_ne_one_of_prod_ne_one took 6.03s
6.03 decl post-processing of prod_empty took 6.03s
6.03 decl post-processing of pointwise_mul_subset_mul took 6.03s
6.02 elaboration of lift took 6.02s
6.01 decl post-processing of map_one took 6.01s
6 decl post-processing of mem_coe took 6s
6 elaboration of pow_add_expansion took 6s
6 elaboration of complete_space took 6s
5.99 elaboration: tactic execution took 5.99s
5.95 decl post-processing of is_unit.mul_lift_right_inv took 5.95s
5.94 elaboration of CommRing_yoneda took 5.94s
5.93 decl post-processing of mul_lift_right_inv took 5.93s
5.93 decl post-processing of group took 5.93s
5.93 decl post-processing of coe_mul took 5.93s
5.93 decl post-processing of has_mem took 5.93s
5.91 elaboration: tactic execution took 5.91s
5.89 elaboration: tactic execution took 5.89s
5.89 elaboration: tactic execution took 5.89s
5.89 decl post-processing of lift took 5.89s
5.87 elaboration of lift took 5.87s
5.87 decl post-processing of has_coe_to_sort took 5.87s
5.86 decl post-processing of map_sup took 5.86s
5.85 decl post-processing of fst_mul_snd took 5.85s
5.85 elaboration of has_limit_pair took 5.85s
5.82 decl post-processing of snd_comp_inr took 5.82s
5.8 elaboration of to_topological_fiber_bundle_core took 5.8s
5.79 elaboration: tactic execution took 5.79s
5.78 decl post-processing of comp_mk'_apply took 5.78s
5.78 decl post-processing of multiset_prod_mem took 5.78s
5.76 elaboration of has_scalar took 5.76s
5.74 decl post-processing of prod_bot_sup_bot_prod took 5.74s
5.74 elaboration: tactic execution took 5.74s
5.73 elaboration of comm_ring took 5.73s
5.73 elaboration of GH_dist_le_Hausdorff_dist took 5.73s
5.72 elaboration: tactic execution took 5.72s
5.72 decl post-processing of has_coe_to_sort took 5.72s
5.72 decl post-processing of prod_singleton took 5.72s
5.72 elaboration: tactic execution took 5.72s
5.71 decl post-processing of fst.is_monoid_hom took 5.71s
5.71 decl post-processing of lift_range took 5.71s
5.7 decl post-processing of mul_equiv.to_Mon_iso_inv took 5.7s
5.66 decl post-processing of prod_mem took 5.66s
5.66 decl post-processing of comp took 5.66s
5.64 decl post-processing of fintype.prod_sum_type took 5.64s
5.61 elaboration: tactic execution took 5.61s
5.6 decl post-processing of ext' took 5.6s
5.6 decl post-processing of mem_closure took 5.6s
5.57 decl post-processing of trans took 5.57s
5.57 decl post-processing of mul_inv_cancel_right took 5.57s
5.57 decl post-processing of closure_le took 5.57s
5.56 decl post-processing of submonoid.of took 5.56s
5.56 decl post-processing of map_of took 5.56s
5.55 elaboration of add_eq_max_of_ne took 5.55s
5.54 decl post-processing of eq_inv_iff_mul_eq_one took 5.54s
5.54 elaboration: tactic execution took 5.54s
5.51 decl post-processing of prod_finset_sum_index took 5.51s
5.5 elaboration of cones_iso took 5.5s
5.48 elaboration of cones_equiv_functor took 5.48s
5.47 decl post-processing of mem_pointwise_one took 5.47s
5.47 elaboration of mk took 5.47s
5.46 elaboration of linear_map.continuous_iff_is_closed_ker took 5.46s
5.45 elaboration of sum_mem took 5.45s
5.45 elaboration of lt_inf took 5.45s
5.44 decl post-processing of induction_on took 5.44s
5.44 decl post-processing of normalizer took 5.44s
5.44 elaboration of mul_assoc took 5.44s
5.44 decl post-processing of is_open_of_nonempty_open_subset took 5.44s
5.43 elaboration of fork.of_cone took 5.43s
5.43 elaboration: tactic execution took 5.43s
5.43 decl post-processing of lift_coe took 5.43s
5.43 decl post-processing of sup_eq_con_gen took 5.43s
5.41 decl post-processing of ext took 5.41s
5.41 decl post-processing of image_closure took 5.41s
5.41 elaboration: tactic execution took 5.41s
5.4 decl post-processing of finset.prod_apply took 5.4s
5.39 decl post-processing of is_monoid_hom took 5.39s
5.39 decl post-processing of map took 5.39s
5.39 decl post-processing of range_snd took 5.39s
5.38 decl post-processing of list_prod_mem took 5.38s
5.34 elaboration of comap_id took 5.34s
5.33 elaboration of cos_lt_cos_of_nonneg_of_le_pi took 5.33s
5.32 elaboration of trans took 5.32s
5.29 elaboration of cocones_iso took 5.29s
5.27 elaboration of diagram_iso_span took 5.27s
5.26 elaboration of functoriality_is_right_adjoint took 5.26s
5.25 decl post-processing of left_coset_right_coset took 5.25s
5.25 elaboration of Inf_sup_Inf took 5.25s
5.24 decl post-processing of lift_mk' took 5.24s
5.23 decl post-processing of inv_mem took 5.23s
5.23 elaboration: tactic execution took 5.23s
5.22 decl post-processing of lift_of_comp_eq_map took 5.22s
5.22 elaboration of sum_four_squares_of_two_mul_sum_four_squares took 5.22s
5.22 elaboration: tactic execution took 5.22s
5.2 elaboration of cofork.of_cocone took 5.2s
5.17 decl post-processing of comm_monoid took 5.17s
5.16 elaboration of mk took 5.16s
5.15 elaboration of normed_uniform_group took 5.15s
5.15 elaboration of Sup_inf_Sup took 5.15s
5.14 decl post-processing of finset.prod_subtype took 5.14s
5.14 elaboration: tactic execution took 5.14s
5.13 decl post-processing of mem_own_right_coset took 5.13s
5.13 decl post-processing of flip took 5.13s
5.12 elaboration of semilattice_inf_bot took 5.12s
5.12 decl post-processing of map_inl took 5.12s
5.11 elaboration of lim_yoneda took 5.11s
5.1 elaboration of lintegral_supr took 5.1s
5.1 decl post-processing of mk'_surjective took 5.1s
5.09 decl post-processing of comap_eq took 5.09s
5.09 elaboration: tactic execution took 5.09s
5.08 elaboration of quotient_prod_linear_equiv took 5.08s
5.08 elaboration of sum_four_squares took 5.08s
5.07 decl post-processing of one_mem took 5.07s
5.06 elaboration of comp_summable_nnreal took 5.06s
5.05 elaboration of linear_equiv_iso_Group_iso took 5.05s
5.03 decl post-processing of coe_injective took 5.03s
5.02 decl post-processing of mem_right_coset took 5.02s
5.02 elaboration of gauss_lemma_aux₁ took 5.02s
5.02 elaboration of functoriality_is_left_adjoint took 5.02s
5.01 decl post-processing of snd_prod took 5.01s
5 decl post-processing of mem_Inf took 5s
5 decl post-processing of prod_eq_one took 5s
4.99 decl post-processing of inhabited took 4.99s
4.99 decl post-processing of lift_apply took 4.99s
4.99 decl post-processing of inv_mk took 4.99s
4.98 decl post-processing of snd_inv took 4.98s
4.97 decl post-processing of id took 4.97s
4.97 elaboration of hahn_decomposition took 4.97s
4.95 decl post-processing of mem_coe took 4.95s
4.92 elaboration of times_cont_diff_on.comp took 4.92s
4.92 decl post-processing of lift_surjective_of_surjective took 4.92s
4.91 decl post-processing of coe_one took 4.91s
4.91 elaboration of chart_target took 4.91s
4.9 decl post-processing of eq_inv_mul_iff_mul_eq took 4.9s
4.9 decl post-processing of pointwise_one took 4.9s
4.88 elaboration of comp_partial_sum_target_tendsto_at_top took 4.88s
4.87 elaboration of Icc_right_chart took 4.87s
4.87 decl post-processing of comm_semigroup took 4.87s
4.85 decl post-processing of map_supr took 4.85s
4.85 decl post-processing of coe_prod took 4.85s
4.85 decl post-processing of perm.prod_eq' took 4.85s
4.82 decl post-processing of coe_ssubset_coe took 4.82s
4.8 decl post-processing of prod_apply took 4.8s
4.79 elaboration: tactic execution took 4.79s
4.77 elaboration of evaln_sound took 4.77s
4.77 decl post-processing of restrict_apply took 4.77s
4.75 elaboration of exi_rat_seq_conv_cauchy took 4.75s
4.73 decl post-processing of coe_comap took 4.73s
4.72 decl post-processing of prod_map_range_index took 4.72s
4.72 elaboration of coeff_mul took 4.72s
4.69 elaboration of factors took 4.69s
4.67 elaboration: tactic execution took 4.67s
4.66 decl post-processing of prod_mono_left took 4.66s
4.66 elaboration: tactic execution took 4.66s
4.65 decl post-processing of range_inr' took 4.65s
4.65 elaboration: tactic execution took 4.65s
4.64 decl post-processing of normal_in_normalizer took 4.64s
4.64 decl post-processing of fst_inv took 4.64s
4.64 decl post-processing of prod_involution took 4.64s
4.63 elaboration of splits_of_exists_multiset took 4.63s
4.61 decl post-processing of finset.prod_equiv took 4.61s
4.61 elaboration: tactic execution took 4.61s
4.59 decl post-processing of range_fst took 4.59s
4.59 elaboration: tactic execution took 4.59s
4.59 decl post-processing of closure_mono took 4.59s
4.57 elaboration: tactic execution took 4.57s
4.57 decl post-processing of pointwise_mul took 4.57s
4.57 decl post-processing of topological_group.ext took 4.57s
4.57 decl post-processing of snd.is_group_hom took 4.57s
4.55 elaboration: tactic execution took 4.55s
4.55 elaboration: tactic execution took 4.55s
4.54 decl post-processing of CommMon took 4.54s
4.54 decl post-processing of mem_own_left_coset took 4.54s
4.52 elaboration of separated_def took 4.52s
4.52 decl post-processing of mk took 4.52s
4.51 elaboration of diagram_iso_wide_span took 4.51s
4.5 elaboration of mod_four_eq_three_of_nat_prime_of_prime took 4.5s
4.5 decl post-processing of ker_lift took 4.5s
4.49 elaboration of norm_mul took 4.49s
4.48 decl post-processing of mem_map took 4.48s
4.47 elaboration of is_noetherian_pi took 4.47s
4.47 decl post-processing of inl_apply took 4.47s
4.46 decl post-processing of mul_left_inj took 4.46s
4.46 elaboration of eisenstein_lemma_aux₁ took 4.46s
4.45 decl post-processing of mem_nhds_one took 4.45s
4.45 decl post-processing of rel_prod took 4.45s
4.45 elaboration of has_deriv_at_real_of_complex_aux took 4.45s
4.42 decl post-processing of prod_image took 4.42s
4.42 elaboration of norm_image_sub_le_of_bound' took 4.42s
4.42 decl post-processing of continuous_monoid took 4.42s
4.41 elaboration of C_sum took 4.41s
4.4 elaboration of forget_reflects_iso took 4.4s
4.39 elaboration: tactic execution took 4.39s
4.39 decl post-processing of subgroup.exists took 4.39s
4.38 elaboration of desc_fun took 4.38s
4.37 elaboration: tactic execution took 4.37s
4.37 decl post-processing of coe_lift_right took 4.37s
4.37 elaboration of norm_eq took 4.37s
4.37 decl post-processing of lift_right_inv_mul took 4.37s
4.36 elaboration: tactic execution took 4.36s
4.36 elaboration of add_comm_group took 4.36s
4.35 elaboration: tactic execution took 4.35s
4.34 elaboration of complete_space took 4.34s
4.34 elaboration of has_sum.sigma took 4.34s
4.34 decl post-processing of fin.prod_univ_eq_prod_range took 4.34s
4.33 elaboration: tactic execution took 4.33s
4.32 decl post-processing of coe_subtype took 4.32s
4.32 elaboration: tactic execution took 4.32s
4.31 elaboration of le_radius_of_bound took 4.31s
4.31 elaboration of preimage_eq_empty_iff took 4.31s
4.3 decl post-processing of bot_prod_bot took 4.3s
4.3 decl post-processing of coprod_comp_inl took 4.3s
4.3 elaboration: tactic execution took 4.3s
4.3 elaboration: tactic execution took 4.3s
4.29 elaboration: tactic execution took 4.29s
4.28 elaboration of id took 4.28s
4.28 elaboration of repr_power_aux₂ took 4.28s
4.27 decl post-processing of mem_top took 4.27s
4.26 elaboration of is_bounded_bilinear_map_comp_multilinear took 4.26s
4.25 elaboration of is_bounded_bilinear_map.is_bounded_linear_map_deriv took 4.25s
4.25 elaboration of lintegral_eq_nnreal took 4.25s
4.24 elaboration of has_strict_deriv_at_inv took 4.24s
4.24 decl post-processing of of took 4.24s
4.24 elaboration of Icc_smooth_manifold took 4.24s
4.24 elaboration of C_compl took 4.24s
4.23 elaboration of lebesgue_length_subadditive took 4.23s
4.23 decl post-processing of inf_def took 4.23s
4.22 decl post-processing of map_le_iff_le_comap took 4.22s
4.22 elaboration of has_colimit_discrete took 4.22s
4.22 elaboration of local_ring took 4.22s
4.21 elaboration of integral_map took 4.21s
4.19 elaboration of exists_preimage_norm_le took 4.19s
4.19 decl post-processing of is_unit.coe_lift_right took 4.19s
4.19 elaboration: tactic execution took 4.19s
4.18 decl post-processing of submonoid.exists took 4.18s
4.18 elaboration of id_comp took 4.18s
4.17 elaboration: tactic execution took 4.17s
4.16 elaboration: tactic execution took 4.16s
4.14 decl post-processing of pointwise_one took 4.14s
4.14 elaboration of has_colimit_span_of_has_colimit_pair_of_has_colimit_parallel_pair took 4.14s
4.14 decl post-processing of mem_inf took 4.14s
4.13 elaboration of change_origin_has_sum took 4.13s
4.13 decl post-processing of is_subgroup took 4.13s
4.13 elaboration: tactic execution took 4.13s
4.12 decl post-processing of free_monoid took 4.12s
4.11 elaboration of diagram_iso_wide_cospan took 4.11s
4.11 elaboration of raised_cone_lowers_to_original took 4.11s
4.11 elaboration of map_midpoint took 4.11s
4.11 elaboration: tactic execution took 4.11s
4.08 elaboration of raised_cone_is_limit took 4.08s
4.08 elaboration: tactic execution took 4.08s
4.08 elaboration: tactic execution took 4.08s
4.08 elaboration of colimit_is_colimit took 4.08s
4.07 elaboration: tactic execution took 4.07s
4.07 decl post-processing of map_mul took 4.07s
4.06 elaboration of rat_dense' took 4.06s
4.06 elaboration: tactic execution took 4.06s
4.05 elaboration of midpoint_fixed took 4.05s
4.05 elaboration of add_comm_group took 4.05s
4.05 elaboration of continuous_multilinear_map.curry_right took 4.05s
4.04 elaboration of colimit_is_colimit_ took 4.04s
4.04 decl post-processing of finset.prod_univ_pi took 4.04s
4.03 decl post-processing of normal_subgroup_of_comm_group took 4.03s
4.03 elaboration of category_of_elements took 4.03s
4.02 elaboration of add_group took 4.02s
4.01 decl post-processing of inhabited took 4.01s
4 elaboration: tactic execution took 4s
4 elaboration: tactic execution took 4s
4 decl post-processing of has_one took 4s
3.99 elaboration of extend_Z_bilin_key took 3.99s
3.99 elaboration: tactic execution took 3.99s
3.98 elaboration of mul_apply_antidiagonal took 3.98s
3.98 decl post-processing of prod_singleton took 3.98s
3.98 decl post-processing of prod took 3.98s
3.97 elaboration of borel_eq_generate_Ioi took 3.97s
3.97 elaboration: tactic execution took 3.97s
3.97 elaboration of erase took 3.97s
3.97 elaboration of continuous_eval took 3.97s
3.97 elaboration of total took 3.97s
3.97 elaboration of has_neg took 3.97s
3.97 elaboration of evaln_complete took 3.97s
3.96 decl post-processing of prod_eq_foldl took 3.96s
3.96 elaboration: tactic execution took 3.96s
3.96 elaboration of linear_map.continuous_of_finite_dimensional took 3.96s
3.94 elaboration: tactic execution took 3.94s
3.93 elaboration of cones_hom took 3.93s
3.92 elaboration of prod.associator took 3.92s
3.9 decl post-processing of one_def took 3.9s
3.9 elaboration: tactic execution took 3.9s
3.9 elaboration of continuous_of_le_add_edist took 3.9s
3.89 decl post-processing of map_gen took 3.89s
3.89 elaboration of bound took 3.89s
3.89 decl post-processing of mul_ite took 3.89s
3.88 decl post-processing of is_submonoid took 3.88s
3.88 elaboration of mem_perms_of_list_of_mem took 3.88s
3.87 elaboration of ennreal.tsum_geometric took 3.87s
3.87 elaboration of times_cont_diff_groupoid took 3.87s
3.87 decl post-processing of mrange_top_of_surjective took 3.87s
3.86 decl post-processing of coe_of took 3.86s
3.86 elaboration of colimit took 3.86s
3.86 elaboration of group took 3.86s
3.85 elaboration of comp_id took 3.85s
3.85 elaboration of mul_inv_of_unit took 3.85s
3.84 decl post-processing of fst_comp_inr took 3.84s
3.84 elaboration of composition_as_set_equiv took 3.84s
3.84 decl post-processing of mem_norm_comm took 3.84s
3.83 decl post-processing of mul_mem took 3.83s
3.83 elaboration of aeval took 3.83s
3.82 elaboration of norm_rat_le_one took 3.82s
3.82 elaboration of borel_eq_generate_Iio took 3.82s
3.82 decl post-processing of fst_comp_inl took 3.82s
3.81 elaboration: tactic execution took 3.81s
3.81 elaboration of functor_category_is_colimit_cocone took 3.81s
3.8 elaboration of of_function took 3.8s
3.79 elaboration: tactic execution took 3.79s
3.78 elaboration of map took 3.78s
3.77 elaboration of model_with_corners.mdifferentiable took 3.77s
3.77 elaboration of limit took 3.77s
3.77 elaboration of has_Inf took 3.77s
3.77 elaboration: tactic execution took 3.77s
3.77 elaboration of kernel_functor took 3.77s
3.76 decl post-processing of coe_one took 3.76s
3.76 elaboration of has_strict_deriv_at took 3.76s
3.76 elaboration: tactic execution took 3.76s
3.76 elaboration of arzela_ascoli₁ took 3.76s
3.75 decl post-processing of ker_lift_mk' took 3.75s
3.75 elaboration: tactic execution took 3.75s
3.74 elaboration: tactic execution took 3.74s
3.74 decl post-processing of has_coe took 3.74s
3.74 elaboration of legendre_sym_two took 3.74s
3.73 elaboration: tactic execution took 3.73s
3.73 decl post-processing of prod_range_succ took 3.73s
3.73 decl post-processing of quotient took 3.73s
3.73 elaboration of eval₂_map took 3.73s
3.72 elaboration of sup_lt_iff took 3.72s
3.72 elaboration of of took 3.72s
3.71 elaboration of category_of_PresheafedSpaces took 3.71s
3.71 decl post-processing of hom_eq took 3.71s
3.71 decl post-processing of inv_eq_iff_mul_eq_one took 3.71s
3.71 decl post-processing of quotient_group_saturate took 3.71s
3.71 elaboration: tactic execution took 3.71s
3.71 elaboration: tactic execution took 3.71s
3.7 elaboration of functor_category_is_limit_cone took 3.7s
3.7 elaboration of mul_equiv_iso_CommGroup_iso took 3.7s
3.69 decl post-processing of is_subgroup.of_div took 3.69s
3.68 decl post-processing of inhabited took 3.68s
3.68 elaboration: tactic execution took 3.68s
3.68 decl post-processing of lift_funext took 3.68s
3.67 elaboration of continuous_on_open_of_generate_from took 3.67s
3.67 elaboration of tendsto_inv took 3.67s
3.66 decl post-processing of snd_comp_inl took 3.66s
3.65 elaboration: tactic execution took 3.65s
3.65 elaboration of sin_bound took 3.65s
3.64 elaboration of exists_root_sum_quadratic took 3.64s
3.64 elaboration of comm_monoid took 3.64s
3.64 elaboration of has_strict_fderiv_at.add took 3.64s
3.63 decl post-processing of has_le took 3.63s
3.62 elaboration of det_mul took 3.62s
3.61 elaboration of has_mfderiv_within_at.congr_of_mem_nhds_within took 3.61s
3.61 elaboration of coprod.associator took 3.61s
3.6 elaboration of is_integral_domain_fin took 3.6s
3.59 elaboration of has_strict_fderiv_at.of_local_left_inverse took 3.59s
3.58 decl post-processing of is_closed_map_mul_right took 3.58s
3.58 elaboration of forget_to_Cat_faithful took 3.58s
3.58 elaboration of kernel_cone took 3.58s
3.58 elaboration of has_fpower_series_at.comp took 3.58s
3.57 elaboration of mul_equiv_iso_Group_iso took 3.57s
3.57 elaboration: tactic execution took 3.57s
3.57 elaboration of is_integral_of_noetherian' took 3.57s
3.57 elaboration of pderivative_mul took 3.57s
3.57 elaboration of completion took 3.57s
3.57 elaboration of rpow_def_of_nonneg took 3.57s
3.56 elaboration of defn took 3.56s
3.56 elaboration of norm_sq_div_sub_div_lt_one took 3.56s
3.56 elaboration: tactic execution took 3.56s
3.56 elaboration: tactic execution took 3.56s
3.56 elaboration of is_bounded_bilinear_map_apply took 3.56s
3.55 elaboration: tactic execution took 3.55s
3.55 decl post-processing of injective_iff took 3.55s
3.55 elaboration of cpow_add took 3.55s
3.54 elaboration: tactic execution took 3.54s
3.54 elaboration of HD_lipschitz_aux1 took 3.54s
3.53 decl post-processing of mul_right_inj took 3.53s
3.53 decl post-processing of closure took 3.53s
3.53 decl post-processing of id took 3.53s
3.52 elaboration of closeds.compact_space took 3.52s
3.52 elaboration: tactic execution took 3.52s
3.52 decl post-processing of has_lt took 3.52s
3.52 elaboration of antilipschitz_of_uniform_embedding took 3.52s
3.51 elaboration: tactic execution took 3.51s
3.51 elaboration of mem_span_insert_exchange took 3.51s
3.51 elaboration: tactic execution took 3.51s
3.5 elaboration: tactic execution took 3.5s
3.5 decl post-processing of mem_left_coset took 3.5s
3.5 decl post-processing of coe.is_monoid_hom took 3.5s
3.5 elaboration: tactic execution took 3.5s
3.49 elaboration of is_cycle_swap_mul_aux₂ took 3.49s
3.49 elaboration of to_CommRing_iso took 3.49s
3.49 elaboration of integral_dirac took 3.49s
3.49 elaboration of written_in_ext_chart_comp took 3.49s
3.49 decl post-processing of coe_subset_coe took 3.49s
3.49 elaboration of ring_equiv_iso_CommRing_iso took 3.49s
3.49 elaboration of prod_add_index took 3.49s
3.48 elaboration: tactic execution took 3.48s
3.48 elaboration of inner_product_space_is_normed_group took 3.48s
3.47 decl post-processing of mem_Inf took 3.47s
3.47 elaboration of has_fpower_series_on_ball.uniform_geometric_approx took 3.47s
3.47 elaboration: tactic execution took 3.47s
3.47 elaboration: tactic execution took 3.47s
3.47 elaboration of HD_lipschitz_aux2 took 3.47s
3.47 elaboration of coprod.associator_naturality took 3.47s
3.47 elaboration of le_lt_decidable took 3.47s
3.46 elaboration of has_deriv_at_real_of_complex took 3.46s
3.46 elaboration of nat_div_mod took 3.46s
3.46 elaboration of restr_norm_le took 3.46s
3.46 elaboration of adj took 3.46s
3.45 elaboration of mul_rpow took 3.45s
3.45 elaboration: tactic execution took 3.45s
3.45 elaboration: tactic execution took 3.45s
3.45 elaboration of continuous_multilinear_map.uncurry_right took 3.45s
3.44 elaboration of module took 3.44s
3.44 elaboration of adj took 3.44s
3.44 elaboration of norm_equiv took 3.44s
3.44 elaboration: tactic execution took 3.44s
3.43 elaboration of exists_simple_func_near took 3.43s
3.43 decl post-processing of ker_lift_is_group_hom took 3.43s
3.43 elaboration of restrict_dom_comp_subtype took 3.43s
3.42 elaboration of comp_coeff_zero took 3.42s
3.42 elaboration of countable_closure_of_compact took 3.42s
3.42 decl post-processing of units.is_unit_mul_units took 3.42s
3.42 elaboration: tactic execution took 3.42s
3.42 elaboration of ring_equiv_iso_Ring_iso took 3.42s
3.41 elaboration of prod_preserves_connected_limits took 3.41s
3.41 elaboration: tactic execution took 3.41s
3.4 elaboration of norm_nonneg took 3.4s
3.4 elaboration of continuous_multilinear_map.fin0_apply_norm took 3.4s
3.4 elaboration: tactic execution took 3.4s
3.4 elaboration of Hausdorff_dist_optimal took 3.4s
3.4 elaboration: tactic execution took 3.4s
3.39 elaboration of module took 3.39s
3.39 elaboration of norm_image_sub_le_of_bound took 3.39s
3.39 elaboration of map_hom took 3.39s
3.39 elaboration of tangent_bundle_model_space_topology_eq_prod took 3.39s
3.39 elaboration of tendsto_exp_div_pow_at_top took 3.39s
3.38 elaboration: tactic execution took 3.38s
3.38 elaboration: tactic execution took 3.38s
3.38 elaboration of bilin_form.to_matrix_comp took 3.38s
3.38 elaboration: tactic execution took 3.38s
3.38 elaboration of linear_map.bound_of_continuous took 3.38s
3.37 elaboration of cohomology_functor took 3.37s
3.37 elaboration of add_comm_group took 3.37s
3.37 decl post-processing of lift_mk' took 3.37s
3.37 elaboration: tactic execution took 3.37s
3.37 elaboration of Hausdorff_dist_optimal_le_HD took 3.37s
3.37 elaboration of integral_lt_top_of_fin_vol_supp took 3.37s
3.37 elaboration: tactic execution took 3.37s
3.36 decl post-processing of prod_map took 3.36s
3.36 elaboration of norm_eq_norm_app_of_nonzero took 3.36s
3.36 elaboration: tactic execution took 3.36s
3.35 elaboration: tactic execution took 3.35s
3.35 elaboration of comp took 3.35s
3.35 elaboration of Ad took 3.35s
3.34 elaboration of borel_eq_generate_from_Iio_rat took 3.34s
3.34 decl post-processing of prod_ite_eq took 3.34s
3.34 decl post-processing of left_coset_mem_left_coset took 3.34s
3.33 elaboration of comp took 3.33s
3.33 elaboration of completion.uniformity_dist' took 3.33s
3.33 elaboration of complete' took 3.33s
3.33 elaboration of has_sum_eval took 3.33s
3.33 elaboration of restrict_preimage' took 3.33s
3.33 elaboration: tactic execution took 3.33s
3.32 elaboration of is_noetherian_iff_well_founded took 3.32s
3.32 elaboration of mdifferentiable_at_atlas_symm took 3.32s
3.32 elaboration: tactic execution took 3.32s
3.32 elaboration: tactic execution took 3.32s
3.32 elaboration of subset_tangent_cone_prod_left took 3.32s
3.31 elaboration of prod_comp took 3.31s
3.31 elaboration of integral_congr took 3.31s
3.3 elaboration of sin_lt_sin_of_le_of_le_pi_div_two took 3.3s
3.3 decl post-processing of topological_group_quotient took 3.3s
3.3 elaboration of HD_candidates_b_dist_le took 3.3s
3.3 elaboration: tactic execution took 3.3s
3.29 elaboration: tactic execution took 3.29s
3.29 elaboration of arg_le_pi took 3.29s
3.29 elaboration: tactic execution took 3.29s
3.29 elaboration: tactic execution took 3.29s
3.28 elaboration of GH_space_metric_space took 3.28s
3.28 elaboration of complete_lattice took 3.28s
3.28 elaboration of has_limit_cospan_of_has_limit_pair_of_has_limit_parallel_pair took 3.28s
3.28 elaboration of to_Ring_iso took 3.28s
3.27 decl post-processing of ext took 3.27s
3.27 elaboration of is_measurable.inter_preimage took 3.27s
3.27 elaboration of prod.associator_naturality took 3.27s
3.27 decl post-processing of has_mul took 3.27s
3.26 elaboration of div_one took 3.26s
3.25 elaboration: tactic execution took 3.25s
3.25 elaboration of comma_category took 3.25s
3.25 elaboration of mul_single_apply_aux took 3.25s
3.24 elaboration: tactic execution took 3.24s
3.23 elaboration of limit_ took 3.23s
3.23 elaboration of continuous_multilinear_map.uncurry_curry_right took 3.23s
3.23 elaboration of sign_bij_aux_inj took 3.23s
3.23 decl post-processing of has_mem took 3.23s
3.22 elaboration of iterated_fderiv_within_univ took 3.22s
3.22 elaboration of matrix.to_bilin_formₗ took 3.22s
3.22 elaboration of complete_lattice took 3.22s
3.22 elaboration of pow_sub_pow_factor took 3.22s
3.22 elaboration of has_deriv_within_at.div took 3.22s
3.21 elaboration of continuous_multilinear_map.uncurry_curry_left took 3.21s
3.2 elaboration: tactic execution took 3.2s
3.2 decl post-processing of one_mem took 3.2s
3.2 decl post-processing of comap_top took 3.2s
3.19 decl post-processing of mul_aut took 3.19s
3.19 decl post-processing of has_forget_to_Mon took 3.19s
3.19 elaboration: tactic execution took 3.19s
3.19 elaboration of is_measurable.diff_null took 3.19s
3.19 elaboration: tactic execution took 3.19s
3.19 decl post-processing of coe_fst took 3.19s
3.19 elaboration of metric_space took 3.19s
3.19 decl post-processing of mul_coe took 3.19s
3.18 elaboration: tactic execution took 3.18s
3.18 elaboration: tactic execution took 3.18s
3.18 elaboration of convex_iff_sum_mem took 3.18s
3.18 elaboration: tactic execution took 3.18s
3.18 elaboration of adj took 3.18s
3.17 elaboration of nonempty_compacts.second_countable_topology took 3.17s
3.17 elaboration of continuous_multilinear_map.curry_left_norm took 3.17s
3.17 elaboration: tactic execution took 3.17s
3.16 elaboration of chart_source took 3.16s
3.16 elaboration of r' took 3.16s
3.15 elaboration of times_cont_diff_on_of_continuous_on_differentiable_on_deriv took 3.15s
3.15 elaboration of f_aux_zero_eq took 3.15s
3.15 elaboration of complete_space took 3.15s
3.15 elaboration of has_limit_discrete took 3.15s
3.15 decl post-processing of mul_left_inj took 3.15s
3.15 elaboration of linear_map.of_real took 3.15s
3.15 elaboration of single_mul_apply_aux took 3.15s
3.15 elaboration of has_fderiv_within_at.comp_has_deriv_within_at took 3.15s
3.14 elaboration of a_soln_is_unique took 3.14s
3.14 elaboration: tactic execution took 3.14s
3.14 elaboration of cpow_nat_inv_pow took 3.14s
3.14 elaboration of exi_rat_seq_conv took 3.14s
3.14 elaboration of exists_has_deriv_within_at_eq_of_gt_of_lt took 3.14s
3.14 elaboration of complete took 3.14s
3.14 elaboration: tactic execution took 3.14s
3.13 elaboration of is_measurable_cut took 3.13s
3.13 decl post-processing of mem_trivial took 3.13s
3.13 elaboration of formal_multilinear_series.has_fpower_series_on_ball took 3.13s
3.13 decl post-processing of induction_on' took 3.13s
3.13 elaboration: tactic execution took 3.13s
3.12 elaboration of prod.triangle took 3.12s
3.12 elaboration of coprod.triangle took 3.12s
3.12 elaboration: tactic execution took 3.12s
3.12 elaboration of sum_hom_units_eq_zero took 3.12s
3.11 elaboration of convex_on_dist took 3.11s
3.11 elaboration of is_integral_trans took 3.11s
3.11 elaboration: tactic execution took 3.11s
3.11 decl post-processing of to_monoid_hom_apply took 3.11s
3.11 elaboration of times_cont_diff_on_succ_iff_has_fderiv_within_at took 3.11s
3.11 elaboration of C_union took 3.11s
3.11 elaboration of sigma_equiv_sigma_pi took 3.11s
3.11 elaboration: tactic execution took 3.11s
3.11 elaboration: tactic execution took 3.11s
3.1 decl post-processing of eq_trivial_iff took 3.1s
3.1 elaboration of max_var_bound took 3.1s
3.1 elaboration of ring took 3.1s
3.1 elaboration of module.endomorphism_algebra took 3.1s
3.09 elaboration of bind took 3.09s
3.09 elaboration of CommRing_iso_to_ring_equiv took 3.09s
3.09 elaboration of riesz_lemma took 3.09s
3.09 elaboration of continuous.mul took 3.09s
3.08 elaboration of coeff_zero_ne_zero took 3.08s
3.08 elaboration of to_linear_equiv took 3.08s
3.08 elaboration of arcsin_nonneg took 3.08s
3.07 elaboration of cos_bound took 3.07s
3.07 elaboration of prime took 3.07s
3.07 decl post-processing of map_of_surjective_eq_map_gen took 3.07s
3.07 elaboration: tactic execution took 3.07s
3.06 elaboration: tactic execution took 3.06s
3.06 decl post-processing of normalizer_is_subgroup took 3.06s
3.05 elaboration of lintegral_supr_directed took 3.05s
3.05 elaboration: tactic execution took 3.05s
3.05 elaboration of antilipschitz took 3.05s
3.05 elaboration of cau_seq_to_rat_cau_seq took 3.05s
3.04 elaboration of model_with_corners.image took 3.04s
3.04 decl post-processing of mem_left_coset_iff took 3.04s
3.04 elaboration of embedding_of_subset_isometry took 3.04s
3.04 elaboration: tactic execution took 3.04s
3.04 decl post-processing of continuous_submonoid took 3.04s
3.04 elaboration: tactic execution took 3.04s
3.03 decl post-processing of ite_mul took 3.03s
3.03 elaboration of Ring_iso_to_ring_equiv took 3.03s
3.03 elaboration: tactic execution took 3.03s
3.03 elaboration of map took 3.03s
3.02 elaboration of yoneda_lemma took 3.02s
3.02 elaboration of to_module_totalize_of_le took 3.02s
3.02 elaboration of dense_Inter_of_open_nat took 3.02s
3.02 elaboration of inductive_limit_dist_eq_dist took 3.02s
3.01 elaboration: tactic execution took 3.01s
3.01 elaboration of continuous_linear_map.uncurry_left_norm took 3.01s
3.01 elaboration: tactic execution took 3.01s
3.01 elaboration of equiv_of_right_inverse took 3.01s
3.01 elaboration: tactic execution took 3.01s
3.01 elaboration of is_bounded_linear_map_continuous_multilinear_map_comp_linear took 3.01s
3.01 elaboration of continuous_multilinear_map.apply_zero_curry0 took 3.01s
3.01 elaboration of restrict_preimage took 3.01s
3.01 elaboration of continuous_inf_edist_Hausdorff_edist took 3.01s
3.01 elaboration of has_deriv_within_at.limsup_norm_slope_le took 3.01s
3 elaboration of mul_single_apply_aux took 3s
3 elaboration of is_integral_of_mem_of_fg took 3s
3 elaboration of newton_seq_norm_eq took 3s
3 elaboration: tactic execution took 3s
3 elaboration of lt_of_is_st_lt took 3s
3 elaboration of Union_aux took 3s
3 elaboration of times_cont_diff_iff_continuous_differentiable took 3s
3 elaboration: tactic execution took 3s
3 decl post-processing of map took 3s
3 elaboration: tactic execution took 3s
2.99 decl post-processing of is_open_of_open_subgroup took 2.99s
2.99 elaboration of has_fderiv_at_filter.comp took 2.99s
2.99 elaboration of mk_pi_ring_apply_one_eq_self took 2.99s
2.99 elaboration of continuous_of_bound took 2.99s
2.99 decl post-processing of prod_unique took 2.99s
2.99 elaboration of soln_unique took 2.99s
2.99 elaboration of newton_seq_dist_tendsto took 2.99s
2.99 elaboration: tactic execution took 2.99s
2.99 elaboration: tactic execution took 2.99s
2.99 elaboration of continuous_rpow_aux3 took 2.99s
2.99 elaboration of units_equiv_aut took 2.99s
2.98 elaboration of colimit_is_colimit took 2.98s
2.98 elaboration of has_deriv_at_log took 2.98s
2.98 elaboration of completion.mem_uniformity_dist took 2.98s
2.98 elaboration of rpow_neg took 2.98s
2.98 elaboration of continuous_multilinear_map.uncurry_right_norm took 2.98s
2.97 elaboration of isometry.isometric_on_range took 2.97s
2.97 elaboration of repr_power took 2.97s
2.97 elaboration of trans took 2.97s
2.97 elaboration of has_mfderiv_at_id took 2.97s
2.96 elaboration: tactic execution took 2.96s
2.96 elaboration of tan_lt_tan_of_nonneg_of_lt_pi_div_two took 2.96s
2.96 elaboration: tactic execution took 2.96s
2.95 elaboration: tactic execution took 2.95s
2.95 elaboration: tactic execution took 2.95s
2.95 elaboration: tactic execution took 2.95s
2.95 elaboration of cos_pi_over_two_pow took 2.95s
2.95 elaboration of comparison_forget took 2.95s
2.95 elaboration of eval took 2.95s
2.94 elaboration: tactic execution took 2.94s
2.94 elaboration of module.restrict_scalars took 2.94s
2.94 elaboration of binary_cofan.mk took 2.94s
2.94 elaboration of is_lebesgue_measurable_Iio took 2.94s
2.93 elaboration: tactic execution took 2.93s
2.93 elaboration of continuous_at_rpow took 2.93s
2.93 elaboration of trim_sum_ge took 2.93s
2.93 elaboration of eval₂_mul_monomial took 2.93s
2.93 elaboration of at_prime.local_ring took 2.93s
2.93 elaboration of edist_smul took 2.93s
2.93 elaboration of exists_is_measurable_superset_of_measure_eq_zero took 2.93s
2.93 elaboration of iso_perm took 2.93s
2.92 elaboration of sum_two_squares_of_nat_prime_of_not_irreducible took 2.92s
2.92 elaboration of eval₂_comp_left took 2.92s
2.92 elaboration of sin_arg took 2.92s
2.92 elaboration of cau_seq.tendsto_limit took 2.92s
2.92 decl post-processing of eq_of_eq_on_mtop took 2.92s
2.92 elaboration of is_bounded_bilinear_map_smul_right took 2.92s
2.91 elaboration of exists_root took 2.91s
2.91 elaboration: tactic execution took 2.91s
2.91 elaboration of cof_eq_one_iff_is_succ took 2.91s
2.91 elaboration of binary_fan.mk took 2.91s
2.91 elaboration of diagram_iso_parallel_pair took 2.91s
2.91 decl post-processing of open_subgroup took 2.91s
2.91 elaboration: tactic execution took 2.91s
2.91 elaboration of continuous_multilinear_map.uncurry0_norm took 2.91s
2.9 elaboration: tactic execution took 2.9s
2.9 elaboration of bundle_mfderiv_within_univ took 2.9s
2.9 elaboration of discriminant_le_zero took 2.9s
2.9 elaboration of symm_comp_deriv took 2.9s
2.9 decl post-processing of subset_closure took 2.9s
2.9 elaboration of lebesgue_outer_Icc took 2.9s
2.89 elaboration of iterated_deriv_within_succ took 2.89s
2.89 elaboration: tactic execution took 2.89s
2.89 elaboration of smul_right_norm took 2.89s
2.89 elaboration of degree_div_X_lt took 2.89s
2.89 decl post-processing of mul_left_surjective took 2.89s
2.89 elaboration of complete_space took 2.89s
2.89 decl post-processing of map_mul took 2.89s
2.89 elaboration of unique_mdiff_on.unique_diff_on took 2.89s
2.88 elaboration: tactic execution took 2.88s
2.88 elaboration of unique_diff_within_at.eq took 2.88s
2.88 elaboration: tactic execution took 2.88s
2.88 elaboration: tactic execution took 2.88s
2.88 elaboration of desc_fun took 2.88s
2.88 elaboration of right_unitor_naturality took 2.88s
2.88 decl post-processing of mem_center took 2.88s
2.88 elaboration of eq_zero_or_eq_zero_of_mul_eq_zero took 2.88s
2.87 elaboration of cpow_eq_zero_iff took 2.87s
2.87 elaboration of of_multiset took 2.87s
2.87 decl post-processing of inv_mul_cancel_right took 2.87s
2.87 elaboration of candidates_dist_bound took 2.87s
2.86 elaboration of differentiable_within_at.has_deriv_within_at took 2.86s
2.86 elaboration of mdifferentiable_within_at_univ took 2.86s
2.86 elaboration of category_theory.forget₂.category_theory.full took 2.86s
2.86 elaboration of inhabited took 2.86s
2.86 elaboration: tactic execution took 2.86s
2.86 elaboration of exists_sum_two_squares_add_one_eq_k took 2.86s
2.86 elaboration: tactic execution took 2.86s
2.86 elaboration of Inf_eq_of_function_Inf_gen took 2.86s
2.86 elaboration of hom_eval₂ took 2.86s
2.86 elaboration of det_mul_aux took 2.86s
2.86 elaboration of to_complex_div_im took 2.86s
2.85 elaboration: tactic execution took 2.85s
2.85 elaboration: tactic execution took 2.85s
2.85 elaboration of has_strict_deriv_at_pow took 2.85s
2.85 elaboration: tactic execution took 2.85s
2.85 elaboration of linear_order.convex_on_of_lt took 2.85s
2.85 elaboration of card_nth_roots_subgroup_units took 2.85s
2.85 elaboration of has_deriv_within_at.smul took 2.85s
2.85 elaboration of metric_space took 2.85s
2.84 elaboration of arg_one took 2.84s
2.84 elaboration of is_bounded_bilinear_map_smul took 2.84s
2.84 elaboration of iterated_fderiv_within_congr took 2.84s
2.84 elaboration of order_topology_of_nhds_abs took 2.84s
2.84 decl post-processing of has_coe_to_fun took 2.84s
2.84 elaboration of left_unitor_naturality took 2.84s
2.83 elaboration of image_le_of_liminf_slope_right_le_deriv_boundary took 2.83s
2.83 elaboration of fin_vol_supp_of_integrable took 2.83s
2.83 decl post-processing of monoid_hom.is_group_hom took 2.83s
2.83 elaboration of repr_add took 2.83s
2.83 elaboration: tactic execution took 2.83s
2.83 elaboration of open_mapping took 2.83s
2.83 elaboration of map_pair took 2.83s
2.82 elaboration of limit_is_limit took 2.82s
2.82 elaboration of log_neg_one took 2.82s
2.82 decl post-processing of left_coset took 2.82s
2.82 elaboration of Hausdorff_edist_self took 2.82s
2.82 elaboration of is_st_add took 2.82s
2.82 elaboration of T_def took 2.82s
2.82 decl post-processing of mk'_ker took 2.82s
2.81 elaboration: tactic execution took 2.81s
2.81 elaboration of post took 2.81s
2.81 elaboration of has_mfderiv_within_at.union took 2.81s
2.81 elaboration of has_deriv_within_at.inv took 2.81s
2.8 elaboration of linear_independent_std_basis took 2.8s
2.8 elaboration: tactic execution took 2.8s
2.8 elaboration of one_cpow took 2.8s
2.8 elaboration: tactic execution took 2.8s
2.8 elaboration of comparison took 2.8s
2.8 elaboration of comp_change_of_variables took 2.8s
2.8 elaboration of continuous_multilinear_map.curry_right_norm took 2.8s
2.8 elaboration of bundle_mfderiv_chart took 2.8s
2.8 elaboration of supported_Union took 2.8s
2.8 elaboration: tactic execution took 2.8s
2.79 elaboration: tactic execution took 2.79s
2.79 decl post-processing of coe_range_restrict took 2.79s
2.79 elaboration of has_inv took 2.79s
2.79 elaboration: tactic execution took 2.79s
2.79 elaboration: tactic execution took 2.79s
2.79 elaboration of mul_inv took 2.79s
2.79 elaboration: tactic execution took 2.79s
2.79 elaboration of lebesgue_outer_trim took 2.79s
2.79 elaboration: tactic execution took 2.79s
2.79 decl post-processing of range_restrict took 2.79s
2.79 elaboration of norm_zero_iff took 2.79s
2.79 elaboration of log_one took 2.79s
2.78 elaboration: tactic execution took 2.78s
2.78 elaboration of closeds.complete_space took 2.78s
2.78 elaboration of arg_neg_one took 2.78s
2.78 elaboration of measure_Union_eq_supr_nat took 2.78s
2.78 elaboration of pempty_equiv_discrete_pempty took 2.78s
2.78 elaboration of has_fpower_series_at.add took 2.78s
2.78 elaboration of ord_cof_eq took 2.78s
2.78 elaboration of compact_candidates_b took 2.78s
2.77 elaboration of sin_pi_div_two took 2.77s
2.77 elaboration of to_complex_div_re took 2.77s
2.77 elaboration: tactic execution took 2.77s
2.77 elaboration of trim_eq_infi' took 2.77s
2.76 elaboration: tactic execution took 2.76s
2.76 elaboration of newton_seq_dist_to_a took 2.76s
2.76 elaboration of compact_of_finite_subfamily_closed took 2.76s
2.76 elaboration: tactic execution took 2.76s
2.76 elaboration of associated_comp took 2.76s
2.75 elaboration: tactic execution took 2.75s
2.75 elaboration of eisenstein_lemma_aux₂ took 2.75s
2.75 elaboration of dirac_caratheodory took 2.75s
2.75 elaboration of a_e took 2.75s
2.75 elaboration of lift took 2.75s
2.75 decl post-processing of injective_ker_lift took 2.75s
2.75 elaboration: tactic execution took 2.75s
2.74 decl post-processing of inhabited took 2.74s
2.74 elaboration of polynomial.continuous_eval took 2.74s
2.74 elaboration of coeff_mul_X' took 2.74s
2.74 elaboration: tactic execution took 2.74s
2.74 elaboration: tactic execution took 2.74s
2.74 elaboration: tactic execution took 2.74s
2.74 elaboration of equiv_zero_of_val_eq_of_equiv_zero took 2.74s
2.74 elaboration of exists_extension_of_le_sublinear took 2.74s
2.74 decl post-processing of mem_right_coset_right_coset took 2.74s
2.74 elaboration of has_deriv_at_filter.add took 2.74s
2.74 elaboration: tactic execution took 2.74s
2.73 elaboration: tactic execution took 2.73s
2.73 elaboration: tactic execution took 2.73s
2.73 elaboration of cos_lt_cos_of_nonneg_of_le_pi_div_two took 2.73s
2.73 elaboration of mfderiv_within_zero_of_not_mdifferentiable_within_at took 2.73s
2.73 elaboration: tactic execution took 2.73s
2.73 elaboration of abs_cpow_inv_nat took 2.73s
2.73 elaboration: tactic execution took 2.73s
2.73 elaboration of dense_sInter_of_Gδ took 2.73s
2.73 elaboration: tactic execution took 2.73s
2.73 elaboration: tactic execution took 2.73s
2.72 elaboration of inf_edist_le_inf_edist_add_edist took 2.72s
2.72 elaboration of mdifferentiable_within_at_iff_differentiable_within_at took 2.72s
2.72 elaboration of trim_add took 2.72s
2.72 elaboration of eval₂_rename_prodmk took 2.72s
2.72 elaboration: tactic execution took 2.72s
2.72 elaboration of candidates_lipschitz_aux took 2.72s
2.72 elaboration: tactic execution took 2.72s
2.72 elaboration of Ico_map_val_min_abs_nat_abs_eq_Ico_map_id took 2.72s
2.72 elaboration: tactic execution took 2.72s
2.72 elaboration of arg_neg_I took 2.72s
2.71 elaboration: tactic execution took 2.71s
2.71 elaboration of continuous_multilinear_map.uncurry0_curry0 took 2.71s
2.71 elaboration of norm_image_sub_le_of_norm_deriv_right_le_segment took 2.71s
2.71 elaboration of compact_pi_infinite took 2.71s
2.71 elaboration of continuous_multilinear_map.norm_map_cons_le took 2.71s
2.71 elaboration of of.zero_exact took 2.71s
2.71 decl post-processing of fintype.prod_fiberwise took 2.71s
2.71 elaboration of has_deriv_at_filter.scomp took 2.71s
2.71 elaboration of to_complex.is_ring_hom took 2.71s
2.71 elaboration of mem_atlas_iff took 2.71s
2.71 elaboration of convex.center_mass_mem took 2.71s
2.7 elaboration: tactic execution took 2.7s
2.7 elaboration of exists_pow_two_eq_prime_iff_of_mod_four_eq_one took 2.7s
2.7 elaboration: tactic execution took 2.7s
2.7 elaboration: tactic execution took 2.7s
2.7 elaboration of field took 2.7s
2.7 decl post-processing of prod_zero took 2.7s
2.7 elaboration of neg took 2.7s
2.7 decl post-processing of prod_insert took 2.7s
2.7 elaboration: tactic execution took 2.7s
2.7 elaboration of inner_sub_left took 2.7s
2.7 elaboration of sum_two_squares_of_two_mul_sum_two_squares took 2.7s
2.7 elaboration of smul_right_one_eq_iff took 2.7s
2.7 elaboration of map_div took 2.7s
2.69 elaboration of cantor_function_aux_succ took 2.69s
2.69 elaboration of deriv_within_fderiv_within took 2.69s
2.69 elaboration of f_aux_deriv took 2.69s
2.69 decl post-processing of is_open took 2.69s
2.69 elaboration of order_eq took 2.69s
2.69 elaboration of continuous_linear_map.re_norm took 2.69s
2.69 elaboration: tactic execution took 2.69s
2.69 elaboration of not_infinite_iff_exist_lt_gt took 2.69s
2.69 elaboration of cos_pi_div_four took 2.69s
2.69 decl post-processing of comp took 2.69s
2.69 elaboration: tactic execution took 2.69s
2.69 elaboration of associated_to_quadratic_form took 2.69s
2.69 elaboration of arg_I took 2.69s
2.69 elaboration of sin_two_pi took 2.69s
2.69 elaboration: tactic execution took 2.69s
2.69 elaboration: tactic execution took 2.69s
2.69 elaboration of exists_forall_abs_polynomial_eval_le took 2.69s
2.69 elaboration: tactic execution took 2.69s
2.68 elaboration: tactic execution took 2.68s
2.68 elaboration of mem_supported' took 2.68s
2.68 elaboration: tactic execution took 2.68s
2.68 elaboration of linear_map.re took 2.68s
2.68 elaboration: tactic execution took 2.68s
2.68 elaboration of sin_pi took 2.68s
2.67 elaboration of has_deriv_at_filter_congr_of_mem_sets took 2.67s
2.67 elaboration of bind took 2.67s
2.67 elaboration of counit_is_iso_of_R_fully_faithful took 2.67s
2.67 elaboration of cos_two_pi took 2.67s
2.67 elaboration of id took 2.67s
2.67 elaboration: tactic execution took 2.67s
2.66 elaboration of sqrt_two_add_series_lt_two took 2.66s
2.66 elaboration of sin_add_pi took 2.66s
2.66 elaboration of iterated_deriv_eq_iterate took 2.66s
2.66 decl post-processing of eq_of_inv_eq_inv took 2.66s
2.66 elaboration of tendsto_pow_at_top_nhds_0_of_lt_1_normed_field took 2.66s
2.66 elaboration: tactic execution took 2.66s
2.66 elaboration of tr_respects_aux₂ took 2.66s
2.66 elaboration of iterated_fderiv_within_apply_eq_iterated_deriv_within_mul_prod took 2.66s
2.66 elaboration of zero_mul took 2.66s
2.66 elaboration: tactic execution took 2.66s
2.65 elaboration of iterated_deriv_one took 2.65s
2.65 elaboration: tactic execution took 2.65s
2.65 elaboration of local_ring took 2.65s
2.65 elaboration of equiv_of_equiv took 2.65s
2.65 decl post-processing of inv_mem took 2.65s
2.65 elaboration of ratio_le_op_norm took 2.65s
2.65 elaboration of continuous_linear_map.of_real_norm took 2.65s
2.65 elaboration of bind_const took 2.65s
2.65 elaboration of continuous_linear_map.im_norm took 2.65s
2.65 elaboration: tactic execution took 2.65s
2.65 elaboration of sin_add_pi_div_two took 2.65s
2.65 elaboration of tangent_bundle_model_space_coe_chart_at_symm took 2.65s
2.64 elaboration of change_origin_eval took 2.64s
2.64 elaboration of cos_pi took 2.64s
2.64 elaboration of cpow_zero took 2.64s
2.64 elaboration of sum_apply took 2.64s
2.64 decl post-processing of comm_group took 2.64s
2.64 elaboration of is_null_measurable.Union_nat took 2.64s
2.64 decl post-processing of mul took 2.64s
2.64 elaboration of map_presheaf took 2.64s
2.64 elaboration: tactic execution took 2.64s
2.64 elaboration of padic_polynomial_dist took 2.64s
2.64 decl post-processing of comp took 2.64s
2.64 elaboration of functoriality_counit took 2.64s
2.64 elaboration of rat_dense took 2.64s
2.64 elaboration: tactic execution took 2.64s
2.64 elaboration of ih_n took 2.64s
2.64 elaboration of adj took 2.64s
2.63 elaboration: tactic execution took 2.63s
2.63 elaboration of prime_of_nat_prime_of_mod_four_eq_three took 2.63s
2.63 elaboration of is_st_mul' took 2.63s
2.63 elaboration of has_deriv_within_at.log took 2.63s
2.63 elaboration of is_bounded_bilinear_map.is_bounded_linear_map_left took 2.63s
2.63 elaboration of arccos_neg_one took 2.63s
2.63 elaboration of post took 2.63s
2.63 elaboration of norm_const took 2.63s
2.63 elaboration of exists_exp_eq_of_pos took 2.63s
2.63 elaboration of glue_eq_of_dist_eq_zero took 2.63s
2.63 elaboration: tactic execution took 2.63s
2.63 elaboration of cos_two_pi took 2.63s
2.63 elaboration of comm_semiring took 2.63s
2.62 elaboration of add_comm_group took 2.62s
2.62 elaboration of linear_map.im took 2.62s
2.62 elaboration: tactic execution took 2.62s
2.62 decl post-processing of is_monoid_hom took 2.62s
2.62 elaboration of cpow_int_cast took 2.62s
2.62 elaboration of measure_bUnion took 2.62s
2.62 elaboration of rename.is_ring_hom took 2.62s
2.62 elaboration: tactic execution took 2.62s
2.62 elaboration of sin_two_pi took 2.62s
2.62 elaboration of op_norm_neg took 2.62s
2.62 elaboration of convex.image_sub_le_mul_sub_of_deriv_le took 2.62s
2.62 elaboration of log_abs took 2.62s
2.62 elaboration of sin_add_pi took 2.62s
2.62 elaboration of has_fderiv_within_at_inter' took 2.62s
2.61 elaboration of induced_maps_commute took 2.61s
2.61 elaboration of proj_ker_of_right_inverse_apply_idem took 2.61s
2.61 elaboration of category_theory.concrete_category took 2.61s
2.61 elaboration of bundle_mfderiv_within_subset took 2.61s
2.61 elaboration of inner_neg_neg took 2.61s
2.61 elaboration of to_semimodule took 2.61s
2.61 elaboration of complete_space_of_cau_seq_complete took 2.61s
2.61 decl post-processing of subset_normalizer took 2.61s
2.61 elaboration of cos_pi_div_eight took 2.61s
2.61 elaboration of category_of_differential_objects took 2.61s
2.61 elaboration of fix took 2.61s
2.61 elaboration of pderivative_C took 2.61s
2.6 elaboration of zero_rpow took 2.6s
2.6 elaboration of eintegral_le_eintegral took 2.6s
2.6 elaboration: tactic execution took 2.6s
2.6 elaboration: tactic execution took 2.6s
2.6 elaboration of congr took 2.6s
2.6 elaboration of newton_seq_succ_dist_weak took 2.6s
2.6 elaboration of cos_pi took 2.6s
2.6 elaboration of arccos_neg took 2.6s
2.6 elaboration of sin_pi took 2.6s
2.6 elaboration of tangent_bundle_model_space_coe_chart_at took 2.6s
2.6 elaboration of Icc_left_chart took 2.6s
2.6 elaboration of is_local_min.has_deriv_at_eq_zero took 2.6s
2.6 elaboration of inner_add_right took 2.6s
2.6 elaboration of of_function_le took 2.6s
2.59 elaboration of has_fderiv_at_filter_iff_has_deriv_at_filter took 2.59s
2.59 decl post-processing of map_is_group_hom took 2.59s
2.59 elaboration of op_norm_neg took 2.59s
2.59 elaboration of C_empty took 2.59s
2.59 elaboration of times_cont_diff_on_zero took 2.59s
2.59 elaboration of sign_aux_swap_zero_one took 2.59s
2.59 elaboration: tactic execution took 2.59s
2.59 elaboration of arcsin_neg_one took 2.59s
2.59 elaboration of deriv_zero_of_not_differentiable_at took 2.59s
2.59 decl post-processing of prod_Ico_eq_mul_inv took 2.59s
2.58 elaboration: tactic execution took 2.58s
2.58 elaboration of deriv_fderiv took 2.58s
2.58 elaboration of is_absolute_value took 2.58s
2.58 elaboration of volume_bUnion_finset took 2.58s
2.58 elaboration of log_zero took 2.58s
2.58 elaboration of comp_change_of_variables_blocks_fun took 2.58s
2.58 elaboration: tactic execution took 2.58s
2.58 decl post-processing of of_mul_eq_cons took 2.58s
2.58 elaboration: tactic execution took 2.58s
2.58 elaboration of is_local_min_on.has_fderiv_within_at_nonneg took 2.58s
2.58 elaboration of continuous_linear_map.of_real took 2.58s
2.58 elaboration of div_mod_by_monic_unique took 2.58s
2.58 elaboration of unique_mdiff_within_at_iff_unique_diff_within_at took 2.58s
2.58 elaboration of is_local_min_on.has_fderiv_within_at_eq_zero took 2.58s
2.58 elaboration of iterated_fderiv_apply_eq_iterated_deriv_mul_prod took 2.58s
2.58 elaboration of is_supported_of took 2.58s
2.58 elaboration of cast_pow took 2.58s
2.57 elaboration: tactic execution took 2.57s
2.57 elaboration of rpow_one took 2.57s
2.57 elaboration of normed_field took 2.57s
2.57 elaboration: tactic execution took 2.57s
2.57 elaboration of has_fderiv_at took 2.57s
2.57 elaboration: tactic execution took 2.57s
2.57 elaboration of inf_edist_le_inf_edist_add_Hausdorff_edist took 2.57s
2.57 decl post-processing of coe_subset_coe took 2.57s
2.57 elaboration of has_sum_geometric took 2.57s
2.57 elaboration of sin_pi_div_eight took 2.57s
2.57 elaboration of times_cont_diff_on.fderiv_within took 2.57s
2.57 elaboration: tactic execution took 2.57s
2.57 elaboration of normed_space.restrict_scalars took 2.57s
2.57 elaboration of sin_pi_div_four took 2.57s
2.57 elaboration of arccos_one took 2.57s
2.56 elaboration: tactic execution took 2.56s
2.56 elaboration of is_Gδ_sInter took 2.56s
2.56 elaboration of zero took 2.56s
2.56 elaboration of convex.image_sub_lt_mul_sub_of_deriv_lt took 2.56s
2.56 elaboration: tactic execution took 2.56s
2.56 elaboration of metric_space_sum took 2.56s
2.56 decl post-processing of finset_prod_mem took 2.56s
2.56 elaboration of is_local_max_on.has_fderiv_within_at_eq_zero took 2.56s
2.56 elaboration: tactic execution took 2.56s
2.56 elaboration of colimit_is_colimit took 2.56s
2.56 elaboration of GH_dist_le_nonempty_compacts_dist took 2.56s
2.56 elaboration: tactic execution took 2.56s
2.56 elaboration of inf_edist_closure took 2.56s
2.56 elaboration: tactic execution took 2.56s
2.56 elaboration of approximates_deriv_on_nhds took 2.56s
2.56 elaboration of le_op_norm took 2.56s
2.56 elaboration of mul took 2.56s
2.56 elaboration: tactic execution took 2.56s
2.56 elaboration: tactic execution took 2.56s
2.56 elaboration: tactic execution took 2.56s
2.55 decl post-processing of finset.prod_fiberwise took 2.55s
2.55 elaboration: tactic execution took 2.55s
2.55 elaboration: tactic execution took 2.55s
2.55 elaboration of cohomology_map_comp took 2.55s
2.55 elaboration: tactic execution took 2.55s
2.55 elaboration of Hausdorff_edist_ne_top_of_nonempty_of_bounded took 2.55s
2.55 elaboration of tendsto_zero_of_norm_tendsto_zero took 2.55s
2.55 elaboration of smul_dirac_apply took 2.55s
2.55 elaboration of is_rat took 2.55s
2.55 elaboration: tactic execution took 2.55s
2.54 elaboration of mul took 2.54s
2.54 elaboration of to_manifold took 2.54s
2.54 decl post-processing of prod_add took 2.54s
2.54 elaboration of functoriality_unit' took 2.54s
2.54 elaboration of coeff_comp_degree_mul_degree took 2.54s
2.54 elaboration of trim_trim took 2.54s
2.54 elaboration of rpow_zero took 2.54s
2.53 elaboration: tactic execution took 2.53s
2.53 elaboration of pow took 2.53s
2.53 elaboration of normed_group.of_core took 2.53s
2.53 elaboration of mem_nonunits took 2.53s
2.53 elaboration of is_bounded_bilinear_map.times_cont_diff took 2.53s
2.53 elaboration of is_bounded_bilinear_map.map_sub_right took 2.53s
2.53 elaboration of mul_equiv_iso_CommMon_iso took 2.53s
2.53 elaboration of mul_action took 2.53s
2.52 elaboration of lebesgue_length_Icc took 2.52s
2.52 elaboration of lebesgue_length_eq_infi_Icc took 2.52s
2.52 elaboration of has_scalar took 2.52s
2.52 decl post-processing of has_inv took 2.52s
2.52 elaboration: tactic execution took 2.52s
2.52 elaboration of padic_norm_e_of_padic_int took 2.52s
2.52 elaboration of a_is_soln took 2.52s
2.52 decl post-processing of prod_sdiff took 2.52s
2.52 elaboration of zero_cpow took 2.52s
2.52 elaboration: tactic execution took 2.52s
2.52 elaboration: tactic execution took 2.52s
2.52 elaboration: tactic execution took 2.52s
2.52 elaboration of lift_aux took 2.52s
2.52 elaboration: tactic execution took 2.52s
2.52 elaboration of coe_coe took 2.52s
2.52 elaboration of point_reflection_dist_self_real took 2.52s
2.51 elaboration of NF_repr_split' took 2.51s
2.51 elaboration of one_rpow took 2.51s
2.51 elaboration: tactic execution took 2.51s
2.51 elaboration of order_top took 2.51s
2.51 elaboration of inf_dist_singleton took 2.51s
2.51 elaboration of Inf_caratheodory took 2.51s
2.51 elaboration: tactic execution took 2.51s
2.51 elaboration of is_bounded_bilinear_map.map_sub_left took 2.51s
2.51 elaboration of iterated_deriv_within_one took 2.51s
2.51 elaboration: tactic execution took 2.51s
2.51 elaboration of norm_lt_one_mul took 2.51s
2.51 elaboration of times_cont_diff_on.differentiable_on_iterated_deriv_within took 2.51s
2.51 elaboration of continuous_linear_map.of_real_isometry took 2.51s
2.51 elaboration: tactic execution took 2.51s
2.51 elaboration of lebesgue_outer_singleton took 2.51s
2.5 elaboration of le_add_caratheodory took 2.5s
2.5 elaboration: tactic execution took 2.5s
2.5 elaboration of exists_pow_two_eq_two_iff took 2.5s
2.5 elaboration: tactic execution took 2.5s
2.5 elaboration of measure_union took 2.5s
2.5 elaboration of div_def took 2.5s
2.5 elaboration of deriv_norm_ne_zero took 2.5s
2.5 elaboration: tactic execution took 2.5s
2.5 elaboration: tactic execution took 2.5s
2.5 elaboration: tactic execution took 2.5s
2.5 elaboration of inner_neg_left took 2.5s
2.49 elaboration of normed_field.to_normed_ring took 2.49s
2.49 elaboration: tactic execution took 2.49s
2.49 elaboration: tactic execution took 2.49s
2.49 elaboration of is_null_measurable.union_null took 2.49s
2.49 elaboration: tactic execution took 2.49s
2.49 elaboration of continuous_multilinear_map.curry0_norm took 2.49s
2.48 elaboration of le_sum_caratheodory took 2.48s
2.48 elaboration of tangent_cone_univ took 2.48s
2.48 elaboration: tactic execution took 2.48s
2.48 elaboration: tactic execution took 2.48s
2.48 elaboration of arctan_neg took 2.48s
2.48 elaboration: tactic execution took 2.48s
2.48 elaboration of category_theory.category took 2.48s
2.48 elaboration of sum took 2.48s
2.48 elaboration: tactic execution took 2.48s
2.48 decl post-processing of is_unit_of_mul_is_unit_right took 2.48s
2.48 elaboration of mul_lt_one took 2.48s
2.48 elaboration of is_o.tendsto_0 took 2.48s
2.47 elaboration of map_map took 2.47s
2.47 elaboration: tactic execution took 2.47s
2.47 elaboration of comp₂ took 2.47s
2.47 elaboration of calc_norm_le_one took 2.47s
2.47 elaboration of pderivative_add took 2.47s
2.47 elaboration: tactic execution took 2.47s
2.47 elaboration of rearr_comp took 2.47s
2.47 elaboration: tactic execution took 2.47s
2.47 elaboration of coeff_inv_aux took 2.47s
2.47 elaboration of associated_is_sym took 2.47s
2.47 elaboration of has_fderiv_at_filter_iff_tendsto took 2.47s
2.47 elaboration: tactic execution took 2.47s
2.47 elaboration of norm_tsum_le_tsum_norm took 2.47s
2.46 elaboration: tactic execution took 2.46s
2.46 elaboration of has_zero_morphisms took 2.46s
2.46 elaboration of exists_right_inverse_linear_map_of_surjective took 2.46s
2.46 elaboration of Hausdorff_edist_triangle took 2.46s
2.46 elaboration of prod_subtype_domain_index took 2.46s
2.46 elaboration of union_null took 2.46s
2.46 elaboration of desc took 2.46s
2.46 elaboration of one took 2.46s
2.46 elaboration of has_add took 2.46s
2.46 elaboration of inv_eq_zero took 2.46s
2.46 elaboration of ext_chart_at_continuous_on_symm took 2.46s
2.46 elaboration of coeff_mul_X took 2.46s
2.46 elaboration of lifted_cone_is_limit took 2.46s
2.46 elaboration: tactic execution took 2.46s
2.46 elaboration: tactic execution took 2.46s
2.45 elaboration of convex_on_exp took 2.45s
2.45 elaboration of coeff_succ_mul_X took 2.45s
2.45 elaboration of sum_totient took 2.45s
2.45 elaboration of norm_id_le took 2.45s
2.45 elaboration: tactic execution took 2.45s
2.45 elaboration of sum.dist_eq_glue_dist took 2.45s
2.45 elaboration of comp_add took 2.45s
2.45 elaboration: tactic execution took 2.45s
2.45 elaboration: tactic execution took 2.45s
2.45 elaboration of inf_dist_empty took 2.45s
2.45 elaboration: tactic execution took 2.45s
2.45 elaboration of inf_dist_eq_closure took 2.45s
2.45 elaboration: tactic execution took 2.45s
2.44 elaboration: tactic execution took 2.44s
2.44 elaboration: tactic execution took 2.44s
2.44 elaboration of dirac took 2.44s
2.44 elaboration of to_matrix_swap took 2.44s
2.44 elaboration of norm_int took 2.44s
2.44 elaboration: tactic execution took 2.44s
2.44 elaboration of norm_one took 2.44s
2.44 elaboration of one_le_max_var took 2.44s
2.44 elaboration of diagonal_to_lin took 2.44s
2.44 elaboration of polar_to_quadratic_form took 2.44s
2.44 elaboration: tactic execution took 2.44s
2.44 elaboration of tendsto_pow_at_top_at_top_of_gt_1_nat took 2.44s
2.44 elaboration of Hausdorff_dist_zero_iff_closure_eq_closure took 2.44s
2.44 elaboration of Hausdorff_dist_closure₂ took 2.44s
2.44 elaboration of norm_rat took 2.44s
2.44 elaboration of cantor_function_le took 2.44s
2.44 elaboration of Hausdorff_dist_triangle' took 2.44s
2.44 elaboration: tactic execution took 2.44s
2.44 elaboration: tactic execution took 2.44s
2.43 elaboration of real.volume_Ico took 2.43s
2.43 elaboration of functoriality_counit' took 2.43s
2.43 elaboration of mem_closure_iff_inf_dist_zero took 2.43s
2.43 elaboration: tactic execution took 2.43s
2.43 elaboration: tactic execution took 2.43s
2.43 elaboration of dense_bUnion_interior_of_closed took 2.43s
2.43 elaboration of free took 2.43s
2.43 elaboration of ext_chart_model_space_eq_id took 2.43s
2.43 elaboration: tactic execution took 2.43s
2.43 elaboration of symmetry took 2.43s
2.43 elaboration of sqrt_two_add_series_zero took 2.43s
2.43 elaboration of euclidean_half_space.inhabited took 2.43s
2.43 elaboration of gauss_lemma_aux₂ took 2.43s
2.43 elaboration of is_o_of_tendsto took 2.43s
2.43 elaboration of associated_right_inverse took 2.43s
2.43 elaboration of mul_equiv_iso_Mon_iso took 2.43s
2.43 elaboration: tactic execution took 2.43s
2.42 elaboration: tactic execution took 2.42s
2.42 elaboration of mem_chart_target_iff took 2.42s
2.42 elaboration of Hausdorff_dist_image took 2.42s
2.42 elaboration of real.volume_Ioo took 2.42s
2.42 elaboration: tactic execution took 2.42s
2.42 elaboration of mem_chart_source_iff took 2.42s
2.42 elaboration: tactic execution took 2.42s
2.42 elaboration of has_strict_fderiv_at_id took 2.42s
2.42 elaboration of equicontinuous_of_continuity_modulus took 2.42s
2.42 decl post-processing of coe_symm_mk took 2.42s
2.42 elaboration of cast_eq_of_rat_of_nat took 2.42s
2.42 elaboration of has_fderiv_at_filter.tendsto_nhds took 2.42s
2.42 elaboration of log_nonpos took 2.42s
2.42 elaboration: tactic execution took 2.42s
2.42 elaboration: tactic execution took 2.42s
2.42 elaboration of fderiv_within_zero_of_not_differentiable_within_at took 2.42s
2.42 elaboration of lsum took 2.42s
2.42 elaboration of Hausdorff_edist_empty took 2.42s
2.42 elaboration: tactic execution took 2.42s
2.42 elaboration of Hausdorff_dist_closure took 2.42s
2.41 elaboration: tactic execution took 2.41s
2.41 elaboration: tactic execution took 2.41s
2.41 elaboration: tactic execution took 2.41s
2.41 elaboration: tactic execution took 2.41s
2.41 elaboration of exists_dist_lt_of_Hausdorff_dist_lt' took 2.41s
2.41 elaboration: tactic execution took 2.41s
2.41 elaboration: tactic execution took 2.41s
2.41 elaboration of cast_eq_of_rat_of_int took 2.41s
2.41 elaboration of repr_sub took 2.41s
2.41 elaboration: tactic execution took 2.41s
2.41 elaboration of has_sum_geometric_two' took 2.41s
2.41 elaboration of real.volume_singleton took 2.41s
2.41 elaboration of pderivative_monomial took 2.41s
2.41 elaboration of zero_def took 2.41s
2.41 elaboration of lintegral_finset_sum took 2.41s
2.4 decl post-processing of inj_of_trivial_ker took 2.4s
2.4 elaboration of exists_dist_lt_of_inf_dist_lt took 2.4s
2.4 elaboration of real.volume_Icc took 2.4s
2.4 elaboration of C_eq_coe_nat took 2.4s
2.4 decl post-processing of left_coset_equiv_rel took 2.4s
2.4 elaboration: tactic execution took 2.4s
2.4 elaboration of finite_of_linear_independent took 2.4s
2.4 elaboration of aux_has_sum_of_le_geometric took 2.4s
2.4 decl post-processing of prod_eq_fold took 2.4s
2.4 elaboration of norm_coe_le_norm took 2.4s
2.4 elaboration: tactic execution took 2.4s
2.4 decl post-processing of lift_unique took 2.4s
2.4 elaboration of to_matrix_comp took 2.4s
2.4 elaboration of C_Union_lt took 2.4s
2.4 elaboration of dirac_bind took 2.4s
2.4 elaboration of coeff_C_mul took 2.4s
2.4 elaboration of inf_dist_zero_of_mem took 2.4s
2.39 elaboration of C_compl_iff took 2.39s
2.39 elaboration of Hausdorff_edist_closure₁ took 2.39s
2.39 elaboration: tactic execution took 2.39s
2.39 elaboration: tactic execution took 2.39s
2.39 elaboration: tactic execution took 2.39s
2.39 elaboration of tendsto_zero_iff_norm_tendsto_zero took 2.39s
2.39 elaboration: tactic execution took 2.39s
2.39 elaboration of factor_set.sup_add_inf_eq_add took 2.39s
2.39 elaboration of integral_on_zero took 2.39s
2.39 elaboration of nat_cast_complex_norm took 2.39s
2.39 decl post-processing of prod_reverse took 2.39s
2.39 elaboration of Union_null took 2.39s
2.39 elaboration: tactic execution took 2.39s
2.39 elaboration of inf_dist_nonneg took 2.39s
2.39 decl post-processing of coprod_comp_inr took 2.39s
2.39 elaboration of yoneda took 2.39s
2.39 elaboration: tactic execution took 2.39s
2.39 elaboration of not_equiv_zero_const_of_nonzero took 2.39s
2.39 elaboration: tactic execution took 2.39s
2.39 elaboration: tactic execution took 2.39s
2.38 elaboration of comp_C took 2.38s
2.38 elaboration of lift_unique took 2.38s
2.38 elaboration of Hausdorff_dist_empty took 2.38s
2.38 elaboration of model_with_corners.right_inv took 2.38s
2.38 elaboration: tactic execution took 2.38s
2.38 elaboration of padic_norm_z.is_absolute_value took 2.38s
2.38 elaboration of Hausdorff_dist_self_closure took 2.38s
2.38 elaboration of range_const took 2.38s
2.38 elaboration: tactic execution took 2.38s
2.38 elaboration: tactic execution took 2.38s
2.38 elaboration of eq_of_linear_independent_of_span_subtype took 2.38s
2.38 elaboration of normed_top_ring took 2.38s
2.38 elaboration of coeff_C_mul took 2.38s
2.38 elaboration of Hausdorff_dist_self_zero took 2.38s
2.38 elaboration of measure_Union took 2.38s
2.38 elaboration: tactic execution took 2.38s
2.38 elaboration of inf_dist_image took 2.38s
2.38 elaboration of differentiable_on_univ took 2.38s
2.37 elaboration: tactic execution took 2.37s
2.37 elaboration of Hausdorff_dist_closure₁ took 2.37s
2.37 elaboration: tactic execution took 2.37s
2.37 decl post-processing of mem_right_coset_iff took 2.37s
2.37 elaboration of is_measurable.is_null_measurable took 2.37s
2.37 elaboration of measurable.ennreal_mul took 2.37s
2.37 elaboration of lebesgue_length_eq_infi_Ioo took 2.37s
2.37 elaboration of Hausdorff_dist_zero_iff_eq_of_closed took 2.37s
2.37 elaboration: tactic execution took 2.37s
2.37 elaboration of induction_on took 2.37s
2.37 elaboration: tactic execution took 2.37s
2.37 elaboration: tactic execution took 2.37s
2.37 decl post-processing of mul_self_iff_eq_one took 2.37s
2.37 elaboration: tactic execution took 2.37s
2.37 elaboration of is_basis took 2.37s
2.37 elaboration: tactic execution took 2.37s
2.37 elaboration of null_is_null_measurable took 2.37s
2.37 decl post-processing of one took 2.37s
2.37 elaboration of edist_eq_add_add took 2.37s
2.37 elaboration of exists_sup took 2.37s
2.37 elaboration: tactic execution took 2.37s
2.37 elaboration of top_apply took 2.37s
2.37 elaboration: tactic execution took 2.37s
2.37 elaboration of ih_0 took 2.37s
2.37 elaboration of Hausdorff_dist_comm took 2.37s
2.36 elaboration of mk_real took 2.36s
2.36 elaboration of eval₂_add took 2.36s
2.36 elaboration of of_endo_map took 2.36s
2.36 elaboration of add_comp took 2.36s
2.36 elaboration of prod.normed_group took 2.36s
2.36 elaboration: tactic execution took 2.36s
2.36 elaboration: tactic execution took 2.36s
2.36 elaboration: tactic execution took 2.36s
2.36 elaboration of coeff_map took 2.36s
2.36 elaboration: tactic execution took 2.36s
2.36 elaboration of card_order_of_eq_totient_aux₁ took 2.36s
2.36 elaboration of cauchy_seq_of_edist_le_geometric_two took 2.36s
2.36 elaboration of norm_one took 2.36s
2.36 elaboration: tactic execution took 2.36s
2.36 elaboration: tactic execution took 2.36s
2.36 elaboration of set.finite.convex_hull_eq_image took 2.36s
2.36 elaboration: tactic execution took 2.36s
2.35 elaboration of minor_cons_row took 2.35s
2.35 elaboration of join took 2.35s
2.35 elaboration of nondiscrete_normed_field took 2.35s
2.35 decl post-processing of comm_monoid took 2.35s
2.35 elaboration: tactic execution took 2.35s
2.35 elaboration of summable_cantor_function took 2.35s
2.35 elaboration: tactic execution took 2.35s
2.35 elaboration of le_smul_caratheodory took 2.35s
2.35 elaboration of cauchy_seq.is_cau_seq took 2.35s
2.35 elaboration of range_half_space took 2.35s
2.35 elaboration: tactic execution took 2.35s
2.35 elaboration: tactic execution took 2.35s
2.34 elaboration: tactic execution took 2.34s
2.34 elaboration: tactic execution took 2.34s
2.34 elaboration: tactic execution took 2.34s
2.34 elaboration of range_quadrant took 2.34s
2.34 elaboration of nat_abs_norm_eq took 2.34s
2.34 elaboration of model_with_corners.left_inv took 2.34s
2.34 elaboration of eq_X_add_C_of_degree_le_one took 2.34s
2.34 elaboration of cast_eq_of_rat took 2.34s
2.34 elaboration: tactic execution took 2.34s
2.34 elaboration: tactic execution took 2.34s
2.34 elaboration of measure'_union took 2.34s
2.34 elaboration of cantor_function_aux_nonneg took 2.34s
2.34 elaboration of nnreal.tendsto_inverse_at_top_nhds_0_nat took 2.34s
2.34 elaboration: tactic execution took 2.34s
2.33 elaboration of nnreal.tendsto_const_div_at_top_nhds_0_nat took 2.33s
2.33 elaboration: tactic execution took 2.33s
2.33 elaboration of of_normed_group took 2.33s
2.33 elaboration of T_pow took 2.33s
2.33 elaboration: tactic execution took 2.33s
2.33 elaboration: tactic execution took 2.33s
2.33 elaboration of sum_prod_distrib took 2.33s
2.33 elaboration of self_eq_mk took 2.33s
2.33 elaboration of coeff_mul_C took 2.33s
2.33 elaboration of category_theory.concrete_category took 2.33s
2.33 elaboration: tactic execution took 2.33s
2.33 elaboration of is_null_measurable_iff took 2.33s
2.33 elaboration of mul_equiv.to_Group_iso took 2.33s
2.33 elaboration of is_subgroup.is_cyclic took 2.33s
2.33 elaboration: tactic execution took 2.33s
2.32 elaboration of has_zero_object took 2.32s
2.32 decl post-processing of sup_eq_range took 2.32s
2.32 elaboration of lmap_domain_supported took 2.32s
2.32 elaboration: tactic execution took 2.32s
2.32 elaboration of is_Gδ.union took 2.32s
2.32 elaboration of restrict_apply took 2.32s
2.32 elaboration of functoriality_unit took 2.32s
2.32 elaboration of integral_join took 2.32s
2.32 elaboration of Hausdorff_dist_empty' took 2.32s
2.32 elaboration: tactic execution took 2.32s
2.32 elaboration of is_o_zero took 2.32s
2.32 elaboration of restrict_integral took 2.32s
2.32 elaboration: tactic execution took 2.32s
2.31 elaboration: tactic execution took 2.31s
2.31 elaboration: tactic execution took 2.31s
2.31 elaboration of model_with_corners_euclidean_half_space took 2.31s
2.31 decl post-processing of is_unit_of_mul_eq_one took 2.31s
2.31 elaboration of euclidean_quadrant.inhabited took 2.31s
2.31 elaboration of bind_pure took 2.31s
2.31 elaboration: tactic execution took 2.31s
2.31 elaboration of X_pow_eq_single took 2.31s
2.31 elaboration: tactic execution took 2.31s
2.31 elaboration of eq_zero_or_eq_zero_of_mul_eq_zero took 2.31s
2.31 elaboration of is_basis.constr_apply took 2.31s
2.31 elaboration of map_rename took 2.31s
2.31 elaboration of span_eq_map_total took 2.31s
2.31 elaboration: tactic execution took 2.31s
2.31 elaboration of wilsons_lemma took 2.31s
2.31 elaboration: tactic execution took 2.31s
2.31 elaboration of norm_mod_lt took 2.31s
2.3 elaboration: tactic execution took 2.3s
2.3 elaboration of exists_norm_lt_one took 2.3s
2.3 elaboration of nat_degree_pow_eq' took 2.3s
2.3 elaboration of glue_premetric took 2.3s
2.3 elaboration of tendsto_inv_zero_at_top took 2.3s
2.3 elaboration: tactic execution took 2.3s
2.3 elaboration of disjoint_span_singleton took 2.3s
2.3 elaboration: tactic execution took 2.3s
2.3 elaboration of nat.modeq.pow_totient took 2.3s
2.3 elaboration of tendsto_pow_at_top_nhds_0_of_lt_1 took 2.3s
2.3 elaboration of padic_int.eq_zero_or_eq_zero_of_mul_eq_zero took 2.3s
2.3 elaboration: tactic execution took 2.3s
2.3 elaboration of repr_mul took 2.3s
2.3 elaboration of findim_euclidean_space took 2.3s
2.3 elaboration of cantor_function_aux_ff took 2.3s
2.3 elaboration of cantor_function_aux_tt took 2.3s
2.29 decl post-processing of prod_top took 2.29s
2.29 elaboration: tactic execution took 2.29s
2.29 elaboration of lintegral_nnnorm_zero took 2.29s
2.29 elaboration of integrable_mk took 2.29s
2.29 decl post-processing of coe_mul took 2.29s
2.29 decl post-processing of decidable_eq took 2.29s
2.29 elaboration of Hausdorff_dist_nonneg took 2.29s
2.29 elaboration of rat.nondiscrete_normed_field took 2.29s
2.29 elaboration: tactic execution took 2.29s
2.29 elaboration of pderivative_eq_zero_of_not_mem_vars took 2.29s
2.29 elaboration: tactic execution took 2.29s
2.29 elaboration of coe_inj took 2.29s
2.29 elaboration of limit_is_limit took 2.29s
2.29 elaboration: tactic execution took 2.29s
2.28 elaboration: tactic execution took 2.28s
2.28 elaboration of to_module took 2.28s
2.28 elaboration: tactic execution took 2.28s
2.28 elaboration of div_eq_filter_card took 2.28s
2.28 elaboration of comp took 2.28s
2.28 elaboration of norm_add_le took 2.28s
2.28 elaboration: tactic execution took 2.28s
2.28 elaboration: tactic execution took 2.28s
2.28 elaboration of to_equiv_inj took 2.28s
2.28 elaboration of linear_independent_comp_subtype took 2.28s
2.28 elaboration of lim_norm_zero took 2.28s
2.28 elaboration: tactic execution took 2.28s
2.28 elaboration of finset.measurable_prod took 2.28s
2.28 elaboration of is_O_with_congr took 2.28s
2.28 decl post-processing of prod_unique took 2.28s
2.28 elaboration: tactic execution took 2.28s
2.28 elaboration of is_open.is_Gδ took 2.28s
2.28 elaboration: tactic execution took 2.28s
2.28 elaboration of infinite_pos_add_not_infinite_neg took 2.28s
2.28 elaboration: tactic execution took 2.28s
2.28 elaboration of norm_fpow took 2.28s
2.28 elaboration of Inf_gen_nonempty2 took 2.28s
2.27 elaboration: tactic execution took 2.27s
2.27 elaboration: tactic execution took 2.27s
2.27 elaboration: tactic execution took 2.27s
2.27 elaboration of mul_equiv.to_CommGroup_iso took 2.27s
2.27 elaboration of comp_assoc took 2.27s
2.27 elaboration: tactic execution took 2.27s
2.27 elaboration of tendsto_mul took 2.27s
2.27 elaboration of norm_fst_le took 2.27s
2.27 elaboration: tactic execution took 2.27s
2.27 elaboration of mk_eq_div took 2.27s
2.27 elaboration: tactic execution took 2.27s
2.27 elaboration of dense_Union_interior_of_closed took 2.27s
2.27 decl post-processing of lift_one took 2.27s
2.27 elaboration: tactic execution took 2.27s
2.27 elaboration: tactic execution took 2.27s
2.27 elaboration: tactic execution took 2.27s
2.26 elaboration of to_dual_eq_repr took 2.26s
2.26 elaboration: tactic execution took 2.26s
2.26 elaboration of norm_pow_le took 2.26s
2.26 elaboration: tactic execution took 2.26s
2.26 elaboration: tactic execution took 2.26s
2.26 elaboration: tactic execution took 2.26s
2.26 elaboration of completion.uniformity_dist took 2.26s
2.26 elaboration of cpow_mul took 2.26s
2.26 elaboration: tactic execution took 2.26s
2.26 elaboration: tactic execution took 2.26s
2.26 elaboration of desc_fun took 2.26s
2.26 elaboration: tactic execution took 2.26s
2.26 elaboration of cantor_function_aux_eq took 2.26s
2.26 elaboration of coe_add took 2.26s
2.26 elaboration: tactic execution took 2.26s
2.26 elaboration: tactic execution took 2.26s
2.25 elaboration of norm_div took 2.25s
2.25 elaboration: tactic execution took 2.25s
2.25 elaboration of mul_to_lin took 2.25s
2.25 elaboration of prod.braiding took 2.25s
2.25 elaboration: tactic execution took 2.25s
2.25 elaboration of convex.translate took 2.25s
2.25 elaboration: tactic execution took 2.25s
2.25 elaboration of sub_rev took 2.25s
2.25 elaboration of nat_cast_real_norm took 2.25s
2.25 elaboration of semimodule took 2.25s
2.25 elaboration of measurable_integral took 2.25s
2.25 elaboration: tactic execution took 2.25s
2.25 elaboration: tactic execution took 2.25s
2.25 elaboration of padic_int.pmul_comm took 2.25s
2.24 elaboration: tactic execution took 2.24s
2.24 elaboration of nnreal.young_inequality took 2.24s
2.24 elaboration of leading_coeff_X_pow took 2.24s
2.24 elaboration: tactic execution took 2.24s
2.24 elaboration: tactic execution took 2.24s
2.24 elaboration of norm_neg took 2.24s
2.24 elaboration of pow_root_multiplicity_dvd took 2.24s
2.24 elaboration: tactic execution took 2.24s
2.24 elaboration of embedding_GL took 2.24s
2.24 decl post-processing of map_comp took 2.24s
2.24 elaboration of eval₂_eta took 2.24s
2.24 elaboration of exists_root_of_splits took 2.24s
2.24 elaboration: tactic execution took 2.24s
2.24 elaboration of equiv_of_is_basis took 2.24s
2.24 decl post-processing of map_inr took 2.24s
2.24 elaboration of nat_degree_comp_le took 2.24s
2.24 elaboration: tactic execution took 2.24s
2.23 elaboration of dist_add_right took 2.23s
2.23 elaboration: tactic execution took 2.23s
2.23 elaboration of polynomial.tendsto_infinity took 2.23s
2.23 elaboration of discr_smul took 2.23s
2.23 elaboration: tactic execution took 2.23s
2.23 elaboration of measurable.ennreal_sub took 2.23s
2.23 elaboration: tactic execution took 2.23s
2.23 elaboration of real.is_topological_basis_Ioo_rat took 2.23s
2.23 elaboration of inv took 2.23s
2.23 elaboration: tactic execution took 2.23s
2.23 elaboration of card_units took 2.23s
2.23 elaboration of separation_setoid.uniform_space took 2.23s
2.23 elaboration of measurable.ennreal_add took 2.23s
2.23 elaboration of one_sub_K_pos' took 2.23s
2.23 elaboration: tactic execution took 2.23s
2.23 elaboration: tactic execution took 2.23s
2.22 elaboration: tactic execution took 2.22s
2.22 elaboration of discr_comp took 2.22s
2.22 elaboration of map_eq_zero took 2.22s
2.22 elaboration: tactic execution took 2.22s
2.22 elaboration of is_bounded_bilinear_map.is_O took 2.22s
2.22 elaboration: tactic execution took 2.22s
2.22 elaboration: tactic execution took 2.22s
2.22 elaboration: tactic execution took 2.22s
2.22 elaboration of eval_sub_factor took 2.22s
2.22 elaboration: tactic execution took 2.22s
2.22 elaboration of uniform_space_of_edist took 2.22s
2.22 elaboration: tactic execution took 2.22s
2.22 elaboration of has_image_maps_of_has_strong_epi_images took 2.22s
2.22 elaboration: tactic execution took 2.22s
2.22 elaboration: tactic execution took 2.22s
2.21 elaboration of coe_eq_coe took 2.21s
2.21 elaboration: tactic execution took 2.21s
2.21 elaboration of leading_coeff_map took 2.21s
2.21 elaboration: tactic execution took 2.21s
2.21 elaboration: tactic execution took 2.21s
2.21 elaboration: tactic execution took 2.21s
2.21 elaboration: tactic execution took 2.21s
2.21 elaboration of div_X took 2.21s
2.21 elaboration: tactic execution took 2.21s
2.21 elaboration: tactic execution took 2.21s
2.21 elaboration: tactic execution took 2.21s
2.21 elaboration: tactic execution took 2.21s
2.21 elaboration: tactic execution took 2.21s
2.21 elaboration: tactic execution took 2.21s
2.21 elaboration: tactic execution took 2.21s
2.21 elaboration of to_complex_inj took 2.21s
2.21 elaboration: tactic execution took 2.21s
2.21 elaboration: tactic execution took 2.21s
2.21 elaboration of pderivative_monomial_single took 2.21s
2.21 elaboration: tactic execution took 2.21s
2.21 decl post-processing of prod_cons took 2.21s
2.21 elaboration: tactic execution took 2.21s
2.2 elaboration: tactic execution took 2.2s
2.2 elaboration: tactic execution took 2.2s
2.2 elaboration: tactic execution took 2.2s
2.2 elaboration of linear_independent_iff took 2.2s
2.2 decl post-processing of ext took 2.2s
2.2 elaboration of unit_is_iso_of_L_fully_faithful took 2.2s
2.2 elaboration: tactic execution took 2.2s
2.2 elaboration: tactic execution took 2.2s
2.2 elaboration: tactic execution took 2.2s
2.2 elaboration: tactic execution took 2.2s
2.2 elaboration: tactic execution took 2.2s
2.2 decl post-processing of coprod_unique took 2.2s
2.2 elaboration: tactic execution took 2.2s
2.2 elaboration of has_zero took 2.2s
2.2 decl post-processing of closure_eq_mrange took 2.2s
2.2 decl post-processing of eq_inv_mul_iff_mul_eq took 2.2s
2.2 elaboration: tactic execution took 2.2s
2.2 elaboration of smul_right_one_one took 2.2s
2.2 elaboration of Inf_gen_empty took 2.2s
2.2 elaboration: tactic execution took 2.2s
2.2 elaboration of tr_supports took 2.2s
2.2 elaboration of trunc_C took 2.2s
2.19 elaboration of eval₂_eq_eval_map took 2.19s
2.19 elaboration of preimage_measurable took 2.19s
2.19 elaboration of mul_zero took 2.19s
2.19 elaboration of fermat_little took 2.19s
2.19 elaboration: tactic execution took 2.19s
2.19 elaboration of to_matrix_id took 2.19s
2.19 elaboration of dist_add_left took 2.19s
2.19 elaboration: tactic execution took 2.19s
2.19 elaboration: tactic execution took 2.19s
2.19 decl post-processing of is_unit_one took 2.19s
2.19 elaboration of fin_dim_vectorspace_equiv took 2.19s
2.19 elaboration: tactic execution took 2.19s
2.19 decl post-processing of injective_iff took 2.19s
2.19 elaboration of lifted_cocone_is_colimit took 2.19s
2.19 decl post-processing of closure_preimage_le took 2.19s
2.19 elaboration of monic_monomial_eq took 2.19s
2.19 elaboration: tactic execution took 2.19s
2.18 elaboration: tactic execution took 2.18s
2.18 elaboration: tactic execution took 2.18s
2.18 elaboration: tactic execution took 2.18s
2.18 elaboration: tactic execution took 2.18s
2.18 elaboration: tactic execution took 2.18s
2.18 elaboration of pderivative_zero took 2.18s
2.18 elaboration of lebesgue_length_Ico took 2.18s
2.18 elaboration: tactic execution took 2.18s
2.18 elaboration of zero_comp took 2.18s
2.18 elaboration of lift_pred took 2.18s
2.18 elaboration: tactic execution took 2.18s
2.18 elaboration of merge' took 2.18s
2.18 elaboration: tactic execution took 2.18s
2.18 elaboration of map_map took 2.18s
2.18 elaboration of tendsto_at_top_mul_left' took 2.18s
2.18 elaboration: tactic execution took 2.18s
2.18 elaboration: tactic execution took 2.18s
2.18 elaboration: tactic execution took 2.18s
2.17 elaboration of convex.norm_image_sub_le_of_norm_deriv_le took 2.17s
2.17 elaboration: tactic execution took 2.17s
2.17 elaboration of measurable_map took 2.17s
2.17 elaboration: tactic execution took 2.17s
2.17 elaboration: tactic execution took 2.17s
2.17 decl post-processing of units.coe_mk_of_mul_eq_one took 2.17s
2.17 elaboration of isometry_emetric_iff_metric took 2.17s
2.17 elaboration of span_mul_span took 2.17s
2.17 elaboration: tactic execution took 2.17s
2.17 elaboration: tactic execution took 2.17s
2.17 elaboration: tactic execution took 2.17s
2.17 elaboration: tactic execution took 2.17s
2.17 elaboration of coeff_zero_mul_X took 2.17s
2.17 elaboration of leading_coeff_pow' took 2.17s
2.17 elaboration of eval₂_rename took 2.17s
2.17 elaboration: tactic execution took 2.17s
2.17 elaboration of neg took 2.17s
2.17 elaboration of degree_le_of_ne_zero took 2.17s
2.17 elaboration: tactic execution took 2.17s
2.17 elaboration: tactic execution took 2.17s
2.17 elaboration of glue_dist_glued_points took 2.17s
2.17 elaboration: tactic execution took 2.17s
2.17 elaboration: tactic execution took 2.17s
2.17 elaboration of measure'_eq took 2.17s
2.17 elaboration: tactic execution took 2.17s
2.17 elaboration of convex_hull_eq took 2.17s
2.16 elaboration of card_roots_sub_C' took 2.16s
2.16 elaboration: tactic execution took 2.16s
2.16 elaboration of tendsto_at_top_mul_right' took 2.16s
2.16 elaboration: tactic execution took 2.16s
2.16 elaboration of lifted_cone took 2.16s
2.16 elaboration of mem_of_mem_span took 2.16s
2.16 elaboration: tactic execution took 2.16s
2.16 elaboration: tactic execution took 2.16s
2.16 elaboration: tactic execution took 2.16s
2.16 elaboration: tactic execution took 2.16s
2.16 elaboration: tactic execution took 2.16s
2.16 elaboration: tactic execution took 2.16s
2.16 elaboration of kernel_map_comp took 2.16s
2.16 elaboration: tactic execution took 2.16s
2.16 elaboration of bilin_form.mul_to_matrix_mul took 2.16s
2.16 elaboration: tactic execution took 2.16s
2.16 elaboration of bundled_hom took 2.16s
2.16 elaboration: tactic execution took 2.16s
2.16 elaboration: tactic execution took 2.16s
2.16 elaboration: tactic execution took 2.16s
2.16 elaboration: tactic execution took 2.16s
2.15 elaboration of zip_with_def took 2.15s
2.15 elaboration of coeff_inv_units took 2.15s
2.15 elaboration: tactic execution took 2.15s
2.15 elaboration: tactic execution took 2.15s
2.15 elaboration: tactic execution took 2.15s
2.15 elaboration: tactic execution took 2.15s
2.15 elaboration: tactic execution took 2.15s
2.15 elaboration of coprod.braiding took 2.15s
2.15 elaboration: tactic execution took 2.15s
2.15 elaboration of monomial_add took 2.15s
2.15 elaboration: tactic execution took 2.15s
2.15 elaboration of to_lin_one took 2.15s
2.15 elaboration of continuous_multilinear_curry_right_equiv took 2.15s
2.15 elaboration of iff_fg took 2.15s
2.15 elaboration of lift'_apply_coe took 2.15s
2.15 elaboration of lebesgue_length_empty took 2.15s
2.15 decl post-processing of mul_inv_eq_iff_eq_mul took 2.15s
2.15 elaboration: tactic execution took 2.15s
2.15 elaboration of comp_smul took 2.15s
2.15 elaboration of tensor_id took 2.15s
2.15 elaboration of supported_Inter took 2.15s
2.15 elaboration: tactic execution took 2.15s
2.15 elaboration of to_complex_re took 2.15s
2.15 elaboration: tactic execution took 2.15s
2.15 elaboration of sl_non_abelian took 2.15s
2.15 elaboration: tactic execution took 2.15s
2.14 elaboration: tactic execution took 2.14s
2.14 elaboration: tactic execution took 2.14s
2.14 elaboration: tactic execution took 2.14s
2.14 elaboration of map_right took 2.14s
2.14 elaboration of measure'_Union_le_tsum_nat took 2.14s
2.14 elaboration: tactic execution took 2.14s
2.14 elaboration: tactic execution took 2.14s
2.14 elaboration of padic_norm_e_lim_le took 2.14s
2.14 elaboration: tactic execution took 2.14s
2.14 elaboration: tactic execution took 2.14s
2.14 elaboration of coeff_zero_eq_eval_zero took 2.14s
2.14 elaboration of change_origin_summable_aux1 took 2.14s
2.14 elaboration of top_caratheodory took 2.14s
2.14 elaboration of inf_edist_singleton took 2.14s
2.14 elaboration: tactic execution took 2.14s
2.14 elaboration: tactic execution took 2.14s
2.14 elaboration: tactic execution took 2.14s
2.13 decl post-processing of univ_subgroup took 2.13s
2.13 elaboration of to_complex_im took 2.13s
2.13 decl post-processing of multiset_prod_mem took 2.13s
2.13 elaboration of is_swap_of_subtype took 2.13s
2.13 elaboration of inf_edist_empty took 2.13s
2.13 elaboration: tactic execution took 2.13s
2.13 elaboration of Hausdorff_edist_closure₂ took 2.13s
2.13 elaboration of image_coev took 2.13s
2.13 elaboration of on_presheaf took 2.13s
2.13 elaboration of inf_edist_union took 2.13s
2.13 decl post-processing of has_lt took 2.13s
2.13 elaboration: tactic execution took 2.13s
2.13 elaboration: tactic execution took 2.13s
2.13 elaboration: tactic execution took 2.13s
2.13 decl post-processing of prod took 2.13s
2.13 elaboration of trace took 2.13s
2.13 elaboration of of_finite_basis took 2.13s
2.13 elaboration of functoriality took 2.13s
2.13 elaboration: tactic execution took 2.13s
2.13 decl post-processing of subset_closure took 2.13s
2.13 elaboration of degree_pos_induction_on took 2.13s
2.13 elaboration: tactic execution took 2.13s
2.13 elaboration: tactic execution took 2.13s
2.13 elaboration: tactic execution took 2.13s
2.12 elaboration of has_zero_morphisms took 2.12s
2.12 elaboration of is_unit_iff_degree_eq_zero took 2.12s
2.12 elaboration of eval₂_X took 2.12s
2.12 elaboration: tactic execution took 2.12s
2.12 elaboration: tactic execution took 2.12s
2.12 elaboration of exists_root_of_degree_eq_one took 2.12s
2.12 elaboration of add_comm_group took 2.12s
2.12 elaboration of eval₂_congr took 2.12s
2.12 elaboration: tactic execution took 2.12s
2.12 elaboration of map_map took 2.12s
2.12 elaboration of bilin_form.mul_to_matrix took 2.12s
2.12 elaboration of derivative_eval took 2.12s
2.12 elaboration of to_real_im took 2.12s
2.12 elaboration: tactic execution took 2.12s
2.12 elaboration: tactic execution took 2.12s
2.12 elaboration: tactic execution took 2.12s
2.12 elaboration: tactic execution took 2.12s
2.12 elaboration: tactic execution took 2.12s
2.12 elaboration: tactic execution took 2.12s
2.12 elaboration of norm_sub_le took 2.12s
2.11 elaboration of prod_Ico_one_prime took 2.11s
2.11 elaboration of functoriality took 2.11s
2.11 elaboration of add_comm_group took 2.11s
2.11 elaboration of lift'_of took 2.11s
2.11 elaboration of topological_add_group.to_uniform_space took 2.11s
2.11 elaboration: tactic execution took 2.11s
2.11 elaboration of has_inv took 2.11s
2.11 elaboration: tactic execution took 2.11s
2.11 elaboration of to_Top took 2.11s
2.11 elaboration: tactic execution took 2.11s
2.11 elaboration: tactic execution took 2.11s
2.11 elaboration: tactic execution took 2.11s
2.11 elaboration of comm_ring took 2.11s
2.11 elaboration: tactic execution took 2.11s
2.11 elaboration of decomposition took 2.11s
2.1 elaboration of nat_degree_comp took 2.1s
2.1 elaboration: tactic execution took 2.1s
2.1 elaboration: tactic execution took 2.1s
2.1 elaboration: tactic execution took 2.1s
2.1 elaboration: tactic execution took 2.1s
2.1 elaboration: tactic execution took 2.1s
2.1 elaboration: tactic execution took 2.1s
2.1 elaboration: tactic execution took 2.1s
2.1 elaboration: tactic execution took 2.1s
2.1 elaboration: tactic execution took 2.1s
2.1 elaboration of module took 2.1s
2.1 elaboration of measurable_join took 2.1s
2.1 elaboration: tactic execution took 2.1s
2.1 elaboration: tactic execution took 2.1s
2.1 decl post-processing of prod_Ico_eq_prod_range took 2.1s
2.1 elaboration of eval₂_monomial took 2.1s
2.1 elaboration of norm_eq_zero took 2.1s
2.1 elaboration of mono_factorisation took 2.1s
2.1 elaboration: tactic execution took 2.1s
2.1 elaboration: tactic execution took 2.1s
2.1 elaboration of coeff_mul took 2.1s
2.1 elaboration: tactic execution took 2.1s
2.1 elaboration: tactic execution took 2.1s
2.1 elaboration of poly_binom_aux3 took 2.1s
2.09 elaboration of cast_sub' took 2.09s
2.09 decl post-processing of prod_range_zero took 2.09s
2.09 elaboration of diag_one took 2.09s
2.09 elaboration of eval₂_assoc took 2.09s
2.09 elaboration of comap_equiv took 2.09s
2.09 elaboration: tactic execution took 2.09s
2.09 elaboration of monomial_single_add took 2.09s
2.09 elaboration: tactic execution took 2.09s
2.09 elaboration: tactic execution took 2.09s
2.09 elaboration of bilin_form.to_matrix_comp_right took 2.09s
2.09 elaboration of comp_zero took 2.09s
2.08 elaboration: tactic execution took 2.08s
2.08 elaboration: tactic execution took 2.08s
2.08 decl post-processing of has_one took 2.08s
2.08 elaboration of proj_ker_of_right_inverse took 2.08s
2.08 elaboration of pi_generate_from_eq_fintype took 2.08s
2.08 elaboration: tactic execution took 2.08s
2.08 elaboration of supported_empty took 2.08s
2.08 elaboration: tactic execution took 2.08s
2.08 elaboration of degree_map_le took 2.08s
2.08 elaboration: tactic execution took 2.08s
2.08 elaboration: tactic execution took 2.08s
2.08 elaboration of abs_norm_sub_norm_le took 2.08s
2.08 elaboration: tactic execution took 2.08s
2.08 elaboration: tactic execution took 2.08s
2.08 elaboration: tactic execution took 2.08s
2.08 elaboration of Hausdorff_edist_closure took 2.08s
2.08 elaboration of linear_independent_union took 2.08s
2.08 elaboration of splits_map_iff took 2.08s
2.08 elaboration of to_real_re took 2.08s
2.08 elaboration of proj_diagonal took 2.08s
2.07 elaboration: tactic execution took 2.07s
2.07 elaboration: tactic execution took 2.07s
2.07 elaboration of eval₂_sum took 2.07s
2.07 elaboration: tactic execution took 2.07s
2.07 elaboration: tactic execution took 2.07s
2.07 elaboration of lmap_domain_total took 2.07s
2.07 elaboration of continuous_multilinear_curry_left_equiv took 2.07s
2.07 elaboration: tactic execution took 2.07s
2.07 elaboration of coeff_mul_degree_add_degree took 2.07s
2.07 elaboration of jacobi took 2.07s
2.07 elaboration of supported_eq_span_single took 2.07s
2.07 elaboration: tactic execution took 2.07s
2.07 elaboration: tactic execution took 2.07s
2.07 elaboration: tactic execution took 2.07s
2.07 elaboration of category_theory.limits.has_terminal took 2.07s
2.07 elaboration: tactic execution took 2.07s
2.07 elaboration: tactic execution took 2.07s
2.07 elaboration: tactic execution took 2.07s
2.07 elaboration of subsingleton took 2.07s
2.07 elaboration: tactic execution took 2.07s
2.07 elaboration: tactic execution took 2.07s
2.07 elaboration of euclidean_domain took 2.07s
2.07 elaboration: tactic execution took 2.07s
2.06 elaboration of eq_top_of_findim_eq took 2.06s
2.06 elaboration of map_comp_map took 2.06s
2.06 elaboration of prod.emetric_space_max took 2.06s
2.06 elaboration of norm_pos took 2.06s
2.06 elaboration: tactic execution took 2.06s
2.06 elaboration: tactic execution took 2.06s
2.06 elaboration of is_bounded_bilinear_map.has_strict_fderiv_at took 2.06s
2.06 elaboration: tactic execution took 2.06s
2.06 elaboration: tactic execution took 2.06s
2.06 elaboration: tactic execution took 2.06s
2.06 elaboration: tactic execution took 2.06s
2.06 elaboration: tactic execution took 2.06s
2.06 elaboration of trunc_C took 2.06s
2.06 elaboration of linear_independent_empty took 2.06s
2.06 elaboration: tactic execution took 2.06s
2.06 elaboration of eval₂_hom took 2.06s
2.06 elaboration: tactic execution took 2.06s
2.06 elaboration of map_add_self took 2.06s
2.06 elaboration: tactic execution took 2.06s
2.05 elaboration of eval_assoc took 2.05s
2.05 elaboration of monomial_add_single took 2.05s
2.05 elaboration of ring took 2.05s
2.05 elaboration of X_prime took 2.05s
2.05 elaboration of sum_hom_units took 2.05s
2.05 elaboration: tactic execution took 2.05s
2.05 elaboration of trunc_one took 2.05s
2.05 elaboration: tactic execution took 2.05s
2.05 elaboration: tactic execution took 2.05s
2.05 elaboration of dual_lc took 2.05s
2.05 elaboration of category_of_graded_objects took 2.05s
2.05 elaboration: tactic execution took 2.05s
2.05 elaboration of colimit_cocone took 2.05s
2.05 elaboration of sum took 2.05s
2.05 elaboration: tactic execution took 2.05s
2.05 elaboration: tactic execution took 2.05s
2.05 elaboration: tactic execution took 2.05s
2.05 elaboration of lift.unique took 2.05s
2.04 decl post-processing of prod_eq_foldr took 2.04s
2.04 elaboration of card_image_polynomial_eval took 2.04s
2.04 elaboration of eval₂_C took 2.04s
2.04 elaboration: tactic execution took 2.04s
2.04 elaboration of degree_div_le took 2.04s
2.04 elaboration: tactic execution took 2.04s
2.04 elaboration: tactic execution took 2.04s
2.04 elaboration: tactic execution took 2.04s
2.04 elaboration of span_gcd took 2.04s
2.04 elaboration: tactic execution took 2.04s
2.04 elaboration of has_strict_deriv_at_fpow took 2.04s
2.04 elaboration: tactic execution took 2.04s
2.04 elaboration of ball_0_eq took 2.04s
2.04 elaboration: tactic execution took 2.04s
2.04 elaboration: tactic execution took 2.04s
2.04 elaboration: tactic execution took 2.04s
2.04 decl post-processing of has_coe_to_sort took 2.04s
2.04 elaboration: tactic execution took 2.04s
2.04 elaboration of skew_prod took 2.04s
2.04 elaboration: tactic execution took 2.04s
2.03 elaboration: tactic execution took 2.03s
2.03 decl post-processing of gpowers_eq_closure took 2.03s
2.03 elaboration of add_comm_group took 2.03s
2.03 elaboration of sections_add_submonoid took 2.03s
2.03 decl post-processing of mem_comap took 2.03s
2.03 elaboration of is_basis_singleton_one took 2.03s
2.03 elaboration of convex_iff_forall_pos took 2.03s
2.03 elaboration: tactic execution took 2.03s
2.03 elaboration: tactic execution took 2.03s
2.03 elaboration: tactic execution took 2.03s
2.03 elaboration of is_st_unique' took 2.03s
2.03 elaboration: tactic execution took 2.03s
2.03 elaboration: tactic execution took 2.03s
2.03 elaboration: tactic execution took 2.03s
2.03 elaboration of total_comp took 2.03s
2.03 elaboration: tactic execution took 2.03s
2.03 elaboration: tactic execution took 2.03s
2.03 elaboration: tactic execution took 2.03s
2.03 elaboration: tactic execution took 2.03s
2.03 elaboration: tactic execution took 2.03s
2.03 elaboration: tactic execution took 2.03s
2.02 elaboration: tactic execution took 2.02s
2.02 elaboration: tactic execution took 2.02s
2.02 elaboration: tactic execution took 2.02s
2.02 elaboration: tactic execution took 2.02s
2.02 elaboration of proj_ker_of_right_inverse_comp_inv took 2.02s
2.02 elaboration of to_unique_factorization_domain took 2.02s
2.02 elaboration: tactic execution took 2.02s
2.02 elaboration: tactic execution took 2.02s
2.02 elaboration: tactic execution took 2.02s
2.02 elaboration: tactic execution took 2.02s
2.02 elaboration: tactic execution took 2.02s
2.02 elaboration: tactic execution took 2.02s
2.02 elaboration: tactic execution took 2.02s
2.02 elaboration: tactic execution took 2.02s
2.02 elaboration: tactic execution took 2.02s
2.01 elaboration: tactic execution took 2.01s
2.01 elaboration: tactic execution took 2.01s
2.01 elaboration of coeff_zero_eq_zero took 2.01s
2.01 elaboration of nat_degree_pow_eq took 2.01s
2.01 elaboration: tactic execution took 2.01s
2.01 elaboration of bind_comm took 2.01s
2.01 elaboration of to_complex_def' took 2.01s
2.01 elaboration: tactic execution took 2.01s
2.01 elaboration: tactic execution took 2.01s
2.01 elaboration of sum_div_fact_le took 2.01s
2.01 elaboration: tactic execution took 2.01s
2.01 elaboration of linear_independent.restrict_of_comp_subtype took 2.01s
2.01 elaboration: tactic execution took 2.01s
2.01 elaboration of has_fderiv_within_at_of_not_mem_closure took 2.01s
2.01 decl post-processing of right_coset_mem_right_coset took 2.01s
2.01 elaboration: tactic execution took 2.01s
2.01 elaboration: tactic execution took 2.01s
2.01 elaboration of degree_eq_zero_of_is_unit took 2.01s
2.01 elaboration: tactic execution took 2.01s
2.01 decl post-processing of eq_mul_inv_iff_mul_eq took 2.01s
2.01 elaboration: tactic execution took 2.01s
2 elaboration of linear_equiv.is_basis took 2s
2 elaboration of uniform_space_of_dist took 2s
2 elaboration: tactic execution took 2s
2 elaboration of bind_bind took 2s
2 elaboration: tactic execution took 2s
2 elaboration: tactic execution took 2s
2 elaboration: tactic execution took 2s
2 elaboration of rank_diagonal took 2s
2 elaboration: tactic execution took 2s
2 elaboration: tactic execution took 2s
2 decl post-processing of prod_map_def took 2s
2 elaboration: tactic execution took 2s
2 elaboration: tactic execution took 2s
2 elaboration: tactic execution took 2s
2 elaboration: tactic execution took 2s
2 elaboration: tactic execution took 2s
2 elaboration: tactic execution took 2s
2 elaboration: tactic execution took 2s
2 elaboration: tactic execution took 2s
2 elaboration: tactic execution took 2s
2 elaboration: tactic execution took 2s
2 elaboration: tactic execution took 2s
2 elaboration: tactic execution took 2s
2 elaboration of bilin_form.to_matrix_comp_left took 2s
2 elaboration: tactic execution took 2s
2 elaboration: tactic execution took 2s
2 elaboration: tactic execution took 2s
2 decl post-processing of closure_subset took 2s
2 elaboration: tactic execution took 2s
2 elaboration: tactic execution took 2s
2 elaboration: tactic execution took 2s
2 elaboration: tactic execution took 2s
2 elaboration: tactic execution took 2s
2 elaboration of range_total took 2s
1.99 elaboration: tactic execution took 1.99s
1.99 elaboration: tactic execution took 1.99s
1.99 elaboration: tactic execution took 1.99s
1.99 elaboration: tactic execution took 1.99s
1.99 elaboration: tactic execution took 1.99s
1.99 elaboration of mem_of_mem_perms_of_list took 1.99s
1.99 elaboration: tactic execution took 1.99s
1.99 elaboration: tactic execution took 1.99s
1.99 elaboration: tactic execution took 1.99s
1.99 elaboration of id_hom_app took 1.99s
1.99 elaboration: tactic execution took 1.99s
1.99 elaboration: tactic execution took 1.99s
1.99 elaboration of nat_abs_norm_mod_lt took 1.99s
1.99 elaboration of legendre_sym_eq_zero_iff took 1.99s
1.99 elaboration: tactic execution took 1.99s
1.99 elaboration: tactic execution took 1.99s
1.99 elaboration: tactic execution took 1.99s
1.99 elaboration: tactic execution took 1.99s
1.99 elaboration: tactic execution took 1.99s
1.99 elaboration: tactic execution took 1.99s
1.99 elaboration: tactic execution took 1.99s
1.99 decl post-processing of map_mul_inv took 1.99s
1.99 elaboration of bundle_mfderiv_chart_symm took 1.99s
1.99 elaboration: tactic execution took 1.99s
1.99 elaboration of CommGroup_iso_to_mul_equiv took 1.99s
1.99 elaboration: tactic execution took 1.99s
1.98 decl post-processing of eq_mul_inv_iff_mul_eq took 1.98s
1.98 elaboration: tactic execution took 1.98s
1.98 elaboration of pderivative_monomial_mul took 1.98s
1.98 elaboration: tactic execution took 1.98s
1.98 elaboration: tactic execution took 1.98s
1.98 elaboration of γ₁ took 1.98s
1.98 elaboration: tactic execution took 1.98s
1.98 elaboration of multilinear_map.curry_left took 1.98s
1.98 elaboration of is_basis_monomials took 1.98s
1.98 elaboration of eq_zero_of took 1.98s
1.98 elaboration: tactic execution took 1.98s
1.98 elaboration: tactic execution took 1.98s
1.98 elaboration of subtype_domain_def took 1.98s
1.98 elaboration: tactic execution took 1.98s
1.98 elaboration: tactic execution took 1.98s
1.98 elaboration: tactic execution took 1.98s
1.98 elaboration of gc_set took 1.98s
1.98 elaboration of degree_map_eq_of_leading_coeff_ne_zero took 1.98s
1.98 elaboration of ext took 1.98s
1.98 elaboration of coeff_zero_mul_X took 1.98s
1.98 elaboration: tactic execution took 1.98s
1.98 elaboration: tactic execution took 1.98s
1.98 elaboration: tactic execution took 1.98s
1.98 elaboration: tactic execution took 1.98s
1.98 elaboration of sum_two_squares took 1.98s
1.98 elaboration: tactic execution took 1.98s
1.98 elaboration of coe_neg took 1.98s
1.98 elaboration of div_by_monic_one took 1.98s
1.98 elaboration: tactic execution took 1.98s
1.98 elaboration: tactic execution took 1.98s
1.98 elaboration: tactic execution took 1.98s
1.98 decl post-processing of of took 1.98s
1.98 elaboration: tactic execution took 1.98s
1.98 elaboration: tactic execution took 1.98s
1.97 elaboration: tactic execution took 1.97s
1.97 elaboration: tactic execution took 1.97s
1.97 elaboration: tactic execution took 1.97s
1.97 elaboration: tactic execution took 1.97s
1.97 elaboration of mul_equiv.to_CommMon_iso took 1.97s
1.97 elaboration of finite_dimensional_iff_dim_lt_omega took 1.97s
1.97 elaboration: tactic execution took 1.97s
1.97 elaboration of root_multiplicity_eq_multiplicity took 1.97s
1.97 elaboration: tactic execution took 1.97s
1.97 elaboration: tactic execution took 1.97s
1.97 elaboration: tactic execution took 1.97s
1.97 elaboration: tactic execution took 1.97s
1.97 elaboration: tactic execution took 1.97s
1.97 elaboration: tactic execution took 1.97s
1.97 elaboration: tactic execution took 1.97s
1.97 decl post-processing of inv_inj' took 1.97s
1.97 elaboration: tactic execution took 1.97s
1.97 elaboration: tactic execution took 1.97s
1.97 elaboration of degree_eq_degree_of_associated took 1.97s
1.97 elaboration: tactic execution took 1.97s
1.97 elaboration: tactic execution took 1.97s
1.97 elaboration: tactic execution took 1.97s
1.96 elaboration: tactic execution took 1.96s
1.96 elaboration: tactic execution took 1.96s
1.96 elaboration of arg_eq_arg_iff took 1.96s
1.96 elaboration: tactic execution took 1.96s
1.96 elaboration of has_one took 1.96s
1.96 elaboration: tactic execution took 1.96s
1.96 decl post-processing of mul_right_injective took 1.96s
1.96 decl post-processing of mul_right_inj took 1.96s
1.96 elaboration: tactic execution took 1.96s
1.96 elaboration of smul_right_comp took 1.96s
1.96 elaboration: tactic execution took 1.96s
1.96 elaboration: tactic execution took 1.96s
1.96 elaboration: tactic execution took 1.96s
1.96 elaboration of ne_zero_of_mul_eq_one took 1.96s
1.96 elaboration: tactic execution took 1.96s
1.96 elaboration: tactic execution took 1.96s
1.96 elaboration: tactic execution took 1.96s
1.96 elaboration of E_trace_zero took 1.96s
1.96 elaboration of map_id took 1.96s
1.96 elaboration: tactic execution took 1.96s
1.95 elaboration: tactic execution took 1.95s
1.95 decl post-processing of comap_inf took 1.95s
1.95 decl post-processing of mul_mul_mul_comm took 1.95s
1.95 elaboration of Group_iso_to_mul_equiv took 1.95s
1.95 elaboration of mem_span_iff_total took 1.95s
1.95 elaboration of C_pow took 1.95s
1.95 elaboration: tactic execution took 1.95s
1.95 elaboration: tactic execution took 1.95s
1.95 elaboration: tactic execution took 1.95s
1.95 elaboration: tactic execution took 1.95s
1.95 elaboration: tactic execution took 1.95s
1.95 elaboration: tactic execution took 1.95s
1.95 elaboration: tactic execution took 1.95s
1.95 elaboration: tactic execution took 1.95s
1.95 elaboration: tactic execution took 1.95s
1.95 elaboration: tactic execution took 1.95s
1.95 elaboration: tactic execution took 1.95s
1.95 elaboration: tactic execution took 1.95s
1.95 elaboration of one_eq_span took 1.95s
1.95 elaboration: tactic execution took 1.95s
1.95 elaboration of monoid_colimit_type took 1.95s
1.95 elaboration: tactic execution took 1.95s
1.95 elaboration: tactic execution took 1.95s
1.95 elaboration: tactic execution took 1.95s
1.94 elaboration: tactic execution took 1.94s
1.94 elaboration of cauchy_product took 1.94s
1.94 decl post-processing of inv_eq_one took 1.94s
1.94 elaboration of support_sum took 1.94s
1.94 elaboration: tactic execution took 1.94s
1.94 elaboration: tactic execution took 1.94s
1.94 elaboration of linear_eq_on took 1.94s
1.94 elaboration of has_inf took 1.94s
1.94 elaboration: tactic execution took 1.94s
1.94 elaboration of sections_submonoid took 1.94s
1.94 elaboration: tactic execution took 1.94s
1.94 elaboration: tactic execution took 1.94s
1.94 elaboration of category_theory.limits.has_zero_morphisms took 1.94s
1.94 elaboration: tactic execution took 1.94s
1.94 elaboration: tactic execution took 1.94s
1.94 elaboration: tactic execution took 1.94s
1.94 elaboration: tactic execution took 1.94s
1.94 elaboration: tactic execution took 1.94s
1.94 elaboration of eq_C_of_degree_le_zero took 1.94s
1.94 elaboration: tactic execution took 1.94s
1.94 elaboration of ker_eq_bot took 1.94s
1.94 elaboration of isometry_subsingleton took 1.94s
1.93 elaboration: tactic execution took 1.93s
1.93 elaboration of continuous_inf_edist took 1.93s
1.93 elaboration of eq_X_add_C_of_degree_eq_one took 1.93s
1.93 elaboration: tactic execution took 1.93s
1.93 elaboration: tactic execution took 1.93s
1.93 elaboration: tactic execution took 1.93s
1.93 elaboration: tactic execution took 1.93s
1.93 elaboration: tactic execution took 1.93s
1.93 elaboration of map_pair_iso took 1.93s
1.93 elaboration of continuous_on.congr_mono took 1.93s
1.93 elaboration of splits_of_degree_eq_one took 1.93s
1.93 elaboration of continuous_edist took 1.93s
1.93 elaboration: tactic execution took 1.93s
1.93 elaboration of is_basis.repr_eq_single took 1.93s
1.93 elaboration: tactic execution took 1.93s
1.93 elaboration: tactic execution took 1.93s
1.93 elaboration of is_cobounded_principal took 1.93s
1.93 decl post-processing of has_le took 1.93s
1.93 elaboration: tactic execution took 1.93s
1.93 elaboration: tactic execution took 1.93s
1.93 elaboration: tactic execution took 1.93s
1.93 elaboration of lift_root took 1.93s
1.93 decl post-processing of is_unit_iff_exists_inv took 1.93s
1.93 elaboration: tactic execution took 1.93s
1.92 elaboration: tactic execution took 1.92s
1.92 elaboration of exists_subgroup_card_pow_prime took 1.92s
1.92 elaboration: tactic execution took 1.92s
1.92 elaboration: tactic execution took 1.92s
1.92 elaboration: tactic execution took 1.92s
1.92 elaboration: tactic execution took 1.92s
1.92 elaboration: tactic execution took 1.92s
1.92 elaboration of sections_add_subgroup took 1.92s
1.92 elaboration: tactic execution took 1.92s
1.92 elaboration: tactic execution took 1.92s
1.92 elaboration: tactic execution took 1.92s
1.92 elaboration: tactic execution took 1.92s
1.92 elaboration of finite_mul_aux took 1.92s
1.92 elaboration: tactic execution took 1.92s
1.92 decl post-processing of right_coset took 1.92s
1.92 elaboration: tactic execution took 1.92s
1.92 elaboration: tactic execution took 1.92s
1.92 elaboration of unshift took 1.92s
1.92 elaboration: tactic execution took 1.92s
1.92 elaboration: tactic execution took 1.92s
1.92 elaboration: tactic execution took 1.92s
1.92 elaboration of curry_obj took 1.92s
1.91 elaboration: tactic execution took 1.91s
1.91 elaboration of mk_self took 1.91s
1.91 elaboration of sections_add_submonoid took 1.91s
1.91 elaboration: tactic execution took 1.91s
1.91 decl post-processing of prod_congr took 1.91s
1.91 elaboration of to_module took 1.91s
1.91 elaboration: tactic execution took 1.91s
1.91 elaboration: tactic execution took 1.91s
1.91 elaboration of free_comm_ring_equiv_mv_polynomial_int took 1.91s
1.91 elaboration: tactic execution took 1.91s
1.91 elaboration: tactic execution took 1.91s
1.91 elaboration of coeff_coe_units_zero_ne_zero took 1.91s
1.91 elaboration of mk_eq took 1.91s
1.91 elaboration: tactic execution took 1.91s
1.91 elaboration: tactic execution took 1.91s
1.91 elaboration: tactic execution took 1.91s
1.91 decl post-processing of coe_mk took 1.91s
1.91 elaboration: tactic execution took 1.91s
1.91 elaboration: tactic execution took 1.91s
1.91 elaboration: tactic execution took 1.91s
1.91 elaboration: tactic execution took 1.91s
1.91 elaboration: tactic execution took 1.91s
1.91 elaboration of fractional_of_subset_one took 1.91s
1.9 elaboration of fg_pow took 1.9s
1.9 elaboration: tactic execution took 1.9s
1.9 elaboration of fold_add took 1.9s
1.9 elaboration of constr_add took 1.9s
1.9 elaboration: tactic execution took 1.9s
1.9 elaboration: tactic execution took 1.9s
1.9 elaboration: tactic execution took 1.9s
1.9 elaboration of linear_independent_inl_union_inr took 1.9s
1.9 elaboration: tactic execution took 1.9s
1.9 elaboration: tactic execution took 1.9s
1.9 elaboration: tactic execution took 1.9s
1.9 elaboration: tactic execution took 1.9s
1.9 elaboration of subsingleton took 1.9s
1.9 decl post-processing of inv took 1.9s
1.9 elaboration: tactic execution took 1.9s
1.89 elaboration: tactic execution took 1.89s
1.89 elaboration: tactic execution took 1.89s
1.89 elaboration: tactic execution took 1.89s
1.89 elaboration: tactic execution took 1.89s
1.89 elaboration: tactic execution took 1.89s
1.89 elaboration: tactic execution took 1.89s
1.89 decl post-processing of mem_left_coset_left_coset took 1.89s
1.89 elaboration of biproduct.π_epi took 1.89s
1.89 elaboration: tactic execution took 1.89s
1.89 elaboration: tactic execution took 1.89s
1.89 elaboration of dim_pi took 1.89s
1.89 elaboration: tactic execution took 1.89s
1.89 elaboration: tactic execution took 1.89s
1.89 elaboration: tactic execution took 1.89s
1.89 elaboration: tactic execution took 1.89s
1.89 elaboration: tactic execution took 1.89s
1.89 elaboration of lid took 1.89s
1.89 elaboration: tactic execution took 1.89s
1.89 elaboration of subsingleton_hom took 1.89s
1.89 elaboration of cone.of_fork took 1.89s
1.89 elaboration: tactic execution took 1.89s
1.88 elaboration of cocone.category took 1.88s
1.88 elaboration: tactic execution took 1.88s
1.88 elaboration: tactic execution took 1.88s
1.88 elaboration: tactic execution took 1.88s
1.88 elaboration: tactic execution took 1.88s
1.88 elaboration of comm_ring took 1.88s
1.88 elaboration: tactic execution took 1.88s
1.88 elaboration: tactic execution took 1.88s
1.88 elaboration of comm_semiring took 1.88s
1.88 elaboration: tactic execution took 1.88s
1.88 elaboration: tactic execution took 1.88s
1.88 elaboration: tactic execution took 1.88s
1.88 elaboration: tactic execution took 1.88s
1.88 elaboration of dim_eq_injective took 1.88s
1.88 elaboration of monic_mul took 1.88s
1.88 elaboration: tactic execution took 1.88s
1.88 decl post-processing of mul_right_eq_self took 1.88s
1.88 elaboration: tactic execution took 1.88s
1.88 elaboration of lie_quotient_has_bracket took 1.88s
1.88 elaboration: tactic execution took 1.88s
1.88 elaboration of exists_antimono_seq took 1.88s
1.88 elaboration of fintype_hom took 1.88s
1.87 elaboration: tactic execution took 1.87s
1.87 elaboration: tactic execution took 1.87s
1.87 elaboration: tactic execution took 1.87s
1.87 elaboration: tactic execution took 1.87s
1.87 elaboration of segment_eq_Icc took 1.87s
1.87 elaboration: tactic execution took 1.87s
1.87 elaboration of sup_aux took 1.87s
1.87 elaboration: tactic execution took 1.87s
1.87 elaboration of to_quadratic_form took 1.87s
1.87 elaboration of zero_le took 1.87s
1.87 elaboration: tactic execution took 1.87s
1.87 elaboration: tactic execution took 1.87s
1.87 elaboration: tactic execution took 1.87s
1.86 elaboration: tactic execution took 1.86s
1.86 elaboration: tactic execution took 1.86s
1.86 elaboration: tactic execution took 1.86s
1.86 elaboration: tactic execution took 1.86s
1.86 elaboration of associativity took 1.86s
1.86 elaboration of linear_independent.injective took 1.86s
1.86 elaboration: tactic execution took 1.86s
1.86 elaboration: tactic execution took 1.86s
1.86 elaboration of findim_eq_card_basis' took 1.86s
1.86 elaboration: tactic execution took 1.86s
1.86 elaboration: tactic execution took 1.86s
1.86 elaboration of cokernel.zero_cocone took 1.86s
1.86 elaboration of of_smul took 1.86s
1.86 elaboration: tactic execution took 1.86s
1.86 elaboration of summable.summable_comp_of_injective took 1.86s
1.85 elaboration: tactic execution took 1.85s
1.85 elaboration: tactic execution took 1.85s
1.85 elaboration: tactic execution took 1.85s
1.85 elaboration of comap_id took 1.85s
1.85 elaboration: tactic execution took 1.85s
1.85 elaboration of div_by_monic_mul_pow_root_multiplicity_eq took 1.85s
1.85 elaboration: tactic execution took 1.85s
1.85 elaboration: tactic execution took 1.85s
1.85 elaboration: tactic execution took 1.85s
1.85 elaboration of mem_zero_iff took 1.85s
1.85 elaboration: tactic execution took 1.85s
1.85 elaboration of has_zero took 1.85s
1.85 elaboration: tactic execution took 1.85s
1.85 elaboration: tactic execution took 1.85s
1.85 elaboration: tactic execution took 1.85s
1.85 elaboration of erase_def took 1.85s
1.85 elaboration: tactic execution took 1.85s
1.85 elaboration: tactic execution took 1.85s
1.85 elaboration: tactic execution took 1.85s
1.85 elaboration: tactic execution took 1.85s
1.84 elaboration: tactic execution took 1.84s
1.84 elaboration: tactic execution took 1.84s
1.84 elaboration of to_cone took 1.84s
1.84 elaboration: tactic execution took 1.84s
1.84 elaboration: tactic execution took 1.84s
1.84 elaboration: tactic execution took 1.84s
1.84 elaboration of constr_basis took 1.84s
1.84 elaboration: tactic execution took 1.84s
1.84 elaboration: tactic execution took 1.84s
1.84 elaboration: tactic execution took 1.84s
1.84 elaboration of antimono_seq_of_seq took 1.84s
1.84 elaboration: tactic execution took 1.84s
1.84 elaboration: tactic execution took 1.84s
1.84 elaboration of union_zero_locus took 1.84s
1.84 elaboration: tactic execution took 1.84s
1.84 elaboration: tactic execution took 1.84s
1.84 elaboration of vanishing_ideal_univ took 1.84s
1.84 elaboration: tactic execution took 1.84s
1.84 elaboration of div_X_eq_zero_iff took 1.84s
1.83 elaboration: tactic execution took 1.83s
1.83 elaboration: tactic execution took 1.83s
1.83 elaboration: tactic execution took 1.83s
1.83 elaboration: tactic execution took 1.83s
1.83 elaboration: tactic execution took 1.83s
1.83 elaboration of emetric.cauchy_seq_iff_le_tendsto_0 took 1.83s
1.83 elaboration: tactic execution took 1.83s
1.83 elaboration: tactic execution took 1.83s
1.83 elaboration: tactic execution took 1.83s
1.83 elaboration of to_cocone took 1.83s
1.83 elaboration of adj took 1.83s
1.83 elaboration of module took 1.83s
1.83 elaboration of Icc_mem_nhds took 1.83s
1.83 elaboration: tactic execution took 1.83s
1.83 elaboration: tactic execution took 1.83s
1.83 elaboration of parallel_pair took 1.83s
1.83 elaboration: tactic execution took 1.83s
1.83 elaboration of real.bounded_iff_bdd_below_bdd_above took 1.83s
1.83 elaboration of kernel.zero_cone took 1.83s
1.83 elaboration of card_modeq_card_fixed_points took 1.83s
1.83 elaboration of uniform_space.comap took 1.83s
1.82 elaboration of convex_on_iff_div took 1.82s
1.82 elaboration: tactic execution took 1.82s
1.82 elaboration: tactic execution took 1.82s
1.82 elaboration: tactic execution took 1.82s
1.82 elaboration: tactic execution took 1.82s
1.82 elaboration: tactic execution took 1.82s
1.82 elaboration: tactic execution took 1.82s
1.82 elaboration: tactic execution took 1.82s
1.82 elaboration of comap_eq_trans took 1.82s
1.82 elaboration: tactic execution took 1.82s
1.82 elaboration: tactic execution took 1.82s
1.82 elaboration: tactic execution took 1.82s
1.82 elaboration: tactic execution took 1.82s
1.82 elaboration: tactic execution took 1.82s
1.81 elaboration of im took 1.81s
1.81 elaboration: tactic execution took 1.81s
1.81 elaboration: tactic execution took 1.81s
1.81 elaboration of exists_finite_card_le_of_finite_of_linear_independent_of_span took 1.81s
1.81 elaboration: tactic execution took 1.81s
1.81 elaboration of degree_map_eq_of_injective took 1.81s
1.81 elaboration of filter_def took 1.81s
1.81 elaboration of nonzero_iff_val_nonzero took 1.81s
1.81 elaboration: tactic execution took 1.81s
1.81 elaboration: tactic execution took 1.81s
1.81 elaboration of equalizer_cone_is_limit took 1.81s
1.81 elaboration: tactic execution took 1.81s
1.81 elaboration: tactic execution took 1.81s
1.81 elaboration: tactic execution took 1.81s
1.81 elaboration of det_permutation took 1.81s
1.81 elaboration: tactic execution took 1.81s
1.81 elaboration of extensions took 1.81s
1.81 elaboration of prod.metric_space_max took 1.81s
1.81 elaboration of lift.principal_seg took 1.81s
1.8 elaboration: tactic execution took 1.8s
1.8 elaboration of forget_limit_is_limit took 1.8s
1.8 elaboration: tactic execution took 1.8s
1.8 elaboration: tactic execution took 1.8s
1.8 elaboration: tactic execution took 1.8s
1.8 elaboration: tactic execution took 1.8s
1.8 elaboration of findim_fin_fun took 1.8s
1.8 elaboration: tactic execution took 1.8s
1.8 decl post-processing of map took 1.8s
1.8 elaboration: tactic execution took 1.8s
1.8 elaboration: tactic execution took 1.8s
1.8 elaboration of comp_X took 1.8s
1.8 elaboration: tactic execution took 1.8s
1.8 elaboration: tactic execution took 1.8s
1.8 decl post-processing of eq_of_eq_on_mdense took 1.8s
1.8 elaboration: tactic execution took 1.8s
1.8 elaboration of mem_sup took 1.8s
1.8 elaboration: tactic execution took 1.8s
1.79 elaboration: tactic execution took 1.79s
1.79 elaboration of alg_hom_int took 1.79s
1.79 elaboration: tactic execution took 1.79s
1.79 elaboration: tactic execution took 1.79s
1.79 elaboration of r_eq_r' took 1.79s
1.79 elaboration of range_coprod took 1.79s
1.79 elaboration: tactic execution took 1.79s
1.79 elaboration of rat.uniform_continuous_add took 1.79s
1.79 elaboration of comap_comp took 1.79s
1.79 elaboration of fintype_hom took 1.79s
1.79 elaboration: tactic execution took 1.79s
1.79 elaboration of eq_zero_iff took 1.79s
1.79 elaboration: tactic execution took 1.79s
1.79 elaboration of pullback_fst_eq_pullback_snd took 1.79s
1.79 elaboration: tactic execution took 1.79s
1.79 elaboration of diff_eq_self took 1.79s
1.79 elaboration of dim_fin_fun took 1.79s
1.79 elaboration: tactic execution took 1.79s
1.79 elaboration: tactic execution took 1.79s
1.78 elaboration of comp_hom_app took 1.78s
1.78 elaboration: tactic execution took 1.78s
1.78 elaboration: tactic execution took 1.78s
1.78 elaboration: tactic execution took 1.78s
1.78 decl post-processing of head_mul_tail_prod' took 1.78s
1.78 elaboration: tactic execution took 1.78s
1.78 elaboration of nat_trans_in_over took 1.78s
1.78 elaboration: tactic execution took 1.78s
1.78 elaboration: tactic execution took 1.78s
1.78 elaboration: tactic execution took 1.78s
1.78 elaboration of C_0 took 1.78s
1.78 decl post-processing of symm_apply_apply took 1.78s
1.78 elaboration: tactic execution took 1.78s
1.77 elaboration: tactic execution took 1.77s
1.77 elaboration: tactic execution took 1.77s
1.77 elaboration: tactic execution took 1.77s
1.77 elaboration: tactic execution took 1.77s
1.77 elaboration: tactic execution took 1.77s
1.77 elaboration: tactic execution took 1.77s
1.77 elaboration: tactic execution took 1.77s
1.77 elaboration: tactic execution took 1.77s
1.77 elaboration: tactic execution took 1.77s
1.77 elaboration of structomorph.trans took 1.77s
1.77 elaboration: tactic execution took 1.77s
1.77 elaboration: tactic execution took 1.77s
1.77 elaboration of finset.prod_univ_pi took 1.77s
1.77 elaboration of prod_involution took 1.77s
1.77 elaboration: tactic execution took 1.77s
1.77 elaboration: tactic execution took 1.77s
1.77 elaboration: tactic execution took 1.77s
1.77 elaboration: tactic execution took 1.77s
1.77 elaboration: tactic execution took 1.77s
1.76 elaboration of map_piecewise_smul took 1.76s
1.76 elaboration: tactic execution took 1.76s
1.76 elaboration: tactic execution took 1.76s
1.76 elaboration: tactic execution took 1.76s
1.76 elaboration: tactic execution took 1.76s
1.76 elaboration: tactic execution took 1.76s
1.76 elaboration of fork.of_ι took 1.76s
1.76 elaboration: tactic execution took 1.76s
1.76 elaboration: tactic execution took 1.76s
1.76 elaboration of is_cycle_inv took 1.76s
1.76 elaboration: tactic execution took 1.76s
1.76 elaboration: tactic execution took 1.76s
1.76 elaboration of C_mul_monomial took 1.76s
1.76 decl post-processing of fin.prod_univ_zero took 1.76s
1.76 elaboration: tactic execution took 1.76s
1.76 elaboration: tactic execution took 1.76s
1.76 elaboration: tactic execution took 1.76s
1.76 elaboration: tactic execution took 1.76s
1.76 elaboration: tactic execution took 1.76s
1.76 elaboration of hom_iso took 1.76s
1.75 elaboration: tactic execution took 1.75s
1.75 elaboration: tactic execution took 1.75s
1.75 elaboration: tactic execution took 1.75s
1.75 elaboration: tactic execution took 1.75s
1.75 elaboration: tactic execution took 1.75s
1.75 elaboration of of_subtype took 1.75s
1.75 elaboration: tactic execution took 1.75s
1.75 elaboration: tactic execution took 1.75s
1.75 decl post-processing of mul_eq_one_iff_eq_inv took 1.75s
1.75 elaboration of comp_inv_app took 1.75s
1.75 elaboration of convex_empty took 1.75s
1.75 elaboration: tactic execution took 1.75s
1.75 elaboration of nat_degree_neg took 1.75s
1.75 elaboration: tactic execution took 1.75s
1.75 elaboration: tactic execution took 1.75s
1.75 elaboration: tactic execution took 1.75s
1.75 elaboration of has_zero_object_punit took 1.75s
1.75 elaboration of det_zero_of_column_eq took 1.75s
1.75 elaboration: tactic execution took 1.75s
1.75 elaboration of forget_colimit_is_colimit took 1.75s
1.75 elaboration: tactic execution took 1.75s
1.75 elaboration: tactic execution took 1.75s
1.75 elaboration of X_ne_zero took 1.75s
1.75 elaboration: tactic execution took 1.75s
1.75 elaboration of sections_add_subgroup took 1.75s
1.74 elaboration of lift_aux.smul took 1.74s
1.74 elaboration: tactic execution took 1.74s
1.74 elaboration: tactic execution took 1.74s
1.74 elaboration: tactic execution took 1.74s
1.74 elaboration: tactic execution took 1.74s
1.74 elaboration: tactic execution took 1.74s
1.74 elaboration: tactic execution took 1.74s
1.74 elaboration: tactic execution took 1.74s
1.74 elaboration: tactic execution took 1.74s
1.74 elaboration of uniform_space.core.to_topological_space took 1.74s
1.74 elaboration: tactic execution took 1.74s
1.74 elaboration: tactic execution took 1.74s
1.74 elaboration: tactic execution took 1.74s
1.74 elaboration: tactic execution took 1.74s
1.74 elaboration: tactic execution took 1.74s
1.74 elaboration of nat_degree_int_cast took 1.74s
1.74 elaboration: tactic execution took 1.74s
1.73 elaboration: tactic execution took 1.73s
1.73 elaboration: tactic execution took 1.73s
1.73 elaboration of is_basis_fun took 1.73s
1.73 elaboration: tactic execution took 1.73s
1.73 elaboration: tactic execution took 1.73s
1.73 elaboration: tactic execution took 1.73s
1.73 elaboration: tactic execution took 1.73s
1.73 elaboration: tactic execution took 1.73s
1.73 elaboration: tactic execution took 1.73s
1.73 elaboration: tactic execution took 1.73s
1.73 elaboration of ne_zero_of_linear_independent took 1.73s
1.73 elaboration of induced_order_topology' took 1.73s
1.73 elaboration: tactic execution took 1.73s
1.73 elaboration of cofork.of_π took 1.73s
1.73 elaboration: tactic execution took 1.73s
1.73 elaboration: tactic execution took 1.73s
1.72 elaboration: tactic execution took 1.72s
1.72 elaboration of tendsto_multiset_prod took 1.72s
1.72 elaboration: tactic execution took 1.72s
1.72 elaboration: tactic execution took 1.72s
1.72 elaboration: tactic execution took 1.72s
1.72 elaboration: tactic execution took 1.72s
1.72 elaboration: tactic execution took 1.72s
1.72 elaboration: tactic execution took 1.72s
1.71 elaboration: tactic execution took 1.71s
1.71 elaboration: tactic execution took 1.71s
1.71 elaboration of fintype took 1.71s
1.71 elaboration: tactic execution took 1.71s
1.71 elaboration of γ₂ took 1.71s
1.71 elaboration of groupoid took 1.71s
1.71 elaboration: tactic execution took 1.71s
1.71 elaboration: tactic execution took 1.71s
1.71 elaboration: tactic execution took 1.71s
1.71 elaboration of swap_mul_eq_mul_swap took 1.71s
1.71 elaboration of sign_aux_mul took 1.71s
1.71 elaboration: tactic execution took 1.71s
1.7 elaboration of is_closed took 1.7s
1.7 decl post-processing of top_prod_top took 1.7s
1.7 elaboration: tactic execution took 1.7s
1.7 elaboration: tactic execution took 1.7s
1.7 elaboration of of.is_ring_hom took 1.7s
1.7 elaboration: tactic execution took 1.7s
1.7 elaboration of cone.category took 1.7s
1.7 elaboration: tactic execution took 1.7s
1.7 elaboration of comp_linear_map took 1.7s
1.7 elaboration: tactic execution took 1.7s
1.7 elaboration: tactic execution took 1.7s
1.7 elaboration: tactic execution took 1.7s
1.7 elaboration of is_open_of_nonempty_open_subset took 1.7s
1.7 elaboration: tactic execution took 1.7s
1.7 elaboration: tactic execution took 1.7s
1.7 elaboration: tactic execution took 1.7s
1.7 elaboration: tactic execution took 1.7s
1.7 elaboration: tactic execution took 1.7s
1.7 elaboration: tactic execution took 1.7s
1.7 decl post-processing of mk' took 1.7s
1.7 elaboration: tactic execution took 1.7s
1.7 elaboration of continuous_multiset_prod took 1.7s
1.7 elaboration: tactic execution took 1.7s
1.69 elaboration: tactic execution took 1.69s
1.69 elaboration: tactic execution took 1.69s
1.69 elaboration of rec_prim took 1.69s
1.69 elaboration of module took 1.69s
1.69 elaboration: tactic execution took 1.69s
1.69 elaboration: tactic execution took 1.69s
1.69 elaboration: tactic execution took 1.69s
1.69 elaboration of topological_group.regular_space took 1.69s
1.69 elaboration: tactic execution took 1.69s
1.69 elaboration: tactic execution took 1.69s
1.69 elaboration: tactic execution took 1.69s
1.69 elaboration: tactic execution took 1.69s
1.69 elaboration: tactic execution took 1.69s
1.69 elaboration: tactic execution took 1.69s
1.69 elaboration: tactic execution took 1.69s
1.69 elaboration of mod_swap took 1.69s
1.68 decl post-processing of mul_inv_eq_one took 1.68s
1.68 elaboration: tactic execution took 1.68s
1.68 elaboration of single_mul_apply_aux took 1.68s
1.68 elaboration: tactic execution took 1.68s
1.68 elaboration of mul_le_mul_left took 1.68s
1.68 elaboration: tactic execution took 1.68s
1.68 elaboration: tactic execution took 1.68s
1.68 elaboration: tactic execution took 1.68s
1.68 elaboration: tactic execution took 1.68s
1.68 elaboration: tactic execution took 1.68s
1.68 elaboration: tactic execution took 1.68s
1.68 elaboration of to_units took 1.68s
1.68 elaboration: tactic execution took 1.68s
1.68 elaboration of submodule.sup_eq_range took 1.68s
1.68 elaboration of prod_sup_prod took 1.68s
1.68 elaboration: tactic execution took 1.68s
1.68 elaboration: tactic execution took 1.68s
1.68 elaboration: tactic execution took 1.68s
1.68 elaboration: tactic execution took 1.68s
1.67 elaboration of complete took 1.67s
1.67 elaboration of single_eq_algebra_map_mul_of took 1.67s
1.67 decl post-processing of inv_comm_of_comm took 1.67s
1.67 elaboration: tactic execution took 1.67s
1.67 elaboration of one_mul took 1.67s
1.67 elaboration: tactic execution took 1.67s
1.67 elaboration: tactic execution took 1.67s
1.67 elaboration of model_with_corners_euclidean_quadrant took 1.67s
1.67 elaboration: tactic execution took 1.67s
1.67 elaboration: tactic execution took 1.67s
1.67 elaboration: tactic execution took 1.67s
1.67 elaboration of emetric_space_pi took 1.67s
1.67 elaboration: tactic execution took 1.67s
1.67 elaboration: tactic execution took 1.67s
1.67 elaboration of cohomology_map took 1.67s
1.67 elaboration: tactic execution took 1.67s
1.67 elaboration of prod.symmetry' took 1.67s
1.67 elaboration of mem_tangent_cone_of_segment_subset took 1.67s
1.67 elaboration of normed_ring_top_monoid took 1.67s
1.67 elaboration of exists_subset_is_basis took 1.67s
1.67 elaboration: tactic execution took 1.67s
1.67 elaboration of coeff_C_mul_X took 1.67s
1.67 elaboration: tactic execution took 1.67s
1.67 elaboration: tactic execution took 1.67s
1.67 elaboration: tactic execution took 1.67s
1.67 decl post-processing of prod took 1.67s
1.67 elaboration: tactic execution took 1.67s
1.67 elaboration of split_eq_scale_split' took 1.67s
1.66 elaboration: tactic execution took 1.66s
1.66 elaboration: tactic execution took 1.66s
1.66 elaboration: tactic execution took 1.66s
1.66 elaboration: tactic execution took 1.66s
1.66 elaboration: tactic execution took 1.66s
1.66 elaboration: tactic execution took 1.66s
1.66 elaboration: tactic execution took 1.66s
1.66 elaboration of hom_iso took 1.66s
1.66 elaboration of injective_of_mono took 1.66s
1.66 elaboration of semimodule took 1.66s
1.66 elaboration: tactic execution took 1.66s
1.66 elaboration: tactic execution took 1.66s
1.66 elaboration: tactic execution took 1.66s
1.66 elaboration of image_to_kernel_map took 1.66s
1.66 decl post-processing of is_unit_iff_exists_inv' took 1.66s
1.66 elaboration: tactic execution took 1.66s
1.66 elaboration: tactic execution took 1.66s
1.66 elaboration: tactic execution took 1.66s
1.65 elaboration of has_sum_iff_has_sum_of_ne_zero_bij took 1.65s
1.65 elaboration of linear_independent.repr_eq_single took 1.65s
1.65 elaboration: tactic execution took 1.65s
1.65 elaboration of cycle_factors_aux took 1.65s
1.65 elaboration of add_left took 1.65s
1.65 elaboration: tactic execution took 1.65s
1.65 elaboration of sum_bernoulli took 1.65s
1.65 elaboration of smul_lie took 1.65s
1.65 elaboration of image.pre_comp took 1.65s
1.65 elaboration: tactic execution took 1.65s
1.65 elaboration: tactic execution took 1.65s
1.65 elaboration: tactic execution took 1.65s
1.65 elaboration: tactic execution took 1.65s
1.65 elaboration of of_aux_relabelling took 1.65s
1.65 decl post-processing of prod_hom took 1.65s
1.65 decl post-processing of prod_nil took 1.65s
1.65 elaboration: tactic execution took 1.65s
1.65 elaboration of metric_space_pi took 1.65s
1.65 elaboration: tactic execution took 1.65s
1.65 elaboration: tactic execution took 1.65s
1.65 elaboration: tactic execution took 1.65s
1.64 elaboration: tactic execution took 1.64s
1.64 elaboration of decidable_linear_ordered_add_comm_group.tendsto_nhds took 1.64s
1.64 elaboration: tactic execution took 1.64s
1.64 elaboration of tsum_nonneg took 1.64s
1.64 elaboration of has_add took 1.64s
1.64 elaboration: tactic execution took 1.64s
1.64 elaboration: tactic execution took 1.64s
1.64 elaboration: tactic execution took 1.64s
1.64 elaboration of support_erase took 1.64s
1.64 elaboration of associativity took 1.64s
1.64 elaboration: tactic execution took 1.64s
1.64 elaboration of bind.summable took 1.64s
1.64 elaboration: tactic execution took 1.64s
1.64 elaboration: tactic execution took 1.64s
1.64 elaboration: tactic execution took 1.64s
1.64 elaboration: tactic execution took 1.64s
1.64 elaboration: tactic execution took 1.64s
1.64 elaboration: tactic execution took 1.64s
1.63 elaboration: tactic execution took 1.63s
1.63 decl post-processing of normal_of_eq_cosets took 1.63s
1.63 elaboration: tactic execution took 1.63s
1.63 elaboration of colimit_cocone took 1.63s
1.63 elaboration: tactic execution took 1.63s
1.63 elaboration of tendsto_locally_uniformly_iff took 1.63s
1.63 elaboration of bernoulli took 1.63s
1.63 elaboration: tactic execution took 1.63s
1.63 elaboration: tactic execution took 1.63s
1.63 elaboration: tactic execution took 1.63s
1.63 elaboration of category_theory.is_iso took 1.63s
1.63 elaboration of tr_supports took 1.63s
1.63 elaboration: tactic execution took 1.63s
1.63 elaboration: tactic execution took 1.63s
1.63 elaboration: tactic execution took 1.63s
1.63 elaboration of map_coprod_prod took 1.63s
1.63 elaboration of prod.right_unitor took 1.63s
1.62 elaboration of nonunits_add took 1.62s
1.62 elaboration: tactic execution took 1.62s
1.62 elaboration: tactic execution took 1.62s
1.62 elaboration: tactic execution took 1.62s
1.62 elaboration: tactic execution took 1.62s
1.62 elaboration of mul_Sup took 1.62s
1.62 elaboration of coeff_single took 1.62s
1.62 elaboration of constr_neg took 1.62s
1.62 elaboration: tactic execution took 1.62s
1.62 elaboration: tactic execution took 1.62s
1.62 elaboration: tactic execution took 1.62s
1.62 elaboration of coe_le_one took 1.62s
1.62 elaboration: tactic execution took 1.62s
1.62 elaboration: tactic execution took 1.62s
1.62 elaboration of tsum_equiv took 1.62s
1.62 elaboration: tactic execution took 1.62s
1.62 elaboration: tactic execution took 1.62s
1.61 elaboration: tactic execution took 1.61s
1.61 elaboration of order_iso.cof.aux took 1.61s
1.61 elaboration: tactic execution took 1.61s
1.61 elaboration of irreducible_induction_on took 1.61s
1.61 elaboration: tactic execution took 1.61s
1.61 elaboration: tactic execution took 1.61s
1.61 elaboration: tactic execution took 1.61s
1.61 elaboration: tactic execution took 1.61s
1.61 elaboration of adjugate_transpose took 1.61s
1.61 elaboration of coeff_C took 1.61s
1.61 elaboration: tactic execution took 1.61s
1.61 elaboration: tactic execution took 1.61s
1.61 elaboration: tactic execution took 1.61s
1.61 elaboration of lie_zero took 1.61s
1.61 decl post-processing of ext_iff took 1.61s
1.61 elaboration: tactic execution took 1.61s
1.61 decl post-processing of lift_coe took 1.61s
1.61 elaboration of lift_mono took 1.61s
1.6 elaboration of cohomology_map_condition took 1.6s
1.6 elaboration: tactic execution took 1.6s
1.6 elaboration: tactic execution took 1.6s
1.6 elaboration: tactic execution took 1.6s
1.6 elaboration of gcd.induction took 1.6s
1.6 elaboration: tactic execution took 1.6s
1.6 elaboration of step took 1.6s
1.6 elaboration: tactic execution took 1.6s
1.6 elaboration: tactic execution took 1.6s
1.6 elaboration: tactic execution took 1.6s
1.6 elaboration of of.zero_exact_aux took 1.6s
1.6 elaboration: tactic execution took 1.6s
1.6 elaboration: tactic execution took 1.6s
1.6 elaboration of rid_tmul took 1.6s
1.6 elaboration of continuous_if took 1.6s
1.6 elaboration of evaln_mono took 1.6s
1.6 elaboration: tactic execution took 1.6s
1.6 elaboration of quot_ker_equiv_range took 1.6s
1.6 elaboration: tactic execution took 1.6s
1.6 elaboration: tactic execution took 1.6s
1.6 elaboration: tactic execution took 1.6s
1.6 elaboration of has_image_map.factor_map took 1.6s
1.59 elaboration: tactic execution took 1.59s
1.59 elaboration of total_range took 1.59s
1.59 elaboration: tactic execution took 1.59s
1.59 elaboration of dist_pi_lt_iff took 1.59s
1.59 elaboration: tactic execution took 1.59s
1.59 elaboration: tactic execution took 1.59s
1.59 elaboration of supr_add_supr took 1.59s
1.59 elaboration: tactic execution took 1.59s
1.59 elaboration: tactic execution took 1.59s
1.59 elaboration: tactic execution took 1.59s
1.59 elaboration of nat_degree_nat_cast took 1.59s
1.59 elaboration of add_right took 1.59s
1.59 elaboration: tactic execution took 1.59s
1.59 elaboration: tactic execution took 1.59s
1.59 decl post-processing of mul_left_eq_self took 1.59s
1.59 elaboration of lie_skew took 1.59s
1.58 elaboration of finite_int_iff took 1.58s
1.58 decl post-processing of id_comp took 1.58s
1.58 elaboration: tactic execution took 1.58s
1.58 elaboration: tactic execution took 1.58s
1.58 elaboration: tactic execution took 1.58s
1.58 elaboration: tactic execution took 1.58s
1.58 elaboration: tactic execution took 1.58s
1.58 elaboration: tactic execution took 1.58s
1.58 elaboration: tactic execution took 1.58s
1.58 decl post-processing of coe_bot took 1.58s
1.58 elaboration: tactic execution took 1.58s
1.58 elaboration: tactic execution took 1.58s
1.58 elaboration of is_lawful_traversable took 1.58s
1.58 elaboration: tactic execution took 1.58s
1.58 elaboration: tactic execution took 1.58s
1.58 elaboration of mk_eq took 1.58s
1.58 elaboration: tactic execution took 1.58s
1.58 elaboration of mk_compl_eq_mk_compl_finite_lift took 1.58s
1.58 elaboration: tactic execution took 1.58s
1.58 elaboration of extend_Z_bilin took 1.58s
1.58 elaboration: tactic execution took 1.58s
1.58 elaboration: tactic execution took 1.58s
1.57 elaboration: tactic execution took 1.57s
1.57 elaboration of coprod.symmetry' took 1.57s
1.57 elaboration: tactic execution took 1.57s
1.57 elaboration of iso_ext took 1.57s
1.57 elaboration: tactic execution took 1.57s
1.57 elaboration: tactic execution took 1.57s
1.57 elaboration of coe_bind_apply took 1.57s
1.57 elaboration: tactic execution took 1.57s
1.57 elaboration: tactic execution took 1.57s
1.57 elaboration of adjugate_eq_one_of_card_eq_one took 1.57s
1.57 elaboration: tactic execution took 1.57s
1.57 elaboration: tactic execution took 1.57s
1.57 elaboration: tactic execution took 1.57s
1.57 decl post-processing of to_monoid_hom took 1.57s
1.57 elaboration of mdifferentiable_at_atlas took 1.57s
1.57 elaboration of uncurry took 1.57s
1.57 elaboration of endomorphism_ring took 1.57s
1.56 elaboration: tactic execution took 1.56s
1.56 elaboration: tactic execution took 1.56s
1.56 elaboration of ext took 1.56s
1.56 elaboration of ker_eq_bot' took 1.56s
1.56 elaboration: tactic execution took 1.56s
1.56 decl post-processing of prod_bind took 1.56s
1.56 elaboration: tactic execution took 1.56s
1.56 elaboration of add_comm_group took 1.56s
1.56 elaboration of uniform_space_core took 1.56s
1.56 elaboration of comm_ring took 1.56s
1.56 elaboration: tactic execution took 1.56s
1.56 elaboration: tactic execution took 1.56s
1.56 elaboration of category_theory.epi took 1.56s
1.56 elaboration: tactic execution took 1.56s
1.56 elaboration: tactic execution took 1.56s
1.56 elaboration of matrix_mul_apply took 1.56s
1.56 elaboration of semimodule took 1.56s
1.56 elaboration of fix_aux took 1.56s
1.56 elaboration: tactic execution took 1.56s
1.56 elaboration of kernel_map_id took 1.56s
1.55 decl post-processing of inv_mul_eq_iff_eq_mul took 1.55s
1.55 elaboration: tactic execution took 1.55s
1.55 elaboration: tactic execution took 1.55s
1.55 elaboration of le_tsum took 1.55s
1.55 elaboration of pilex.partial_order took 1.55s
1.55 elaboration: tactic execution took 1.55s
1.55 elaboration of kernel_map_condition took 1.55s
1.55 elaboration of nhds_top took 1.55s
1.55 decl post-processing of mem_coe took 1.55s
1.55 elaboration of mk_pi_ring took 1.55s
1.55 elaboration: tactic execution took 1.55s
1.55 elaboration: tactic execution took 1.55s
1.55 elaboration of quotient_ring_saturate took 1.55s
1.55 elaboration: tactic execution took 1.55s
1.55 elaboration of direct_sum took 1.55s
1.55 elaboration: tactic execution took 1.55s
1.55 elaboration: tactic execution took 1.55s
1.55 elaboration of sign_aux_eq_sign_aux2 took 1.55s
1.54 elaboration of topological_space.second_countable_topology took 1.54s
1.54 elaboration: tactic execution took 1.54s
1.54 decl post-processing of prod_eq_multiset_prod took 1.54s
1.54 elaboration: tactic execution took 1.54s
1.54 elaboration of infi_ker_proj_equiv took 1.54s
1.54 elaboration of monomial_zero_eq_C_apply took 1.54s
1.54 elaboration: tactic execution took 1.54s
1.54 elaboration of coprod.right_unitor took 1.54s
1.54 elaboration of free took 1.54s
1.54 elaboration of cos_inj_of_nonneg_of_le_pi took 1.54s
1.54 elaboration: tactic execution took 1.54s
1.54 elaboration of finset_sum_supr_nat took 1.54s
1.54 elaboration: tactic execution took 1.54s
1.54 elaboration of ring took 1.54s
1.54 elaboration of total_single took 1.54s
1.54 elaboration: tactic execution took 1.54s
1.54 elaboration: tactic execution took 1.54s
1.54 elaboration: tactic execution took 1.54s
1.54 elaboration of disjoint_filter took 1.54s
1.54 elaboration of mul_le_mul_right took 1.54s
1.54 elaboration of rec_computable took 1.54s
1.53 elaboration: tactic execution took 1.53s
1.53 elaboration: tactic execution took 1.53s
1.53 elaboration of rec_prim' took 1.53s
1.53 elaboration: tactic execution took 1.53s
1.53 elaboration of id took 1.53s
1.53 elaboration of mul_le_mul_left took 1.53s
1.53 elaboration: tactic execution took 1.53s
1.53 elaboration of scale_power_aux took 1.53s
1.53 decl post-processing of is_unit.map took 1.53s
1.53 elaboration: tactic execution took 1.53s
1.53 elaboration of continuous_on_iff took 1.53s
1.53 elaboration of prod_take_of_fn took 1.53s
1.53 decl post-processing of lift_restrict took 1.53s
1.53 elaboration: tactic execution took 1.53s
1.52 elaboration of eval_equiv took 1.52s
1.52 elaboration of coe_tsum took 1.52s
1.52 elaboration: tactic execution took 1.52s
1.52 elaboration of bounded_bUnion took 1.52s
1.52 elaboration: tactic execution took 1.52s
1.52 elaboration: tactic execution took 1.52s
1.52 elaboration of left_le_sup took 1.52s
1.52 elaboration of lie_neg took 1.52s
1.52 elaboration: tactic execution took 1.52s
1.52 elaboration of linear_independent_monoid_hom took 1.52s
1.52 elaboration of neg_lie took 1.52s
1.52 elaboration of cauchy_seq_finset_iff_vanishing took 1.52s
1.52 elaboration: tactic execution took 1.52s
1.52 elaboration: tactic execution took 1.52s
1.52 elaboration: tactic execution took 1.52s
1.52 elaboration: tactic execution took 1.52s
1.52 elaboration of biproduct.ι_mono took 1.52s
1.52 elaboration: tactic execution took 1.52s
1.52 elaboration of Mon_iso_to_mul_equiv took 1.52s
1.51 elaboration: tactic execution took 1.51s
1.51 elaboration of exists_Ioc_subset_of_mem_nhds' took 1.51s
1.51 elaboration: tactic execution took 1.51s
1.51 decl post-processing of prod_singleton took 1.51s
1.51 elaboration of Sup_add took 1.51s
1.51 elaboration of det_transpose took 1.51s
1.51 elaboration: tactic execution took 1.51s
1.51 elaboration: tactic execution took 1.51s
1.51 elaboration: tactic execution took 1.51s
1.51 elaboration: tactic execution took 1.51s
1.51 elaboration of derivative_mul took 1.51s
1.51 elaboration: tactic execution took 1.51s
1.51 elaboration of zero_lie took 1.51s
1.51 elaboration: tactic execution took 1.51s
1.51 elaboration: tactic execution took 1.51s
1.51 elaboration: tactic execution took 1.51s
1.51 elaboration: tactic execution took 1.51s
1.51 elaboration: tactic execution took 1.51s
1.51 elaboration of prod_mk_prod took 1.51s
1.51 elaboration: tactic execution took 1.51s
1.51 elaboration of cofan.mk took 1.51s
1.51 elaboration: tactic execution took 1.51s
1.51 elaboration: tactic execution took 1.51s
1.51 elaboration of sum_sub_index took 1.51s
1.51 elaboration: tactic execution took 1.51s
1.51 elaboration: tactic execution took 1.51s
1.5 elaboration: tactic execution took 1.5s
1.5 elaboration of image.eq_to_hom took 1.5s
1.5 decl post-processing of mul_left_injective took 1.5s
1.5 elaboration of has_sum_mul_left_iff took 1.5s
1.5 elaboration of exists_irreducible_factor took 1.5s
1.5 elaboration of tendsto_to_nnreal took 1.5s
1.5 elaboration of has_neg took 1.5s
1.5 elaboration: tactic execution took 1.5s
1.5 elaboration: tactic execution took 1.5s
1.5 elaboration of add_eq_max_of_ne took 1.5s
1.5 elaboration of extend_function took 1.5s
1.5 elaboration: tactic execution took 1.5s
1.5 elaboration of of_fintype took 1.5s
1.5 elaboration: tactic execution took 1.5s
1.5 decl post-processing of cases_on took 1.5s
1.5 elaboration: tactic execution took 1.5s
1.5 elaboration: tactic execution took 1.5s
1.5 elaboration: tactic execution took 1.5s
1.5 elaboration: tactic execution took 1.5s
1.49 elaboration of mul_eq_left_iff took 1.49s
1.49 elaboration: tactic execution took 1.49s
1.49 elaboration: tactic execution took 1.49s
1.49 elaboration of mul_eq_mul_left took 1.49s
1.49 elaboration of rtendsto'_def took 1.49s
1.49 elaboration: tactic execution took 1.49s
1.49 elaboration: tactic execution took 1.49s
1.49 elaboration of cofree took 1.49s
1.49 elaboration of cseval_add took 1.49s
1.49 decl post-processing of prod_union_inter took 1.49s
1.49 elaboration of fan.mk took 1.49s
1.49 elaboration: tactic execution took 1.49s
1.49 elaboration of alternate took 1.49s
1.49 elaboration of summable.sigma_factor took 1.49s
1.49 elaboration: tactic execution took 1.49s
1.49 elaboration: tactic execution took 1.49s
1.49 elaboration: tactic execution took 1.49s
1.49 elaboration: tactic execution took 1.49s
1.49 elaboration: tactic execution took 1.49s
1.49 elaboration of add_comm_group took 1.49s
1.49 elaboration: tactic execution took 1.49s
1.49 elaboration: tactic execution took 1.49s
1.48 elaboration: tactic execution took 1.48s
1.48 decl post-processing of one_eq_mk took 1.48s
1.48 elaboration of lift took 1.48s
1.48 elaboration of nhds_zero took 1.48s
1.48 elaboration: tactic execution took 1.48s
1.48 elaboration: tactic execution took 1.48s
1.48 elaboration: tactic execution took 1.48s
1.48 elaboration of ker_pi took 1.48s
1.48 elaboration of exp_bound took 1.48s
1.48 elaboration: tactic execution took 1.48s
1.48 elaboration: tactic execution took 1.48s
1.48 elaboration: tactic execution took 1.48s
1.48 elaboration: tactic execution took 1.48s
1.48 elaboration: tactic execution took 1.48s
1.47 elaboration: tactic execution took 1.47s
1.47 elaboration of has_fderiv_at_filter.add took 1.47s
1.47 elaboration: tactic execution took 1.47s
1.47 elaboration: tactic execution took 1.47s
1.47 elaboration of const_comp took 1.47s
1.47 elaboration: tactic execution took 1.47s
1.47 elaboration: tactic execution took 1.47s
1.47 elaboration: tactic execution took 1.47s
1.47 elaboration: tactic execution took 1.47s
1.47 elaboration of NF_power took 1.47s
1.47 elaboration of bernoulli_four took 1.47s
1.47 elaboration: tactic execution took 1.47s
1.47 elaboration: tactic execution took 1.47s
1.47 elaboration of category_theory.faithful took 1.47s
1.47 elaboration: tactic execution took 1.47s
1.47 elaboration: tactic execution took 1.47s
1.47 elaboration: tactic execution took 1.47s
1.46 elaboration: tactic execution took 1.46s
1.46 elaboration: tactic execution took 1.46s
1.46 elaboration of disjoint_ker took 1.46s
1.46 elaboration: tactic execution took 1.46s
1.46 elaboration of free_group_unit_equiv_int took 1.46s
1.46 elaboration of comp took 1.46s
1.46 elaboration of rtendsto_iff_le_comap took 1.46s
1.46 elaboration: tactic execution took 1.46s
1.46 elaboration of normal_epi.regular_epi took 1.46s
1.46 elaboration: tactic execution took 1.46s
1.46 decl post-processing of id took 1.46s
1.46 elaboration of has_sum_single took 1.46s
1.46 elaboration of second_countable_of_almost_dense_set took 1.46s
1.45 elaboration: tactic execution took 1.45s
1.45 elaboration: tactic execution took 1.45s
1.45 elaboration of continuous_of_locally_uniform_approx_of_continuous took 1.45s
1.45 elaboration of hom_mk took 1.45s
1.45 elaboration of tsum_mul_left took 1.45s
1.45 elaboration: tactic execution took 1.45s
1.45 elaboration of eq_bot_or_top took 1.45s
1.45 elaboration of EilenbergMoore took 1.45s
1.45 elaboration of commute.add_pow took 1.45s
1.45 elaboration: tactic execution took 1.45s
1.45 elaboration of to_linear_map took 1.45s
1.45 elaboration: tactic execution took 1.45s
1.45 elaboration: tactic execution took 1.45s
1.45 elaboration: tactic execution took 1.45s
1.45 elaboration: tactic execution took 1.45s
1.45 elaboration of card_eq_sum_card_image took 1.45s
1.45 elaboration of precompose_comp took 1.45s
1.45 elaboration of of_int took 1.45s
1.45 elaboration of map_sub took 1.45s
1.45 elaboration of has_sum.sub took 1.45s
1.44 elaboration of prod_univ_units_id_eq_neg_one took 1.44s
1.44 elaboration: tactic execution took 1.44s
1.44 elaboration of coyoneda took 1.44s
1.44 elaboration: tactic execution took 1.44s
1.44 elaboration: tactic execution took 1.44s
1.44 elaboration of image_to_kernel_map_condition took 1.44s
1.44 elaboration: tactic execution took 1.44s
1.44 elaboration of calc_eval_z' took 1.44s
1.44 elaboration: tactic execution took 1.44s
1.44 elaboration of edist_le_tsum_of_edist_le_of_tendsto₀ took 1.44s
1.44 elaboration of map_comp took 1.44s
1.44 elaboration of mem_insert took 1.44s
1.44 elaboration of has_sum_coe took 1.44s
1.44 elaboration: tactic execution took 1.44s
1.44 elaboration: tactic execution took 1.44s
1.44 decl post-processing of exists_list_of_mem_closure took 1.44s
1.44 elaboration: tactic execution took 1.44s
1.44 elaboration of tsum_eq_tsum_of_has_sum_iff_has_sum took 1.44s
1.44 elaboration of prod_map_fst took 1.44s
1.44 elaboration: tactic execution took 1.44s
1.44 elaboration: tactic execution took 1.44s
1.44 elaboration of multilinear_map.uncurry_curry_left took 1.44s
1.43 elaboration of empty_ext took 1.43s
1.43 elaboration of disjoint_def took 1.43s
1.43 elaboration: tactic execution took 1.43s
1.43 elaboration: tactic execution took 1.43s
1.43 elaboration: tactic execution took 1.43s
1.43 elaboration of ext took 1.43s
1.43 elaboration of colimit_cocone took 1.43s
1.43 elaboration: tactic execution took 1.43s
1.43 elaboration of inf took 1.43s
1.43 elaboration of EilenbergMoore took 1.43s
1.43 elaboration of swap_induction_on took 1.43s
1.43 elaboration of sum_card_order_of_eq_card_pow_eq_one took 1.43s
1.43 elaboration of prime.mul_eq_prime_pow_two_iff took 1.43s
1.43 elaboration: tactic execution took 1.43s
1.43 elaboration: tactic execution took 1.43s
1.43 elaboration: tactic execution took 1.43s
1.42 elaboration of metric_space.to_emetric_space took 1.42s
1.42 elaboration: tactic execution took 1.42s
1.42 elaboration: tactic execution took 1.42s
1.42 elaboration: tactic execution took 1.42s
1.42 elaboration of tr_supports took 1.42s
1.42 elaboration of strong_epi_mono_factorisation.to_mono_is_image took 1.42s
1.42 elaboration of emetric_space.to_metric_space_of_dist took 1.42s
1.42 elaboration of cof_add took 1.42s
1.42 elaboration of mem_pi took 1.42s
1.42 elaboration of image.pre_comp_comp took 1.42s
1.42 elaboration: tactic execution took 1.42s
1.42 elaboration of has_image_map_id took 1.42s
1.42 elaboration of det_diagonal took 1.42s
1.42 elaboration: tactic execution took 1.42s
1.42 elaboration of second_countable_of_separable took 1.42s
1.41 elaboration of normalization_domain took 1.41s
1.41 elaboration: tactic execution took 1.41s
1.41 elaboration of triv_change took 1.41s
1.41 elaboration: tactic execution took 1.41s
1.41 elaboration: tactic execution took 1.41s
1.41 elaboration: tactic execution took 1.41s
1.41 elaboration of pointwise_mul took 1.41s
1.41 elaboration: tactic execution took 1.41s
1.41 elaboration of trunc_fun took 1.41s
1.41 elaboration of det_adjugate_of_is_unit took 1.41s
1.41 elaboration of model_with_corners.mdifferentiable_on_symm took 1.41s
1.41 elaboration of totally_bounded_iff_filter took 1.41s
1.41 elaboration: tactic execution took 1.41s
1.41 elaboration of multilinear_map.uncurry_curry_right took 1.41s
1.41 elaboration: tactic execution took 1.41s
1.41 decl post-processing of is_mul_hom took 1.41s
1.41 elaboration of sqrt_exists took 1.41s
1.4 elaboration: tactic execution took 1.4s
1.4 elaboration of comap_mul_action took 1.4s
1.4 decl post-processing of coprod_inl_inr took 1.4s
1.4 elaboration: tactic execution took 1.4s
1.4 elaboration of mk_span_singleton_apply took 1.4s
1.4 elaboration of map_range_def took 1.4s
1.4 elaboration of card_order_of_eq_totient_aux₂ took 1.4s
1.4 elaboration: tactic execution took 1.4s
1.4 elaboration of option_equiv_left took 1.4s
1.4 elaboration of split_mono_equalizes took 1.4s
1.4 elaboration: tactic execution took 1.4s
1.4 elaboration of tsum_mul_right took 1.4s
1.4 elaboration of pure_map took 1.4s
1.4 elaboration of evaln_prim took 1.4s
1.4 elaboration of monomial_mul_monomial took 1.4s
1.4 elaboration: tactic execution took 1.4s
1.4 elaboration of eq_top_of_unit_mem took 1.4s
1.4 elaboration of map_id took 1.4s
1.4 elaboration: tactic execution took 1.4s
1.4 elaboration of mk_pi_ring_apply_one_eq_self took 1.4s
1.39 elaboration of tendsto.const_div took 1.39s
1.39 elaboration: tactic execution took 1.39s
1.39 elaboration of finset.mem_enum took 1.39s
1.39 elaboration of id took 1.39s
1.39 elaboration of tan_eq_sin_div_cos took 1.39s
1.39 elaboration of regular_epi.of_split_epi took 1.39s
1.39 elaboration of rcomap'_rcomap' took 1.39s
1.39 elaboration: tactic execution took 1.39s
1.39 elaboration of mem_span_singleton took 1.39s
1.39 decl post-processing of prod_mem took 1.39s
1.39 elaboration of module took 1.39s
1.39 elaboration: tactic execution took 1.39s
1.39 elaboration: tactic execution took 1.39s
1.39 elaboration of regular_mono.of_split_mono took 1.39s
1.39 elaboration of sum_range_sub_sum_range took 1.39s
1.39 elaboration: tactic execution took 1.39s
1.38 elaboration: tactic execution took 1.38s
1.38 elaboration: tactic execution took 1.38s
1.38 elaboration: tactic execution took 1.38s
1.38 elaboration: tactic execution took 1.38s
1.38 elaboration of map_eq_comap took 1.38s
1.38 elaboration of comap took 1.38s
1.38 elaboration of functor_to_core took 1.38s
1.38 elaboration of lt_power_cof took 1.38s
1.38 elaboration: tactic execution took 1.38s
1.38 elaboration of exists_finset_roots took 1.38s
1.38 decl post-processing of prod_map_mul took 1.38s
1.38 elaboration: tactic execution took 1.38s
1.38 elaboration: tactic execution took 1.38s
1.38 elaboration: tactic execution took 1.38s
1.38 elaboration of rcomap_rcomap took 1.38s
1.38 elaboration of integral_eq_lintegral_max_sub_lintegral_min took 1.38s
1.38 elaboration of le_nhds_iff took 1.38s
1.38 elaboration of tendsto_coe_nnreal_nhds_top took 1.38s
1.38 elaboration of prod_map_range_index took 1.38s
1.38 elaboration: tactic execution took 1.38s
1.38 elaboration of liftq took 1.38s
1.38 elaboration: tactic execution took 1.38s
1.38 elaboration: tactic execution took 1.38s
1.37 elaboration of tendsto.div took 1.37s
1.37 elaboration of rat.continuous_mul took 1.37s
1.37 elaboration of cof_cof took 1.37s
1.37 elaboration of nonneg_mul took 1.37s
1.37 elaboration of prod_finset_sum_index took 1.37s
1.37 elaboration of hom took 1.37s
1.37 elaboration of linear_order took 1.37s
1.37 elaboration: tactic execution took 1.37s
1.37 elaboration of exists_clause_holds_core took 1.37s
1.37 elaboration of of_nat_surjective_aux took 1.37s
1.37 elaboration: tactic execution took 1.37s
1.37 elaboration of continuous_on_iff' took 1.37s
1.37 elaboration: tactic execution took 1.37s
1.37 elaboration of postcompose_comp took 1.37s
1.37 elaboration of sub_single_one_add took 1.37s
1.37 elaboration: tactic execution took 1.37s
1.37 elaboration: tactic execution took 1.37s
1.37 elaboration of indicator_finset_bUnion took 1.37s
1.37 elaboration of count_bind took 1.37s
1.37 elaboration of continuous_at_rpow_of_ne_zero took 1.37s
1.37 elaboration of rat.totally_bounded_Icc took 1.37s
1.37 elaboration of f_aux_limit took 1.37s
1.36 elaboration: tactic execution took 1.36s
1.36 elaboration of decidable_eq took 1.36s
1.36 elaboration of add_supr took 1.36s
1.36 elaboration: tactic execution took 1.36s
1.36 elaboration of map_inr took 1.36s
1.36 elaboration of cof_sup_le_lift took 1.36s
1.36 elaboration: tactic execution took 1.36s
1.36 elaboration: tactic execution took 1.36s
1.36 elaboration of sup_range_inl_inr took 1.36s
1.36 elaboration of continuous_at_of_locally_lipschitz took 1.36s
1.36 elaboration of pullback.fst_of_mono took 1.36s
1.36 decl post-processing of coe_inj took 1.36s
1.36 elaboration: tactic execution took 1.36s
1.36 elaboration: tactic execution took 1.36s
1.36 elaboration of of_subtype_subtype_perm took 1.36s
1.36 elaboration of lift'.is_ring_hom took 1.36s
1.36 elaboration of cons_vec_mul_vec took 1.36s
1.36 elaboration of rat.uniform_continuous_abs took 1.36s
1.35 elaboration of composition_as_set.to_composition_boundaries took 1.35s
1.35 elaboration: tactic execution took 1.35s
1.35 elaboration: tactic execution took 1.35s
1.35 elaboration of normal_mono.regular_mono took 1.35s
1.35 elaboration: tactic execution took 1.35s
1.35 elaboration: tactic execution took 1.35s
1.35 elaboration of split_mono_sigma_ι took 1.35s
1.35 elaboration of finite_subset_Union took 1.35s
1.35 decl post-processing of prod_comp_prod_map took 1.35s
1.35 elaboration of nat_iso took 1.35s
1.35 elaboration: tactic execution took 1.35s
1.35 elaboration: tactic execution took 1.35s
1.35 elaboration of map_piecewise_add took 1.35s
1.35 elaboration: tactic execution took 1.35s
1.35 elaboration of comap_distrib_mul_action took 1.35s
1.35 elaboration of has_zero took 1.35s
1.35 elaboration of pushout.inr_of_epi took 1.35s
1.35 elaboration: tactic execution took 1.35s
1.35 elaboration of bind_decode_iff took 1.35s
1.35 elaboration: tactic execution took 1.35s
1.35 elaboration of prod_comap_inl took 1.35s
1.35 elaboration: tactic execution took 1.35s
1.35 elaboration: tactic execution took 1.35s
1.34 elaboration of snd.is_semiring_hom took 1.34s
1.34 elaboration: tactic execution took 1.34s
1.34 elaboration of prod_map_snd took 1.34s
1.34 elaboration of change_origin_summable_aux2 took 1.34s
1.34 elaboration: tactic execution took 1.34s
1.34 elaboration: tactic execution took 1.34s
1.34 elaboration of id_groupoid took 1.34s
1.34 elaboration: tactic execution took 1.34s
1.34 elaboration: tactic execution took 1.34s
1.34 elaboration: tactic execution took 1.34s
1.34 elaboration of prod_comap_inr took 1.34s
1.34 elaboration of neg_cons took 1.34s
1.34 elaboration of of_equiv took 1.34s
1.34 elaboration: tactic execution took 1.34s
1.34 elaboration of terminal.from took 1.34s
1.34 elaboration: tactic execution took 1.34s
1.34 elaboration: tactic execution took 1.34s
1.34 elaboration of list_prod took 1.34s
1.34 elaboration: tactic execution took 1.34s
1.34 elaboration: tactic execution took 1.34s
1.34 elaboration: tactic execution took 1.34s
1.34 elaboration of dvd took 1.34s
1.33 elaboration: tactic execution took 1.33s
1.33 elaboration of lintegral_le_lintegral_ae took 1.33s
1.33 elaboration of tendsto.const_mul took 1.33s
1.33 elaboration: tactic execution took 1.33s
1.33 elaboration of comap_snd took 1.33s
1.33 elaboration: tactic execution took 1.33s
1.33 elaboration: tactic execution took 1.33s
1.33 elaboration of eq_infi_principal took 1.33s
1.33 elaboration: tactic execution took 1.33s
1.33 elaboration of pushout.inl_of_epi took 1.33s
1.33 elaboration of is_colimit.mk took 1.33s
1.33 elaboration of forget_faithful took 1.33s
1.33 decl post-processing of has_inv took 1.33s
1.33 elaboration of add_cons took 1.33s
1.33 elaboration: tactic execution took 1.33s
1.33 elaboration of prod_apply_ite took 1.33s
1.33 elaboration: tactic execution took 1.33s
1.33 elaboration: tactic execution took 1.33s
1.33 elaboration of is_limit.mk took 1.33s
1.33 elaboration: tactic execution took 1.33s
1.33 elaboration of exp_zero took 1.33s
1.33 decl post-processing of inv_mul_eq_one took 1.33s
1.33 elaboration of uniform_embedding_def' took 1.33s
1.32 elaboration: tactic execution took 1.32s
1.32 elaboration of local_triv'_trans took 1.32s
1.32 elaboration: tactic execution took 1.32s
1.32 elaboration of proj_std_basis_same took 1.32s
1.32 elaboration: tactic execution took 1.32s
1.32 elaboration: tactic execution took 1.32s
1.32 elaboration of geometric_bound_of_lt_radius took 1.32s
1.32 elaboration: tactic execution took 1.32s
1.32 elaboration of cone_iso_of_hom_iso took 1.32s
1.32 elaboration of exp_add took 1.32s
1.32 elaboration: tactic execution took 1.32s
1.32 elaboration of tendsto_uniformly_iff took 1.32s
1.32 elaboration: tactic execution took 1.32s
1.32 elaboration of support_subset_iff took 1.32s
1.32 elaboration: tactic execution took 1.32s
1.32 elaboration: tactic execution took 1.32s
1.32 elaboration of induction₂ took 1.32s
1.32 elaboration of comap_map_eq took 1.32s
1.32 elaboration of has_fderiv_at.of_local_left_inverse took 1.32s
1.32 elaboration of le_comp_radius_of_summable took 1.32s
1.32 elaboration of image_closure_subset_closure_image took 1.32s
1.32 elaboration of full_of_equivalence took 1.32s
1.32 decl post-processing of left_inv_eq_right_inv took 1.32s
1.32 elaboration of tendsto.div_const took 1.32s
1.32 elaboration: tactic execution took 1.32s
1.32 elaboration: tactic execution took 1.32s
1.32 elaboration of to_matrix_trans took 1.32s
1.31 elaboration: tactic execution took 1.31s
1.31 elaboration: tactic execution took 1.31s
1.31 elaboration of cocone_iso_of_hom_iso took 1.31s
1.31 decl post-processing of coprod_apply took 1.31s
1.31 elaboration of pullback.snd_of_mono took 1.31s
1.31 elaboration of biprod.fst_epi took 1.31s
1.31 decl post-processing of eq_cosets_of_normal took 1.31s
1.31 elaboration: tactic execution took 1.31s
1.31 elaboration: tactic execution took 1.31s
1.31 elaboration of comap_fst took 1.31s
1.31 elaboration: tactic execution took 1.31s
1.31 elaboration of lid_tmul took 1.31s
1.31 elaboration: tactic execution took 1.31s
1.31 elaboration of locally_compact_of_proper took 1.31s
1.31 elaboration of comap_mkq.order_iso took 1.31s
1.31 elaboration of ball_pi took 1.31s
1.31 elaboration: tactic execution took 1.31s
1.31 elaboration: tactic execution took 1.31s
1.31 elaboration: tactic execution took 1.31s
1.31 elaboration: tactic execution took 1.31s
1.31 elaboration: tactic execution took 1.31s
1.31 elaboration of nhds_eq took 1.31s
1.31 elaboration of times_cont_diff_on.comp_same_univ took 1.31s
1.31 elaboration of disjoint_disjointed took 1.31s
1.3 elaboration: tactic execution took 1.3s
1.3 elaboration of mul_le_of_limit_aux took 1.3s
1.3 elaboration of local_triv took 1.3s
1.3 elaboration of cod_restrict took 1.3s
1.3 decl post-processing of map_mclosure took 1.3s
1.3 elaboration of cof_bsup_le took 1.3s
1.3 elaboration: tactic execution took 1.3s
1.3 elaboration: tactic execution took 1.3s
1.3 elaboration of sign_cycle took 1.3s
1.3 elaboration of topological_ring took 1.3s
1.3 elaboration of biprod.inl_mono took 1.3s
1.3 elaboration of biprod.snd_epi took 1.3s
1.3 elaboration: tactic execution took 1.3s
1.3 decl post-processing of has_mul took 1.3s
1.3 elaboration of local_triv' took 1.3s
1.3 elaboration of mul_matrix_apply took 1.3s
1.3 elaboration: tactic execution took 1.3s
1.3 elaboration of extend took 1.3s
1.29 elaboration: tactic execution took 1.29s
1.29 elaboration of sub_NF_below took 1.29s
1.29 elaboration of nhds_pointwise_mul took 1.29s
1.29 elaboration of ne_ones_iff took 1.29s
1.29 elaboration: tactic execution took 1.29s
1.29 parsing took 1.29s
1.29 elaboration of bundle_trivialization.continuous_at_proj took 1.29s
1.29 elaboration: tactic execution took 1.29s
1.29 elaboration: tactic execution took 1.29s
1.29 elaboration of image.factor_map took 1.29s
1.29 elaboration of cramer_map_is_linear took 1.29s
1.29 elaboration: tactic execution took 1.29s
1.29 elaboration: tactic execution took 1.29s
1.29 decl post-processing of coprod took 1.29s
1.29 elaboration: tactic execution took 1.29s
1.29 elaboration: tactic execution took 1.29s
1.29 elaboration of det_eq_one_of_card_eq_zero took 1.29s
1.29 elaboration: tactic execution took 1.29s
1.29 elaboration of le_div_two_iff_lt_neg took 1.29s
1.29 elaboration of mk_prod_prf took 1.29s
1.29 elaboration: tactic execution took 1.29s
1.29 elaboration of continuous_at_of_locally_uniform_approx_of_continuous_at took 1.29s
1.29 elaboration: tactic execution took 1.29s
1.29 elaboration of sign_aux3_mul_and_swap took 1.29s
1.29 elaboration of neg_Z took 1.29s
1.29 elaboration of map_subtype.order_iso took 1.29s
1.29 elaboration of nhds_order_unbounded took 1.29s
1.28 elaboration of has_scalar took 1.28s
1.28 elaboration of id took 1.28s
1.28 elaboration of inj_of_trivial_ker took 1.28s
1.28 elaboration of bilin_form_equiv_matrix took 1.28s
1.28 elaboration: tactic execution took 1.28s
1.28 elaboration of lift_cof took 1.28s
1.28 elaboration of continuants_aux_eq_continuants_aux_squash_gcf_of_le took 1.28s
1.28 elaboration: tactic execution took 1.28s
1.28 decl post-processing of comp took 1.28s
1.28 elaboration of union_subset_iff took 1.28s
1.28 elaboration of cons_add took 1.28s
1.28 elaboration of has_dist_metric_quot took 1.28s
1.28 elaboration of algebra_map took 1.28s
1.28 elaboration of le_iff_neg_ge took 1.28s
1.28 elaboration: tactic execution took 1.28s
1.28 elaboration of prod_bot took 1.28s
1.28 elaboration of mul_vec_cons took 1.28s
1.28 elaboration: tactic execution took 1.28s
1.28 elaboration of map_coord_zero took 1.28s
1.28 decl post-processing of monoid_to_is_right_id took 1.28s
1.28 elaboration of image_mono_iso_source_inv_ι took 1.28s
1.28 elaboration of abv_pos_of_not_lim_zero took 1.28s
1.28 elaboration of tendsto_order took 1.28s
1.28 elaboration of smul_right took 1.28s
1.28 elaboration: tactic execution took 1.28s
1.28 elaboration of comap_smul_single took 1.28s
1.28 elaboration of has_add took 1.28s
1.28 elaboration of metric_space took 1.28s
1.28 elaboration of mul_le_edist took 1.28s
1.28 elaboration of initial.to took 1.28s
1.28 elaboration of has_image.uniq took 1.28s
1.27 elaboration of vec_mul_vec_cons took 1.27s
1.27 elaboration of bernoulli_three took 1.27s
1.27 elaboration of is_linear_map_add took 1.27s
1.27 elaboration of closure_Iio' took 1.27s
1.27 elaboration of map_cod_restrict took 1.27s
1.27 elaboration of split_epi_coequalizes took 1.27s
1.27 decl post-processing of inv_mul_cancel_left took 1.27s
1.27 elaboration of local_of_nonunits_ideal took 1.27s
1.27 decl post-processing of map_exists_right_inv took 1.27s
1.27 elaboration of prod_add_index took 1.27s
1.27 elaboration of ext took 1.27s
1.27 elaboration of equiv_lt took 1.27s
1.27 elaboration: tactic execution took 1.27s
1.27 elaboration of to_matrix_injective took 1.27s
1.27 elaboration: tactic execution took 1.27s
1.27 elaboration: tactic execution took 1.27s
1.27 elaboration: tactic execution took 1.27s
1.27 elaboration: tactic execution took 1.27s
1.27 elaboration: tactic execution took 1.27s
1.27 elaboration of has_ftaylor_series_up_to_on.prod took 1.27s
1.27 elaboration: tactic execution took 1.27s
1.27 elaboration: tactic execution took 1.27s
1.26 elaboration: tactic execution took 1.26s
1.26 elaboration: tactic execution took 1.26s
1.26 elaboration: tactic execution took 1.26s
1.26 elaboration of has_sum.add took 1.26s
1.26 elaboration of adjugate_zero took 1.26s
1.26 elaboration of support_swap_mul_eq took 1.26s
1.26 elaboration: tactic execution took 1.26s
1.26 elaboration of quotient_rel took 1.26s
1.26 decl post-processing of snd_comp_prod took 1.26s
1.26 elaboration of monomial took 1.26s
1.26 elaboration of pi_field_equiv_aux took 1.26s
1.26 elaboration of with_density took 1.26s
1.26 elaboration of traverse took 1.26s
1.26 elaboration of whiskering_left took 1.26s
1.26 elaboration: tactic execution took 1.26s
1.26 elaboration of Sup_aux took 1.26s
1.26 elaboration of uniform_inducing.mk' took 1.26s
1.26 elaboration: tactic execution took 1.26s
1.26 elaboration of sign_bij took 1.26s
1.26 elaboration of polynomial.is_noetherian_ring took 1.26s
1.26 elaboration: tactic execution took 1.26s
1.26 elaboration: tactic execution took 1.26s
1.26 elaboration: tactic execution took 1.26s
1.25 elaboration of eq_mk_support took 1.25s
1.25 elaboration of of_equiv took 1.25s
1.25 elaboration of prod_single_index took 1.25s
1.25 elaboration of infi_coe took 1.25s
1.25 elaboration of support_swap took 1.25s
1.25 elaboration: tactic execution took 1.25s
1.25 elaboration of to_linear_equiv took 1.25s
1.25 elaboration of zero_linear_action took 1.25s
1.25 elaboration: tactic execution took 1.25s
1.25 elaboration of val_min_abs_eq_zero took 1.25s
1.25 elaboration of map_prod took 1.25s
1.25 elaboration of nonneg_add took 1.25s
1.25 elaboration: tactic execution took 1.25s
1.25 elaboration of span_singleton_prime took 1.25s
1.25 elaboration: tactic execution took 1.25s
1.25 elaboration: tactic execution took 1.25s
1.25 elaboration: tactic execution took 1.25s
1.25 elaboration: tactic execution took 1.25s
1.25 elaboration of antilipschitz_with.mul_le_dist took 1.25s
1.25 elaboration of cons_transpose took 1.25s
1.25 elaboration: tactic execution took 1.25s
1.25 elaboration: tactic execution took 1.25s
1.25 elaboration of repr_power_aux₁ took 1.25s
1.25 elaboration of map.is_ring_hom took 1.25s
1.25 decl post-processing of trivial_normal took 1.25s
1.25 elaboration: tactic execution took 1.25s
1.25 elaboration: tactic execution took 1.25s
1.25 elaboration of exists_nhds_split_inv took 1.25s
1.24 elaboration: tactic execution took 1.24s
1.24 elaboration: tactic execution took 1.24s
1.24 elaboration: tactic execution took 1.24s
1.24 elaboration of nonarchimedean_aux took 1.24s
1.24 elaboration of cseval_add_const took 1.24s
1.24 elaboration: tactic execution took 1.24s
1.24 elaboration of nhds_eq_comap_uniformity took 1.24s
1.24 elaboration of linear_action_zero took 1.24s
1.24 elaboration of comap took 1.24s
1.24 parsing took 1.24s
1.24 elaboration: tactic execution took 1.24s
1.24 decl post-processing of val_coe took 1.24s
1.24 elaboration: tactic execution took 1.24s
1.24 elaboration: tactic execution took 1.24s
1.24 elaboration: tactic execution took 1.24s
1.24 elaboration: tactic execution took 1.24s
1.24 elaboration: tactic execution took 1.24s
1.24 elaboration of real.uniform_continuous_neg took 1.24s
1.24 elaboration: tactic execution took 1.24s
1.24 elaboration of gauss_lemma took 1.24s
1.24 elaboration of col_cons took 1.24s
1.24 elaboration of inv_pow took 1.24s
1.24 elaboration: tactic execution took 1.24s
1.24 elaboration of is_image.fac_lift took 1.24s
1.23 elaboration: tactic execution took 1.23s
1.23 elaboration: tactic execution took 1.23s
1.23 elaboration: tactic execution took 1.23s
1.23 elaboration of is_coprime_def took 1.23s
1.23 elaboration of normalizer_is_subgroup took 1.23s
1.23 elaboration of vec_mul_cons took 1.23s
1.23 elaboration of cprank_max_sum took 1.23s
1.23 parsing took 1.23s
1.23 elaboration of cons_mul took 1.23s
1.23 elaboration of normalization_domain took 1.23s
1.23 elaboration: tactic execution took 1.23s
1.23 elaboration of sum_range_sub_of_monotone took 1.23s
1.23 elaboration of add_Z took 1.23s
1.23 elaboration: tactic execution took 1.23s
1.23 elaboration of strong_epi_mono_factorisation_inhabited took 1.23s
1.23 elaboration: tactic execution took 1.23s
1.23 elaboration: tactic execution took 1.23s
1.23 elaboration of transpose_nonsing_inv took 1.23s
1.23 elaboration: tactic execution took 1.23s
1.23 elaboration of has_ftaylor_series_up_to_on.comp_continuous_linear_map took 1.23s
1.23 elaboration of prod_top took 1.23s
1.23 elaboration: tactic execution took 1.23s
1.23 elaboration of bundled_hom took 1.23s
1.23 elaboration of sum_unit_vec_mul_slice took 1.23s
1.23 elaboration: tactic execution took 1.23s
1.23 elaboration of id_c_app took 1.23s
1.22 elaboration of strong_epi_comp took 1.22s
1.22 elaboration: tactic execution took 1.22s
1.22 elaboration of mk' took 1.22s
1.22 elaboration: tactic execution took 1.22s
1.22 elaboration: tactic execution took 1.22s
1.22 elaboration: tactic execution took 1.22s
1.22 decl post-processing of ne_one_iff_exists took 1.22s
1.22 elaboration of cocone_of_split_epi took 1.22s
1.22 elaboration: tactic execution took 1.22s
1.22 elaboration: tactic execution took 1.22s
1.22 elaboration: tactic execution took 1.22s
1.22 elaboration of indicator_union_of_not_mem_inter took 1.22s
1.22 elaboration of totally_bounded_preimage took 1.22s
1.22 elaboration of cof_succ took 1.22s
1.22 elaboration: tactic execution took 1.22s
1.22 elaboration: tactic execution took 1.22s
1.22 elaboration of open_source' took 1.22s
1.22 elaboration: tactic execution took 1.22s
1.22 elaboration: tactic execution took 1.22s
1.22 elaboration of det_smul took 1.22s
1.22 elaboration of multiplicity_eq_card_pow_dvd took 1.22s
1.22 elaboration of nhds_translation_mul_inv took 1.22s
1.21 elaboration of continuous_within_at_iff_continuous_within_at_comp_right took 1.21s
1.21 elaboration of has_bot took 1.21s
1.21 elaboration: tactic execution took 1.21s
1.21 elaboration: tactic execution took 1.21s
1.21 elaboration of exists_nhds_split took 1.21s
1.21 elaboration of finset_prod_mem took 1.21s
1.21 elaboration of det_adjugate_eq_one took 1.21s
1.21 elaboration of has_top took 1.21s
1.21 elaboration: tactic execution took 1.21s
1.21 elaboration: tactic execution took 1.21s
1.21 decl post-processing of one_apply took 1.21s
1.21 elaboration of stmts₁_trans took 1.21s
1.21 elaboration of closure.is_subfield took 1.21s
1.21 elaboration: tactic execution took 1.21s
1.21 elaboration of has_add took 1.21s
1.21 elaboration of complete_lattice took 1.21s
1.21 elaboration of image_subgroup took 1.21s
1.21 elaboration: tactic execution took 1.21s
1.21 elaboration: tactic execution took 1.21s
1.21 elaboration of is_local_ring took 1.21s
1.21 elaboration of division_ring took 1.21s
1.21 elaboration of tr_stmts₁ took 1.21s
1.21 elaboration: tactic execution took 1.21s
1.21 elaboration: tactic execution took 1.21s
1.21 decl post-processing of mrange took 1.21s
1.21 decl post-processing of map_mul took 1.21s
1.21 elaboration of equiv_fun_basis_symm_apply took 1.21s
1.2 elaboration of exists_left_inverse_linear_map_of_injective took 1.2s
1.2 elaboration of to_group.unique took 1.2s
1.2 elaboration of topological_add_group_is_uniform took 1.2s
1.2 decl post-processing of map_ne_one_iff took 1.2s
1.2 elaboration of strong_epi_of_strong_epi took 1.2s
1.2 elaboration of cons_vec_mul took 1.2s
1.2 elaboration of preimage_mk_equiv_subgroup_times_set took 1.2s
1.2 parsing took 1.2s
1.2 elaboration: tactic execution took 1.2s
1.2 elaboration of tendsto_sub_comap_self took 1.2s
1.2 elaboration of cluster_point_of_compact took 1.2s
1.2 elaboration: tactic execution took 1.2s
1.2 elaboration: tactic execution took 1.2s
1.2 elaboration: tactic execution took 1.2s
1.2 elaboration: tactic execution took 1.2s
1.2 elaboration of dist_le_Ico_sum_dist took 1.2s
1.2 elaboration of set.image took 1.2s
1.2 elaboration of monoid_hom.range_factorization took 1.2s
1.2 elaboration: tactic execution took 1.2s
1.2 elaboration of abs_exp_sub_one_sub_id_le took 1.2s
1.2 elaboration: tactic execution took 1.2s
1.2 elaboration of equivalence_preserves_zero_morphisms took 1.2s
1.2 elaboration of sum_single took 1.2s
1.2 elaboration of dvd_or_coprime took 1.2s
1.2 elaboration: tactic execution took 1.2s
1.2 elaboration of sum_ring_equiv took 1.2s
1.2 elaboration of diam_eq_zero_of_unbounded took 1.2s
1.2 elaboration: tactic execution took 1.2s
1.2 elaboration of list took 1.2s
1.2 elaboration: tactic execution took 1.2s
1.2 elaboration: tactic execution took 1.2s
1.2 elaboration of eq_of_cmp_eq took 1.2s
1.2 elaboration of monoid took 1.2s
1.2 elaboration: tactic execution took 1.2s
1.2 elaboration: tactic execution took 1.2s
1.2 elaboration of ppred took 1.2s
1.2 elaboration of is_cyclic took 1.2s
1.2 elaboration of is_linear_map_sub took 1.2s
1.2 elaboration: tactic execution took 1.2s
1.2 elaboration of disjoint.symm took 1.2s
1.2 elaboration: tactic execution took 1.2s
1.2 elaboration of commute.geom_sum₂_mul_add took 1.2s
1.19 elaboration of cons_mul_vec took 1.19s
1.19 elaboration: tactic execution took 1.19s
1.19 elaboration of sup_h_of_disjoint took 1.19s
1.19 elaboration: tactic execution took 1.19s
1.19 elaboration of is_open_iff took 1.19s
1.19 elaboration of mem_span_insert' took 1.19s
1.19 elaboration of as_hom_injective took 1.19s
1.19 elaboration of comp took 1.19s
1.19 elaboration of sin_pos_of_pos_of_le_one took 1.19s
1.19 elaboration of preimage took 1.19s
1.19 elaboration of of_function took 1.19s
1.19 decl post-processing of mul_eq_one_iff_inv_eq took 1.19s
1.19 elaboration of inr took 1.19s
1.19 elaboration of map_id_obj_unop took 1.19s
1.19 elaboration: tactic execution took 1.19s
1.19 decl post-processing of inv_ne_one took 1.19s
1.19 decl post-processing of fst_comp_prod took 1.19s
1.19 elaboration: tactic execution took 1.19s
1.19 elaboration: tactic execution took 1.19s
1.19 elaboration: tactic execution took 1.19s
1.19 elaboration of uniformity_translate took 1.19s
1.19 elaboration of mem_pos_tangent_cone_at_of_segment_subset took 1.19s
1.19 elaboration of comap_smul' took 1.19s
1.19 elaboration: tactic execution took 1.19s
1.19 decl post-processing of one_iff_ker_inv took 1.19s
1.19 elaboration of self took 1.19s
1.19 elaboration of ker_mkq took 1.19s
1.19 elaboration of compact.elim_finite_subcover took 1.19s
1.19 elaboration of of_isos took 1.19s
1.19 elaboration: tactic execution took 1.19s
1.18 elaboration of monad took 1.18s
1.18 elaboration of cof_univ took 1.18s
1.18 decl post-processing of center_normal took 1.18s
1.18 elaboration of vector_space took 1.18s
1.18 elaboration: tactic execution took 1.18s
1.18 elaboration: tactic execution took 1.18s
1.18 elaboration of oadd_mul_NF_below took 1.18s
1.18 elaboration of map_parallel took 1.18s
1.18 elaboration: tactic execution took 1.18s
1.18 elaboration of assoc took 1.18s
1.18 elaboration of support_single_ne_zero took 1.18s
1.18 elaboration: tactic execution took 1.18s
1.18 elaboration of of_real_mul took 1.18s
1.18 elaboration: tactic execution took 1.18s
1.18 elaboration: tactic execution took 1.18s
1.18 elaboration: tactic execution took 1.18s
1.18 elaboration of ext took 1.18s
1.18 elaboration: tactic execution took 1.18s
1.18 elaboration: tactic execution took 1.18s
1.18 elaboration of prod.normed_space took 1.18s
1.18 elaboration: tactic execution took 1.18s
1.18 elaboration: tactic execution took 1.18s
1.18 elaboration: tactic execution took 1.18s
1.18 elaboration: tactic execution took 1.18s
1.18 elaboration of pointwise_mul_union took 1.18s
1.18 decl post-processing of map_eq_one_iff took 1.18s
1.18 elaboration of prod.map_fst took 1.18s
1.18 elaboration: tactic execution took 1.18s
1.18 elaboration of neg took 1.18s
1.18 elaboration: tactic execution took 1.18s
1.18 elaboration of uniform_space.has_bot took 1.18s
1.18 elaboration: tactic execution took 1.18s
1.17 elaboration: tactic execution took 1.17s
1.17 elaboration of frequently_principal took 1.17s
1.17 elaboration: tactic execution took 1.17s
1.17 elaboration: tactic execution took 1.17s
1.17 elaboration of eq_of_local_equiv_eq took 1.17s
1.17 decl post-processing of ker_lift_mk took 1.17s
1.17 elaboration of lie_ring took 1.17s
1.17 elaboration of cons_head_tail took 1.17s
1.17 elaboration of det_one took 1.17s
1.17 elaboration of mapq took 1.17s
1.17 elaboration of dot_product_cons took 1.17s
1.17 elaboration: tactic execution took 1.17s
1.17 elaboration: tactic execution took 1.17s
1.17 elaboration: tactic execution took 1.17s
1.17 elaboration of union_pointwise_mul took 1.17s
1.17 elaboration of valid.replace_aux took 1.17s
1.17 elaboration of dist_nonneg took 1.17s
1.17 elaboration: tactic execution took 1.17s
1.17 elaboration: tactic execution took 1.17s
1.17 elaboration of uniform_continuous_dist' took 1.17s
1.17 elaboration of semimodule took 1.17s
1.17 elaboration: tactic execution took 1.17s
1.17 elaboration of has_fderiv_within_at.lim took 1.17s
1.17 decl post-processing of coe_ssubset_coe took 1.17s
1.17 elaboration: tactic execution took 1.17s
1.17 decl post-processing of mem_norm_comm_iff took 1.17s
1.17 elaboration of coprod.inr_map took 1.17s
1.17 elaboration: tactic execution took 1.17s
1.17 elaboration: tactic execution took 1.17s
1.16 elaboration of real.metric_space took 1.16s
1.16 elaboration of has_neg took 1.16s
1.16 elaboration of frequently_Sup took 1.16s
1.16 elaboration of pi_generate_from_eq took 1.16s
1.16 elaboration of has_sum.sigma_of_has_sum took 1.16s
1.16 elaboration of smul_cons took 1.16s
1.16 elaboration of eq_bot_of_zero_eq_one took 1.16s
1.16 elaboration of eq_top_iff_one took 1.16s
1.16 elaboration: tactic execution took 1.16s
1.16 elaboration: tactic execution took 1.16s
1.16 elaboration of cseval_mul took 1.16s
1.16 elaboration: tactic execution took 1.16s
1.16 elaboration of mul_vec.is_add_monoid_hom_left took 1.16s
1.16 elaboration of finite.induction_on took 1.16s
1.16 elaboration of hom_equiv took 1.16s
1.16 elaboration of self took 1.16s
1.16 decl post-processing of gi took 1.16s
1.16 elaboration: tactic execution took 1.16s
1.16 elaboration: tactic execution took 1.16s
1.16 elaboration: tactic execution took 1.16s
1.16 elaboration: tactic execution took 1.16s
1.16 elaboration: tactic execution took 1.16s
1.16 elaboration of sum_comap_domain took 1.16s
1.16 elaboration of second_countable_of_proper took 1.16s
1.16 elaboration of inverse took 1.16s
1.15 elaboration: tactic execution took 1.15s
1.15 elaboration: tactic execution took 1.15s
1.15 elaboration of cone_of_split_mono took 1.15s
1.15 elaboration: tactic execution took 1.15s
1.15 elaboration of split_mono_coprod_inr took 1.15s
1.15 elaboration of measurable_to_encodable took 1.15s
1.15 elaboration of prod_at_top_at_top_eq took 1.15s
1.15 elaboration: tactic execution took 1.15s
1.15 elaboration of inr_eq_inl took 1.15s
1.15 elaboration: tactic execution took 1.15s
1.15 elaboration: tactic execution took 1.15s
1.15 elaboration of prod_pos took 1.15s
1.15 elaboration: tactic execution took 1.15s
1.15 elaboration: tactic execution took 1.15s
1.15 elaboration of prod_nonneg took 1.15s
1.15 elaboration: tactic execution took 1.15s
1.15 elaboration: tactic execution took 1.15s
1.15 elaboration of preimage_interior took 1.15s
1.15 elaboration: tactic execution took 1.15s
1.15 elaboration: tactic execution took 1.15s
1.15 elaboration of tsum_eq_zero_of_not_summable took 1.15s
1.15 elaboration of is_complete_image_iff took 1.15s
1.15 elaboration of series_ratio_test took 1.15s
1.15 elaboration of uniform_continuous_neg took 1.15s
1.15 elaboration of cons_dot_product took 1.15s
1.15 elaboration: tactic execution took 1.15s
1.15 elaboration: tactic execution took 1.15s
1.15 elaboration: tactic execution took 1.15s
1.15 elaboration of Sup_le took 1.15s
1.15 elaboration of add_one_le_exp_of_nonneg took 1.15s
1.15 parsing took 1.15s
1.14 elaboration of lim_eq_lim_im_add_lim_re took 1.14s
1.14 elaboration of restr_source_inter took 1.14s
1.14 decl post-processing of coe_map took 1.14s
1.14 elaboration: tactic execution took 1.14s
1.14 elaboration: tactic execution took 1.14s
1.14 elaboration of cons_eq_zero_iff took 1.14s
1.14 elaboration: tactic execution took 1.14s
1.14 elaboration of split_epi_prod_fst took 1.14s
1.14 elaboration: tactic execution took 1.14s
1.14 elaboration of cof took 1.14s
1.14 elaboration of uniform_space_eq took 1.14s
1.14 elaboration of id_rel_subset took 1.14s
1.14 elaboration: tactic execution took 1.14s
1.14 elaboration of add_sub_self took 1.14s
1.14 elaboration of simple_func_sequence_tendsto' took 1.14s
1.14 elaboration of summable.has_sum took 1.14s
1.14 elaboration of has_ftaylor_series_up_to_on.continuous_linear_map_comp took 1.14s
1.14 elaboration of group took 1.14s
1.14 elaboration of mem_fixed_points_mul_left_cosets_iff_mem_normalizer took 1.14s
1.14 elaboration: tactic execution took 1.14s
1.14 elaboration of left_rel took 1.14s
1.14 elaboration of inf_assoc took 1.14s
1.14 elaboration of list_foldl' took 1.14s
1.14 elaboration: tactic execution took 1.14s
1.14 elaboration: tactic execution took 1.14s
1.14 elaboration: tactic execution took 1.14s
1.14 elaboration of inl took 1.14s
1.14 elaboration of has_neg took 1.14s
1.14 elaboration of to_matrix_refl took 1.14s
1.14 elaboration of is_open_lt took 1.14s
1.14 elaboration of padic_val_rat_self took 1.14s
1.14 elaboration of defn took 1.14s
1.14 elaboration: tactic execution took 1.14s
1.14 elaboration: tactic execution took 1.14s
1.14 elaboration of indicator_indicator took 1.14s
1.14 elaboration of nndist_edist took 1.14s
1.13 elaboration of slice_unit_vec_mul took 1.13s
1.13 elaboration: tactic execution took 1.13s
1.13 elaboration of coprod.symmetry took 1.13s
1.13 elaboration of tail_val' took 1.13s
1.13 elaboration of sup took 1.13s
1.13 elaboration: tactic execution took 1.13s
1.13 elaboration of inf_uniformity took 1.13s
1.13 elaboration of span_singleton_eq_bot took 1.13s
1.13 elaboration of comap_map_mkq took 1.13s
1.13 elaboration: tactic execution took 1.13s
1.13 elaboration of subset_tangent_cone_prod_right took 1.13s
1.13 decl post-processing of one_ker_inv' took 1.13s
1.13 elaboration of diagonal_add took 1.13s
1.13 elaboration: tactic execution took 1.13s
1.13 elaboration of split_epi_prod_snd took 1.13s
1.13 elaboration: tactic execution took 1.13s
1.13 elaboration: tactic execution took 1.13s
1.13 elaboration of omega_le_cof took 1.13s
1.13 elaboration: tactic execution took 1.13s
1.13 elaboration: tactic execution took 1.13s
1.13 elaboration of disjoint_map_map took 1.13s
1.13 elaboration of frontier_lt_subset_eq took 1.13s
1.13 elaboration: tactic execution took 1.13s
1.13 elaboration: tactic execution took 1.13s
1.13 elaboration of trans took 1.13s
1.13 elaboration of ulower took 1.13s
1.13 elaboration of inv_lt_inv took 1.13s
1.13 elaboration: tactic execution took 1.13s
1.13 elaboration of of_homs took 1.13s
1.13 elaboration of has_colimit_equivalence_comp took 1.13s
1.13 elaboration: tactic execution took 1.13s
1.13 elaboration: tactic execution took 1.13s
1.13 elaboration: tactic execution took 1.13s
1.13 elaboration of cons_zero_zero took 1.13s
1.13 elaboration of bounded_iff_subset_ball took 1.13s
1.13 elaboration of finset.prod_attach_univ took 1.13s
1.13 elaboration: tactic execution took 1.13s
1.13 elaboration of sup_assoc took 1.13s
1.12 elaboration: tactic execution took 1.12s
1.12 elaboration of det_adjugate_of_cancel took 1.12s
1.12 elaboration: tactic execution took 1.12s
1.12 elaboration of module took 1.12s
1.12 elaboration of normal_closure.is_normal took 1.12s
1.12 elaboration: tactic execution took 1.12s
1.12 elaboration of diagonal_mul_diagonal took 1.12s
1.12 elaboration: tactic execution took 1.12s
1.12 elaboration: tactic execution took 1.12s
1.12 elaboration: tactic execution took 1.12s
1.12 elaboration: tactic execution took 1.12s
1.12 elaboration: tactic execution took 1.12s
1.12 elaboration of exists_succ took 1.12s
1.12 elaboration: tactic execution took 1.12s
1.12 elaboration of is_connected_iff_sUnion_disjoint_open took 1.12s
1.12 elaboration: tactic execution took 1.12s
1.12 elaboration: tactic execution took 1.12s
1.12 elaboration: tactic execution took 1.12s
1.12 elaboration: tactic execution took 1.12s
1.12 elaboration: tactic execution took 1.12s
1.12 elaboration of complete_lattice took 1.12s
1.12 elaboration: tactic execution took 1.12s
1.12 elaboration of bundle_mfderiv_comp_at took 1.12s
1.12 elaboration: tactic execution took 1.12s
1.12 elaboration of range_range_restrict took 1.12s
1.12 elaboration of symm_gen took 1.12s
1.12 elaboration: tactic execution took 1.12s
1.12 decl post-processing of is_unit_unit took 1.12s
1.12 elaboration of map_subtype_top took 1.12s
1.12 elaboration: tactic execution took 1.12s
1.12 decl post-processing of mem_prod took 1.12s
1.12 elaboration: tactic execution took 1.12s
1.12 elaboration of support_zip_with took 1.12s
1.12 elaboration of NF.of_dvd_omega_power took 1.12s
1.12 elaboration: tactic execution took 1.12s
1.12 elaboration: tactic execution took 1.12s
1.12 elaboration of compact_iff_closed_bounded took 1.12s
1.12 elaboration: tactic execution took 1.12s
1.12 elaboration of nhds_one_symm took 1.12s
1.12 elaboration of id_inv_app' took 1.12s
1.11 elaboration of topological_group.t1_space took 1.11s
1.11 elaboration: tactic execution took 1.11s
1.11 elaboration of tensor_product took 1.11s
1.11 elaboration of diagonal_neg took 1.11s
1.11 decl post-processing of le_def took 1.11s
1.11 elaboration: tactic execution took 1.11s
1.11 elaboration of map_pointwise_one took 1.11s
1.11 elaboration of complete_linear_order took 1.11s
1.11 elaboration of uniform_embedding_translate took 1.11s
1.11 decl post-processing of ext' took 1.11s
1.11 elaboration of support_neg took 1.11s
1.11 elaboration of transpose_add took 1.11s
1.11 elaboration: tactic execution took 1.11s
1.11 elaboration of add_le_add_right took 1.11s
1.11 elaboration of has_ftaylor_series_up_to_on.has_fderiv_within_at took 1.11s
1.11 elaboration of w took 1.11s
1.11 elaboration of topological_add_group took 1.11s
1.11 elaboration: tactic execution took 1.11s
1.11 elaboration: tactic execution took 1.11s
1.11 elaboration of exists_nhds_split4 took 1.11s
1.11 elaboration of add_NF_below took 1.11s
1.11 elaboration of fst_eq_coprod took 1.11s
1.11 elaboration of snd_eq_coprod took 1.11s
1.11 elaboration of eq_single_iff took 1.11s
1.11 elaboration of iterated_fderiv_within_succ_apply_right took 1.11s
1.11 elaboration of uniform_embedding_iff' took 1.11s
1.11 elaboration of inl_eq_inr took 1.11s
1.11 elaboration of empty took 1.11s
1.11 elaboration of omega_le_oadd took 1.11s
1.11 elaboration of prod_add took 1.11s
1.11 elaboration of metric.emetric_ball_nnreal took 1.11s
1.11 elaboration: tactic execution took 1.11s
1.11 elaboration of abs_exp_sub_one_le took 1.11s
1.11 elaboration of blocks_partial_sum took 1.11s
1.1 elaboration: tactic execution took 1.1s
1.1 elaboration: tactic execution took 1.1s
1.1 elaboration: tactic execution took 1.1s
1.1 elaboration: tactic execution took 1.1s
1.1 elaboration of cSup_intro took 1.1s
1.1 elaboration: tactic execution took 1.1s
1.1 elaboration: tactic execution took 1.1s
1.1 elaboration: tactic execution took 1.1s
1.1 elaboration of order_bot took 1.1s
1.1 elaboration of support_mul took 1.1s
1.1 elaboration: tactic execution took 1.1s
1.1 elaboration: tactic execution took 1.1s
1.1 elaboration: tactic execution took 1.1s
1.1 elaboration of diam_closed_ball took 1.1s
1.1 elaboration of pointwise_mul_monoid took 1.1s
1.1 elaboration: tactic execution took 1.1s
1.1 elaboration of id_hom_app' took 1.1s
1.1 elaboration of mkq took 1.1s
1.1 elaboration of nat_elim took 1.1s
1.1 elaboration: tactic execution took 1.1s
1.1 elaboration of bounded_empty took 1.1s
1.1 elaboration: tactic execution took 1.1s
1.1 elaboration: tactic execution took 1.1s
1.1 elaboration: tactic execution took 1.1s
1.1 elaboration: tactic execution took 1.1s
1.1 elaboration: tactic execution took 1.1s
1.1 decl post-processing of prod_preimage took 1.1s
1.1 elaboration of mk_eq_zero took 1.1s
1.1 elaboration: tactic execution took 1.1s
1.1 elaboration of infi_principal_finset took 1.1s
1.1 decl post-processing of prod_eq_foldr took 1.1s
1.1 elaboration: tactic execution took 1.1s
1.1 elaboration of ordered_cancel_comm_monoid took 1.1s
1.1 elaboration: tactic execution took 1.1s
1.1 elaboration: tactic execution took 1.1s
1.1 elaboration of nndist_triangle took 1.1s
1.1 elaboration of ordered_add_comm_group took 1.1s
1.09 elaboration: tactic execution took 1.09s
1.09 elaboration: tactic execution took 1.09s
1.09 elaboration: tactic execution took 1.09s
1.09 elaboration of fst.is_semiring_hom took 1.09s
1.09 elaboration of cons_val_fin_one took 1.09s
1.09 elaboration of image_union took 1.09s
1.09 elaboration of smul_add_hom took 1.09s
1.09 elaboration of fintype_walking_pair took 1.09s
1.09 elaboration: tactic execution took 1.09s
1.09 elaboration of sign_aux3_symm_trans_trans took 1.09s
1.09 elaboration: tactic execution took 1.09s
1.09 elaboration of cone_point took 1.09s
1.09 elaboration: tactic execution took 1.09s
1.09 elaboration of size_up_to_index_le took 1.09s
1.09 elaboration: tactic execution took 1.09s
1.09 elaboration: tactic execution took 1.09s
1.09 elaboration: tactic execution took 1.09s
1.09 elaboration: tactic execution took 1.09s
1.09 elaboration: tactic execution took 1.09s
1.09 elaboration: tactic execution took 1.09s
1.09 elaboration: tactic execution took 1.09s
1.09 elaboration of move_left_card took 1.09s
1.09 elaboration of int.metric_space took 1.09s
1.09 elaboration: tactic execution took 1.09s
1.09 elaboration of prod_map_add took 1.09s
1.09 elaboration of finite_nat_iff took 1.09s
1.09 elaboration: tactic execution took 1.09s
1.09 elaboration: tactic execution took 1.09s
1.09 elaboration: tactic execution took 1.09s
1.09 elaboration: tactic execution took 1.09s
1.09 elaboration: tactic execution took 1.09s
1.09 elaboration: tactic execution took 1.09s
1.09 elaboration of prod.symmetry took 1.09s
1.09 elaboration: tactic execution took 1.09s
1.09 elaboration: tactic execution took 1.09s
1.09 elaboration of precompose_id took 1.09s
1.09 elaboration: tactic execution took 1.09s
1.09 elaboration of map_zero took 1.09s
1.09 elaboration: tactic execution took 1.09s
1.09 elaboration of coe_mem_upper_bounds took 1.09s
1.09 elaboration of tendsto_log_one_zero took 1.09s
1.09 elaboration: tactic execution took 1.09s
1.09 elaboration: tactic execution took 1.09s
1.08 elaboration: tactic execution took 1.08s
1.08 elaboration of red.step.to_group took 1.08s
1.08 elaboration of repr_of_nat took 1.08s
1.08 elaboration: tactic execution took 1.08s
1.08 elaboration: tactic execution took 1.08s
1.08 elaboration: tactic execution took 1.08s
1.08 elaboration of totally_bounded_iff_subset took 1.08s
1.08 elaboration of map.unique took 1.08s
1.08 elaboration: tactic execution took 1.08s
1.08 elaboration of mem_ball_comm took 1.08s
1.08 elaboration of sum_nat_coe_enat took 1.08s
1.08 elaboration of step_aux_read took 1.08s
1.08 decl post-processing of closure_range_of took 1.08s
1.08 elaboration: tactic execution took 1.08s
1.08 elaboration of snd.is_ring_hom took 1.08s
1.08 elaboration of complete_space_extension took 1.08s
1.08 elaboration of postcompose_id took 1.08s
1.08 elaboration of liminf_const took 1.08s
1.08 elaboration of limsup_const took 1.08s
1.08 elaboration: tactic execution took 1.08s
1.08 elaboration: tactic execution took 1.08s
1.08 elaboration: tactic execution took 1.08s
1.08 elaboration of lintegral_eq_supr_eapprox_integral took 1.08s
1.08 elaboration of Cauchy_eq took 1.08s
1.08 elaboration: tactic execution took 1.08s
1.08 elaboration: tactic execution took 1.08s
1.08 elaboration: tactic execution took 1.08s
1.08 elaboration: tactic execution took 1.08s
1.08 elaboration of eq_swap_of_is_cycle_of_apply_apply_eq_self took 1.08s
1.08 elaboration of list_prod_mem took 1.08s
1.08 elaboration: tactic execution took 1.08s
1.08 elaboration: tactic execution took 1.08s
1.08 elaboration: tactic execution took 1.08s
1.08 elaboration: tactic execution took 1.08s
1.08 elaboration: tactic execution took 1.08s
1.08 elaboration of map_subtype_le took 1.08s
1.08 elaboration: tactic execution took 1.08s
1.08 elaboration: tactic execution took 1.08s
1.08 elaboration of multiplicity_pow took 1.08s
1.08 elaboration of geom_sum_inv took 1.08s
1.08 elaboration of op_obj_op took 1.08s
1.08 elaboration of le_comap_mkq took 1.08s
1.08 elaboration: tactic execution took 1.08s
1.08 elaboration of cprank_max_add took 1.08s
1.08 elaboration: tactic execution took 1.08s
1.08 elaboration: tactic execution took 1.08s
1.08 elaboration of tanh_zero took 1.08s
1.08 elaboration: tactic execution took 1.08s
1.07 elaboration of is_topological_fiber_bundle_snd took 1.07s
1.07 elaboration: tactic execution took 1.07s
1.07 elaboration of card_units_eq_totient took 1.07s
1.07 elaboration: tactic execution took 1.07s
1.07 elaboration of continuous_within_at_iff_continuous_within_at_comp_left took 1.07s
1.07 elaboration of eq_ones_iff took 1.07s
1.07 elaboration: tactic execution took 1.07s
1.07 elaboration: tactic execution took 1.07s
1.07 decl post-processing of image_subgroup took 1.07s
1.07 decl post-processing of mul_inv_cancel_left took 1.07s
1.07 elaboration of multiplicity_le_multiplicity_choose_add took 1.07s
1.07 elaboration of range_subtype took 1.07s
1.07 elaboration of real.dist_0_eq_abs took 1.07s
1.07 elaboration of lim took 1.07s
1.07 elaboration of coe_bind took 1.07s
1.07 elaboration of support_eq_empty took 1.07s
1.07 elaboration of fintype_of_fintype_image took 1.07s
1.07 elaboration of mem_range_embedding_iff took 1.07s
1.07 elaboration of NF_repr_split took 1.07s
1.07 elaboration: tactic execution took 1.07s
1.07 elaboration of rmap took 1.07s
1.07 elaboration: tactic execution took 1.07s
1.07 elaboration of model_with_corners.prod took 1.07s
1.07 elaboration of hom_iso' took 1.07s
1.07 elaboration of ennreal.tendsto_pow_at_top_nhds_0_of_lt_1 took 1.07s
1.07 elaboration of is_Z_bilin.comp_hom took 1.07s
1.07 elaboration: tactic execution took 1.07s
1.07 elaboration of op_obj_unop took 1.07s
1.07 elaboration of of_primrec took 1.07s
1.07 elaboration: tactic execution took 1.07s
1.07 elaboration: tactic execution took 1.07s
1.07 elaboration of order_topology.regular_space took 1.07s
1.07 elaboration: tactic execution took 1.07s
1.07 elaboration of is_cau_seq_iff_lift took 1.07s
1.07 elaboration of univ_inaccessible took 1.07s
1.07 elaboration of finset.univ_sum_single took 1.07s
1.07 elaboration of trivial_normal took 1.07s
1.07 elaboration of of_mul_equiv took 1.07s
1.06 elaboration: tactic execution took 1.06s
1.06 elaboration of op_map_comp_obj took 1.06s
1.06 elaboration: tactic execution took 1.06s
1.06 elaboration of comp took 1.06s
1.06 elaboration of of_equiv took 1.06s
1.06 elaboration of has_zero took 1.06s
1.06 elaboration of one_sub_K_ne_top took 1.06s
1.06 elaboration: tactic execution took 1.06s
1.06 elaboration of decidable_rel took 1.06s
1.06 elaboration: tactic execution took 1.06s
1.06 elaboration of computable_iff_re_compl_re took 1.06s
1.06 elaboration: tactic execution took 1.06s
1.06 elaboration of has_shift took 1.06s
1.06 elaboration of bernoulli_two took 1.06s
1.06 elaboration: tactic execution took 1.06s
1.06 elaboration of cof_sup_le took 1.06s
1.06 elaboration of measurable.if took 1.06s
1.06 elaboration: tactic execution took 1.06s
1.06 elaboration of order_dual.order_topology took 1.06s
1.06 elaboration of comap_zero took 1.06s
1.06 elaboration of to_real_mul_to_real took 1.06s
1.06 elaboration of hom_mk took 1.06s
1.06 elaboration of prod_ite_eq' took 1.06s
1.06 elaboration of cast_eq_mod took 1.06s
1.06 elaboration of associator took 1.06s
1.06 elaboration of countable_prod took 1.06s
1.06 elaboration of cons_val' took 1.06s
1.06 decl post-processing of is_group_hom_quotient_lift took 1.06s
1.06 elaboration of composition.to_composition_as_set_blocks took 1.06s
1.06 elaboration: tactic execution took 1.06s
1.06 elaboration of subsingleton_hom took 1.06s
1.06 elaboration of edist_le_Ico_sum_edist took 1.06s
1.06 elaboration: tactic execution took 1.06s
1.06 elaboration of exists_list_of_mem_closure took 1.06s
1.06 elaboration: tactic execution took 1.06s
1.06 elaboration of irreducible_iff_nat_prime took 1.06s
1.06 elaboration: tactic execution took 1.06s
1.06 elaboration of rat_mul_continuous_lemma took 1.06s
1.06 elaboration: tactic execution took 1.06s
1.06 elaboration of comm_group took 1.06s
1.06 elaboration of opposite took 1.06s
1.06 elaboration: tactic execution took 1.06s
1.05 elaboration of cos_add took 1.05s
1.05 elaboration: tactic execution took 1.05s
1.05 elaboration: tactic execution took 1.05s
1.05 elaboration of cosh_add took 1.05s
1.05 elaboration of list_blank.ext took 1.05s
1.05 elaboration: tactic execution took 1.05s
1.05 elaboration: tactic execution took 1.05s
1.05 elaboration of mem_traverse took 1.05s
1.05 elaboration of mem_fixed_points_iff_card_orbit_eq_one took 1.05s
1.05 elaboration of join_join took 1.05s
1.05 elaboration of eq_mlocus took 1.05s
1.05 elaboration: tactic execution took 1.05s
1.05 elaboration of map_comp_obj_unop took 1.05s
1.05 elaboration: tactic execution took 1.05s
1.05 elaboration of mul took 1.05s
1.05 elaboration of exists_Z_half took 1.05s
1.05 elaboration: tactic execution took 1.05s
1.05 elaboration: tactic execution took 1.05s
1.05 elaboration: tactic execution took 1.05s
1.05 elaboration of filter.tendsto.sub took 1.05s
1.05 elaboration of pi_lt_3141593 took 1.05s
1.05 elaboration of mul' took 1.05s
1.05 elaboration of dot_product_diagonal' took 1.05s
1.05 decl post-processing of is_unit took 1.05s
1.05 elaboration of dot_product_diagonal took 1.05s
1.05 elaboration of convergents_eq_convergents' took 1.05s
1.05 elaboration: tactic execution took 1.05s
1.05 elaboration of nnreal.am_gm_weighted took 1.05s
1.05 elaboration: tactic execution took 1.05s
1.05 elaboration of abs_cpow_real took 1.05s
1.05 elaboration: tactic execution took 1.05s
1.05 elaboration of exists_gpow_eq_one took 1.05s
1.05 elaboration of to_nnreal_eq_zero_iff took 1.05s
1.05 elaboration of succ_nth_convergent_eq_squash_gcf_nth_convergent took 1.05s
1.05 elaboration of reduce.red took 1.05s
1.05 elaboration: tactic execution took 1.05s
1.05 elaboration: tactic execution took 1.05s
1.05 elaboration: tactic execution took 1.05s
1.05 elaboration of functor_category_colimit_cocone took 1.05s
1.04 decl post-processing of mem_closure_union_iff took 1.04s
1.04 elaboration of subset_union_elim took 1.04s
1.04 elaboration of forget_creates_colimits took 1.04s
1.04 elaboration: tactic execution took 1.04s
1.04 elaboration: tactic execution took 1.04s
1.04 elaboration of list_prod_apply took 1.04s
1.04 elaboration of cons_val_succ' took 1.04s
1.04 elaboration: tactic execution took 1.04s
1.04 elaboration of NF_mul_nat took 1.04s
1.04 elaboration: tactic execution took 1.04s
1.04 elaboration of mk_preimage_of_subset_range_lift took 1.04s
1.04 elaboration of has_Sup took 1.04s
1.04 elaboration of inducing.continuous_iff took 1.04s
1.04 elaboration of cauchy_prod took 1.04s
1.04 elaboration of sup_lt_ord took 1.04s
1.04 elaboration: tactic execution took 1.04s
1.04 elaboration: tactic execution took 1.04s
1.04 elaboration: tactic execution took 1.04s
1.04 elaboration of cycle_of_inv took 1.04s
1.04 elaboration of subtype_perm_of_subtype took 1.04s
1.04 elaboration: tactic execution took 1.04s
1.04 elaboration of mem_iff_of_subtype_apply_mem took 1.04s
1.04 elaboration of multiplicity_pow_self took 1.04s
1.04 decl post-processing of eq_mlocus took 1.04s
1.04 elaboration: tactic execution took 1.04s
1.04 elaboration of finset.range_prod_eq_univ_prod took 1.04s
1.04 elaboration of cast_mod_nat took 1.04s
1.04 elaboration: tactic execution took 1.04s
1.04 elaboration: tactic execution took 1.04s
1.04 elaboration of to_group.is_group_hom took 1.04s
1.04 elaboration of map_id took 1.04s
1.04 elaboration: tactic execution took 1.04s
1.04 elaboration of fst.is_ring_hom took 1.04s
1.04 elaboration: tactic execution took 1.04s
1.04 elaboration of sqrt took 1.04s
1.04 elaboration of uniform_inducing_pure_cauchy took 1.04s
1.04 elaboration of lift_inj took 1.04s
1.04 elaboration of cast_add_of_ne_zero took 1.04s
1.04 elaboration: tactic execution took 1.04s
1.04 elaboration: tactic execution took 1.04s
1.04 elaboration of lift_rel took 1.04s
1.04 elaboration of evaln_bound took 1.04s
1.04 elaboration of diagonal_transpose took 1.04s
1.04 elaboration: tactic execution took 1.04s
1.04 elaboration: tactic execution took 1.04s
1.04 elaboration: tactic execution took 1.04s
1.04 elaboration of erase_ne took 1.04s
1.04 elaboration of change_origin_summable_aux3 took 1.04s
1.04 elaboration of is_closed_eq took 1.04s
1.04 elaboration of vec_mul_zero took 1.04s
1.04 elaboration: tactic execution took 1.04s
1.04 elaboration of sigma_pi_composition_eq_iff took 1.04s
1.03 elaboration of metric.complete_of_convergent_controlled_sequences took 1.03s
1.03 elaboration of pure_cauchy_dense took 1.03s
1.03 elaboration: tactic execution took 1.03s
1.03 elaboration of hom_iso' took 1.03s
1.03 elaboration: tactic execution took 1.03s
1.03 elaboration: tactic execution took 1.03s
1.03 elaboration: tactic execution took 1.03s
1.03 elaboration of sub_apply took 1.03s
1.03 elaboration of pi_field_equiv took 1.03s
1.03 elaboration of power_le_max_power_one took 1.03s
1.03 elaboration: tactic execution took 1.03s
1.03 elaboration: tactic execution took 1.03s
1.03 decl post-processing of closure_mono took 1.03s
1.03 elaboration of diagonal_dot_product took 1.03s
1.03 elaboration of continuous.sub took 1.03s
1.03 elaboration: tactic execution took 1.03s
1.03 elaboration of cprank_max_upper_bound took 1.03s
1.03 elaboration: tactic execution took 1.03s
1.03 elaboration: tactic execution took 1.03s
1.03 elaboration: tactic execution took 1.03s
1.03 elaboration: tactic execution took 1.03s
1.03 elaboration: tactic execution took 1.03s
1.03 elaboration of extend_function_of_lt took 1.03s
1.03 elaboration: tactic execution took 1.03s
1.03 elaboration: tactic execution took 1.03s
1.03 elaboration of cons_val_succ took 1.03s
1.03 elaboration of tendsto_list_prod took 1.03s
1.03 elaboration of mul_not_equiv_zero took 1.03s
1.03 elaboration: tactic execution took 1.03s
1.03 elaboration of is_lawful_monad took 1.03s
1.03 elaboration: tactic execution took 1.03s
1.03 elaboration of smul_eq_diagonal_mul took 1.03s
1.03 elaboration of is_subgroup took 1.03s
1.03 elaboration: tactic execution took 1.03s
1.03 elaboration of smul_eq_mul_diagonal took 1.03s
1.03 elaboration of card_support_swap took 1.03s
1.03 elaboration of is_preconnected_iff_subset_of_disjoint took 1.03s
1.03 elaboration: tactic execution took 1.03s
1.03 elaboration of finite_dimensional.complete took 1.03s
1.03 elaboration of NF.zero_of_zero took 1.03s
1.03 elaboration of lift_comp took 1.03s
1.02 elaboration: tactic execution took 1.02s
1.02 elaboration of exists_code took 1.02s
1.02 decl post-processing of prod_bind took 1.02s
1.02 elaboration: tactic execution took 1.02s
1.02 elaboration: tactic execution took 1.02s
1.02 elaboration: tactic execution took 1.02s
1.02 elaboration of algebra_iso_of_iso took 1.02s
1.02 elaboration: tactic execution took 1.02s
1.02 elaboration of finite_dimensional.proper took 1.02s
1.02 elaboration of step.append_right took 1.02s
1.02 elaboration of sin_add took 1.02s
1.02 elaboration of fintype_walking_parallel_pair took 1.02s
1.02 elaboration of ne_and_ne_of_swap_mul_apply_ne_self took 1.02s
1.02 elaboration of compact_space_of_finite_subfamily_closed took 1.02s
1.02 elaboration of enumerate_inj took 1.02s
1.02 elaboration: tactic execution took 1.02s
1.02 elaboration of is_topological_fiber_bundle_fst took 1.02s
1.02 elaboration of comap_has_scalar took 1.02s
1.02 elaboration of sequential_space took 1.02s
1.02 elaboration: tactic execution took 1.02s
1.02 decl post-processing of inv took 1.02s
1.02 elaboration: tactic execution took 1.02s
1.02 elaboration: tactic execution took 1.02s
1.02 elaboration of one took 1.02s
1.02 elaboration: tactic execution took 1.02s
1.02 parsing took 1.02s
1.02 elaboration of prod_pow_eq_pow_sum took 1.02s
1.02 elaboration: tactic execution took 1.02s
1.02 elaboration of Sup_of_continuous took 1.02s
1.02 elaboration of cof_zero took 1.02s
1.02 elaboration: tactic execution took 1.02s
1.02 elaboration of fintype.card_sum took 1.02s
1.02 elaboration: tactic execution took 1.02s
1.02 elaboration of map_length_split_wrt_composition_aux took 1.02s
1.02 elaboration: tactic execution took 1.02s
1.02 elaboration of hG took 1.02s
1.02 elaboration of exp_conj took 1.02s
1.02 elaboration of cosh_sub took 1.02s
1.02 elaboration of conj_inv took 1.02s
1.02 elaboration of comm_ring took 1.02s
1.02 elaboration of conditionally_complete_linear_order_bot took 1.02s
1.02 elaboration of module.gsmul_eq_smul_cast took 1.02s
1.02 elaboration of Inf_lt took 1.02s
1.02 elaboration: tactic execution took 1.02s
1.02 elaboration of card_le_of_subset took 1.02s
1.02 elaboration: tactic execution took 1.02s
1.01 elaboration of bounded took 1.01s
1.01 elaboration of disjoint_union_left took 1.01s
1.01 elaboration: tactic execution took 1.01s
1.01 elaboration: tactic execution took 1.01s
1.01 elaboration of of.inj took 1.01s
1.01 elaboration of tendsto_iff_rtendsto' took 1.01s
1.01 elaboration of finset.prod took 1.01s
1.01 elaboration: tactic execution took 1.01s
1.01 elaboration of tail_cons took 1.01s
1.01 elaboration of right_inverse_eq took 1.01s
1.01 elaboration: tactic execution took 1.01s
1.01 elaboration of pmap_res took 1.01s
1.01 elaboration: tactic execution took 1.01s
1.01 elaboration of subtype_perm took 1.01s
1.01 elaboration of map took 1.01s
1.01 elaboration of continuous_on_iff_continuous_on_comp_right took 1.01s
1.01 elaboration of op_map_id_obj took 1.01s
1.01 elaboration of is_add_subgroup.gsmul_coe took 1.01s
1.01 elaboration of valid.as_list_nodup took 1.01s
1.01 elaboration: tactic execution took 1.01s
1.01 elaboration: tactic execution took 1.01s
1.01 elaboration: tactic execution took 1.01s
1.01 elaboration of ball_insert_iff took 1.01s
1.01 elaboration of pow_cast_right took 1.01s
1.01 elaboration of mul_action took 1.01s
1.01 elaboration of fin.prod_univ_cast_succ took 1.01s
1.01 elaboration of cosh_neg took 1.01s
1.01 elaboration of equivalence took 1.01s
1.01 elaboration of vec_mul_vec_eq took 1.01s
1.01 elaboration of eq_pell_lem took 1.01s
1.01 elaboration: tactic execution took 1.01s
1.01 elaboration of sqrt_two_add_series_step_up took 1.01s
1.01 elaboration: tactic execution took 1.01s
1.01 elaboration: tactic execution took 1.01s
1.01 elaboration of functor_category_limit_cone took 1.01s
1.01 elaboration of lift_lt took 1.01s
1.01 elaboration of of_rel_of_rel took 1.01s
1.01 decl post-processing of mrange_top_iff_surjective took 1.01s
1.01 elaboration of inv_top took 1.01s
1.01 elaboration: tactic execution took 1.01s
1.01 elaboration of eq_of_add_eq_of_omega_le took 1.01s
1.01 elaboration of of_inj took 1.01s
1.01 elaboration: tactic execution took 1.01s
1.01 elaboration of powers_eq_gpowers took 1.01s
1.01 elaboration of countable_set_of_finite_subset took 1.01s
1.01 elaboration of rfind took 1.01s
1.01 elaboration: tactic execution took 1.01s
1.01 elaboration of left_coset_equiv_subgroup took 1.01s
1 elaboration: tactic execution took 1s
1 elaboration of lift_rel₂ took 1s
1 elaboration of mod_by_monic_eq_sub_mul_div took 1s
1 elaboration: tactic execution took 1s
1 elaboration: tactic execution took 1s
1 elaboration of slice_sum took 1s
1 elaboration of x_sub_y_dvd_pow took 1s
1 elaboration of prod took 1s
1 elaboration of cof_eq_zero took 1s
1 elaboration of op_map_id_obj took 1s
1 elaboration of nat_strong_rec took 1s
1 elaboration of support_map_range took 1s
1 elaboration of denumerable_list_aux took 1s
1 elaboration: tactic execution took 1s
1 elaboration of map_id_obj_unop took 1s
1 elaboration of prod_pow took 1s
1 elaboration of int.coe_nat_multiplicity took 1s
1 elaboration: tactic execution took 1s
1 elaboration of gpow_eq_mod_order_of took 1s
1 elaboration: tactic execution took 1s
1 elaboration of mul_vec_zero took 1s