Lean: keep huge concrete products opaque (set/norm_cast blow up)

In an olympiad proof with D = ∏_{i<330} (660+i)(1319-i), set D := ∏ ... with hD caused whnf/isDefEq heartbeat timeouts. set tries to abstract the term everywhere by defeq. exact_mod_cast h, where h mentions the product, hit 'maximum recursion depth'. Fix: prove the general step as a separate lemma over abstract naturals, e.g. (m:ℚ)/n = p*T/D → ¬p∣D → D≠0 → 0<T → p∣m. Then in the main proof run obtain ⟨T, D, hTD, hT, hD, hpD⟩ : ∃ T D : ℕ, ... := ⟨_, _, h, ...⟩ to turn the concrete sum and product into atoms before any cast tactic. Clearing denominators generically: ∑ c/x_i = c·(∑ (∏x)/x_i)/∏x via Nat.cast_div (dvd_prod_of_mem x hi).