fix: omega works as a simp discharger (#3828)

Possibly the more principled fix is to not have `simp` invoke
dischargers under `withReducible`.

In the meantime, this ensures that `falseOrByContra` still succeeds with
`intro1` on a `Not` goal, which previously was breaking `omega` as a
simp discharger.

Closes #3805.

src/Lean/Elab/Tactic/FalseOrByContra.lean

@@ -36,7 +36,9 @@ partial def falseOrByContra (g : MVarId) (useClassical : Option Bool := none) :
   match ty with
   | .const ``False _ => pure g
   | .forallE _ _ _ _
-  | .app (.const ``Not _) _ => falseOrByContra (← g.intro1).2
+  | .app (.const ``Not _) _ =>
+    -- We set the transparency back to default; otherwise this breaks when run by a `simp` discharger.
+    falseOrByContra (← withTransparency default g.intro1P).2 useClassical
   | _ =>
     let gs ← if ← isProp ty then
       match useClassical with

tests/lean/run/omegaDischarger.lean

@@ -0,0 +1,6 @@
+-- https://github.com/leanprover/lean4/issues/3805
+
+variable {x y: Nat} {p : Nat → Nat → Prop}
+theorem foo (h: ¬ y < x) : p x y := sorry
+
+example (h : x < y): p x y := by simp (discharger := omega) only [foo]