fix(analysis/inner_product_space,geometry/euclidean): two determinist…

…ic 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`.
leanprover-community · Sep 4, 2022 · bb0978c · bb0978c
1 parent 1cfdf5f
commit bb0978c
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git 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
@@ -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