perf(analysis/complex/circle): fix a slow @[simps] (#17504)

j-loreaux · j-loreaux · commit ad3dfaca9ea2 · 2022-11-13T01:44:34.000Z
This `@[simps]` is really slow on master and caused me a timeout in #17164, and moreover it generated a bad `simp` lemma (it used `↥(metric.sphere 0 1)` instead of `↥circle`), so I just wrote the lemma by hand.
diff --git a/src/analysis/complex/circle.lean b/src/analysis/complex/circle.lean
@@ -64,7 +64,11 @@ by rw [coe_inv_circle, inv_def, norm_sq_eq_of_mem_circle, inv_one, of_real_one,
 circle.subtype.map_div z w
 
 /-- The elements of the circle embed into the units. -/
-@[simps apply] def circle.to_units : circle →* units ℂ := unit_sphere_to_units ℂ
+def circle.to_units : circle →* units ℂ := unit_sphere_to_units ℂ
+
+-- written manually because `@[simps]` was slow and generated the wrong lemma
+@[simp] lemma circle.to_units_apply (z : circle) :
+  circle.to_units z = units.mk0 z (ne_zero_of_mem_circle z) := rfl
 
 instance : compact_space circle := metric.sphere.compact_space _ _
 
