From 29d5700b0872ffc82431073f46c5b1092f74151c Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 15 Mar 2023 11:17:36 +0000 Subject: [PATCH] chore(geometry/manifold/instances/sphere): speedup a proof (#18586) This goes from 15s to 1.75 seconds. I've squeezed this in multiple steps to make the proof easier to follow. --- src/geometry/manifold/instances/sphere.lean | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/geometry/manifold/instances/sphere.lean b/src/geometry/manifold/instances/sphere.lean index 1ad1ee1abe08f..45b43f2d94681 100644 --- a/src/geometry/manifold/instances/sphere.lean +++ b/src/geometry/manifold/instances/sphere.lean @@ -398,8 +398,15 @@ begin have H₂ := (cont_diff_stereo_inv_fun_aux.comp (ℝ ∙ (v:E))ᗮ.subtypeL.cont_diff).comp U.symm.cont_diff, convert H₁.comp' (H₂.cont_diff_on : cont_diff_on ℝ ⊤ _ set.univ) using 1, - ext, - simp [sphere_ext_iff, stereographic'_symm_apply, real_inner_comm] + -- squeezed from `ext, simp [sphere_ext_iff, stereographic'_symm_apply, real_inner_comm]` + simp only [local_homeomorph.trans_to_local_equiv, local_homeomorph.symm_to_local_equiv, + local_equiv.trans_source, local_equiv.symm_source, stereographic'_target, + stereographic'_source], + simp only [model_with_corners_self_coe, model_with_corners_self_coe_symm, set.preimage_id, + set.range_id, set.inter_univ, set.univ_inter, set.compl_singleton_eq, set.preimage_set_of_eq], + simp only [id.def, comp_apply, submodule.subtypeL_apply, local_homeomorph.coe_coe_symm, + innerSL_apply, ne.def, sphere_ext_iff, real_inner_comm (v' : E)], + refl, end /-- The inclusion map (i.e., `coe`) from the sphere in `E` to `E` is smooth. -/