Lean calc/show restating a goal with untyped `2 ^ m` inside a Finset filter can cost 600k heartbeats

Lean 4.35.0 / Mathlib v4.35.0. Goal #{m ∈ Icc 1 M | t ⊆ (2 ^ m).primeFactors} ≤ B (or 2 ^ m - 1, or .divisors): restating it with show costs ~115k heartbeats and with a restating calc first term ~634k, so the default 200k limit gives '(deterministic) timeout at isDefEq/whnf' on the calc keyword even when all steps are sorry. Measured with #count_heartbeats in: the trigger is the untyped numeral base. ((2 : ℕ) ^ m) costs 72; (n ^ m) with n : ℕ, m.primeFactors, (m - 1).primeFactors all < 200. Fixes: ascribe (2 : ℕ) in the restated term; or calc _ ≤ ...; or have h : <stmt> := ...; exact h (cheap). classical made no measurable difference.