slow typeclass synthesis: takes 19000 heartbeats to fail in MulHomClass C(ℝ, ↥circle) ?m ?m

[kim-em]

import Mathlib

/--
error: failed to synthesize
  MulHomClass C(ℝ, ↥circle) ?m.26276 ?m.26277
(deterministic) timeout at 'typeclass', maximum number of heartbeats (19000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)
-/
#guard_msgs in
set_option synthInstance.maxHeartbeats 19000 in
example : expMapCircle (2 * π) = 1 := by simp

This then gets slightly worse after leanprover/lean4#3807, and thereafter causes the simpNF linter to fail on expMapCircle_two_pi.

[mattrobball]

Also fixed by leanprover/lean4#4085

[jcommelin]

Confirm:

import Mathlib

open Real in
set_option synthInstance.maxHeartbeats 8000 in
example : expMapCircle (2 * π) = 1 := by simp