From bb0978c26626b8ce0eb39eeb1a36a21fa914b0a5 Mon Sep 17 00:00:00 2001 From: Mauricio Collares Date: Sun, 4 Sep 2022 06:25:03 +0000 Subject: [PATCH] fix(analysis/inner_product_space,geometry/euclidean): two deterministic timeout fixes (#16365) CI seems to be having some issues after #16356, which I can't reproduce with `-T100000` locally but can with `-T90000`. This PR speeds up `analysis/inner_product_space/l2_space.lean:hilbert_basis.coe_mk` (which was already investigated before in #15271) and `geometry/euclidean/oriented_angle.lean:inner_eq_norm_mul_norm_mul_cos_oangle`. --- src/analysis/inner_product_space/l2_space.lean | 2 +- src/geometry/euclidean/oriented_angle.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analysis/inner_product_space/l2_space.lean b/src/analysis/inner_product_space/l2_space.lean index 1a07d1c490c3a..5257cbb58485f 100644 --- a/src/analysis/inner_product_space/l2_space.lean +++ b/src/analysis/inner_product_space/l2_space.lean @@ -501,7 +501,7 @@ by rw [is_hilbert_sum.linear_isometry_equiv_symm_apply_single, @[simp] protected lemma coe_mk (hsp : ⊤ ≤ (span 𝕜 (set.range v)).topological_closure) : ⇑(hilbert_basis.mk hv hsp) = v := -funext $ orthonormal.linear_isometry_equiv_symm_apply_single_one hv _ +by apply (funext $ orthonormal.linear_isometry_equiv_symm_apply_single_one hv hsp) /-- An orthonormal family of vectors whose span has trivial orthogonal complement is a Hilbert basis. -/ diff --git a/src/geometry/euclidean/oriented_angle.lean b/src/geometry/euclidean/oriented_angle.lean index 8762d2e983886..c803acefa02d3 100644 --- a/src/geometry/euclidean/oriented_angle.lean +++ b/src/geometry/euclidean/oriented_angle.lean @@ -879,7 +879,7 @@ begin star_ring_end_apply, star_trivial], rw [finset.sum_insert (dec_trivial : (0 : fin 2) ∉ ({1} : finset (fin 2))), finset.sum_singleton], - field_simp [norm_ne_zero_iff.2 hx, norm_ne_zero_iff.2 hy], + field_simp only [norm_ne_zero_iff.2 hx, norm_ne_zero_iff.2 hy, ne.def, not_false_iff], ring end