chore: allow omega to use classicality, in case Decidable instances a…

…re too big (#4073)

From bug report at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/omega.20regression.20in.204.2E8.2E0-rc1/near/437150155

src/Lean/Elab/Tactic/Omega/Frontend.lean

@@ -666,7 +666,6 @@ open Lean Elab Tactic Parser.Tactic
 def omegaTactic (cfg : OmegaConfig) : TacticM Unit := do
   liftMetaFinishingTactic fun g => do
     let g ← g.falseOrByContra
-      (useClassical := false) -- because all the hypotheses we can make use of are decidable
     g.withContext do
       let hyps := (← getLocalHyps).toList
       trace[omega] "analyzing {hyps.length} hypotheses:\n{← hyps.mapM inferType}"

tests/lean/run/omega.lean

@@ -377,8 +377,12 @@ example (i j : Nat) (p : i ≥ j) : True := by
 -- From https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Nat.2Emul_sub_mod/near/428107094
 example (a b : Nat) (h : a % b + 1 = 0) : False := by omega
 
-/-! ### Fin -/
+-- From https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/omega.20regression.20in.204.2E8.2E0-rc1/near/437150155
+example (x : Nat) : x < 2 →
+    (0 = 0 → 0 = 0 → 0 = 0 → 0 = 0 → x < 2) ∧ (0 = 0 → 0 = 0 → 0 = 0 → 0 = 0 → x < 2 → x < 3) := by
+  omega
 
+/-! ### Fin -/
 
 -- Test `<`
 example (n : Nat) (i j : Fin n) (h : i < j) : (i : Nat) < n - 1 := by omega