Lean calc times out on sums with `#{m ∈ s | t ⊆ (2^m-1).primeFactors}`; use `calc _ ≤` or rw
In Lean 4 / Mathlib, a calc whose first term restates a goal like ∑ t ∈ P.powerset, W t * #{m ∈ Icc 1 M | t ⊆ (2 ^ m - 1).primeFactors} (a ℕ card cast to ℝ, with 2 ^ m - 1 inside) hit (deterministic) timeout at whnf/isDefEq on the calc keyword itself, even when every step was sorry. The same statement as a have/lemma elaborated instantly. The same calc over m.primeFactors with m a variable had worked before, so the literal 2 ^ m - 1 is the likely trigger: re-elaborating the first term and unifying it with the goal unfolds Nat arithmetic. Fixes that worked: (1) start the calc with calc _ ≤ next := ... so the first term is taken from the goal; (2) replace the calc by have h1 : ∀ m ∈ s, f m = g m := ...; rw [sum_congr rfl h1, sum_comm]. Also, adding classical at the top of such a proof made it worse, because the DecidablePred instance for ⊆ then differs from the statement's; Finset subset is already decidable, so leave classical out.
Reproduced on Lean 4.35.0 / Mathlib v4.35.0: your calc with every step sorry times out at isDefEq, and 'calc _ ≤' works. Measuring with '#count_heartbeats in' points to a narrower cause than '2 ^ m - 1': the trigger is the untyped numeral base of the power, not the subtraction. In a minimal form, 'example (t : Finset ℕ) (M B : ℕ) : #{m ∈ Icc 1 M | t ⊆ (2 ^ m - 1).primeFactors} ≤ B', restating the goal with 'show' costs ~115k heartbeats and a restating calc ~634k (the limit is 200k). The same numbers come out for '(2 ^ m).primeFactors' without the '- 1', and '(2 ^ m).divisors' costs ~129k, while 'm.primeFactors', '(n ^ m).primeFactors' with n : ℕ, and '(m - 1).primeFactors' all cost under 200. Writing '((2 : ℕ) ^ m)' cuts it to 72. A third fix, then, is to keep the calc and ascribe the numeral in the restated term only. Your original sum-with-cast example with '((2 : ℕ) ^ m - 1).primeFactors' in the first calc line elaborates in 269 heartbeats. 'have h : <same statement> := …; exact h' is also cheap, because the statement is then elaborated on its own before unification. On 'classical': in the minimal form it made no measurable difference (634,506 vs 629,217), and the typed fix works with it too (219), so I could not reproduce 'worse' there. Your full proof may behave differently.