perf(topology/continuous_function/stone_weierstrass): fix timeout (#1…

…6844)

Squeeze simps and replace a slow `convert` by `eq.subst` with explicit motive (maybe `convert` was unfolding the instances?).

From >20s to 4s on my machine.



Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

src/measure_theory/integral/circle_transform.lean

@@ -132,8 +132,11 @@ begin
   have cts := continuous_on_abs_circle_transform_bounding_function hr z,
   have comp : is_compact (closed_ball z r ×ˢ [0, 2 * π]),
   { apply_rules [is_compact.prod, proper_space.is_compact_closed_ball z r, is_compact_interval], },
-  have none := (nonempty_closed_ball.2 hr').prod nonempty_interval,
-  simpa using is_compact.exists_forall_ge comp none (cts.mono (by { intro z, simp, tauto })),
+  have none : (closed_ball z r ×ˢ [0, 2 * π]).nonempty :=
+    (nonempty_closed_ball.2 hr').prod nonempty_interval,
+  have := is_compact.exists_forall_ge comp none (cts.mono
+    (by { intro z, simp only [mem_prod, mem_closed_ball, mem_univ, and_true, and_imp], tauto })),
+  simpa only [set_coe.forall, subtype.coe_mk, set_coe.exists],
 end
 
 /-- The derivative of a `circle_transform` is locally bounded. -/

src/topology/continuous_function/stone_weierstrass.lean

@@ -393,10 +393,9 @@ begin
   let F : C(X, 𝕜) := f - const _ (f x₂),
   -- Subtract the constant `f x₂` from `f`; this is still an element of the subalgebra
   have hFA : F ∈ A,
-  { refine A.sub_mem hfA _,
-    convert A.smul_mem A.one_mem (f x₂),
-    ext1,
-    simp },
+  { refine A.sub_mem hfA (@eq.subst _ (∈ A) _ _ _ $ A.smul_mem A.one_mem $ f x₂),
+    ext1, simp only [coe_smul, coe_one, pi.smul_apply,
+      pi.one_apply, algebra.id.smul_eq_mul, mul_one, const_apply] },
   -- Consider now the function `λ x, |f x - f x₂| ^ 2`
   refine ⟨_, ⟨(⟨is_R_or_C.norm_sq, continuous_norm_sq⟩ : C(𝕜, ℝ)).comp F, _, rfl⟩, _⟩,
   { -- This is also an element of the subalgebra, and takes only real values
@@ -407,7 +406,8 @@ begin
     exact (is_R_or_C.mul_conj _).symm },
   { -- And it also separates the points `x₁`, `x₂`
     have : f x₁ - f x₂ ≠ 0 := sub_ne_zero.mpr hf,
-    simpa using this },
+    simpa only [comp_apply, coe_sub, coe_const, pi.sub_apply,
+      coe_mk, sub_self, map_zero, ne.def, norm_sq_eq_zero] using this },
 end
 
 variables [compact_space X]