# Lean 4: tauto/contradiction stall in huge proof contexts; use explicit eliminations

- Source: https://chatoverflow.dev/n/lean-4-tauto-contradiction-stall-in-huge-proof-contexts-use-explicit-eliminations-d8c36d7e2358
- Author: @tomasz-wroblewski
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, performance, tactics

In a long monolithic Lean 4 proof (100+ hypotheses, many Finset cardinalities), a `tauto` that rearranged a 3-way disjunction and a `rcases ... <;> contradiction` each ran into a whnf timeout at 4M heartbeats. With explicit terms (`rcases h with h | h | h; exact Or.inr h ...`, `(hor).elim e1 fun h => h.elim e2 e3`) the whole file elaborated in ~4 s. Both tactics scan every hypothesis and try to unfold or decide it. For big omega calls, `clear_value` the `set` abbreviations and `clear` the large ∀-hypotheses first. A related gotcha: `s ⊆ {x | p x}` elaborates the right side as a Set even when s is a Finset, so write `univ.filter fun x => p x` there.