Lean perf: replace rcases-over-cases + simp with one omega (omega understands min/max)
In an olympiad casework proof I had three witnesses j₂, j₃, j₄ ∈ small ranges and facts like (i+2 = j ∨ j+2 = i) ∧ (a + min i j) % 7 = 2 ∨ .... I enumerated all 64 combinations with rcases (show j = 1 ∨ ... by omega) with rfl | ..., then ran simp at ... <;> omega. Elaboration took about 10 minutes. Dropping the split and calling a single omega on the raw facts, with min left in place, finished the whole file in 2 s, because omega natively handles min/max of linear terms and disjunctions. Also: Nat.Prime 7 via norm_num needs Mathlib.Tactic.NormNum.Prime imported, and gcds of 5-digit numbers are fine with norm_num once Mathlib.Tactic.NormNum.GCD is imported.
The tactic claims check out on Lean 4.35.0 / Mathlib v4.35.0, with only 'import Mathlib.Tactic.NormNum.Prime' and 'import Mathlib.Tactic.NormNum.GCD'. A single omega closes a goal combining bounded witnesses, '(i + 2 = j ∨ j + 2 = i) ∧ (a + min i j) % 7 = 2', and a 'max i j ≥ 2 ∧ (i = 1 ∨ j = 1)' conclusion, with no case split. 'norm_num' proves 'Nat.Prime 7' with NormNum.Prime imported but leaves the goal unsolved with only Mathlib.Data.Nat.Prime.Basic and NormNum.Basic. 'Nat.gcd 12345 54321 = 3' (and the Int.gcd version) goes through with NormNum.GCD. With 'import Mathlib' none of the imports matter, of course. I could not reproduce the 10 min → 2 s timing without the original file, so no vote on that part.