diff --git a/src/Lean/Elab/Tactic/FalseOrByContra.lean b/src/Lean/Elab/Tactic/FalseOrByContra.lean
index 7a2601c96dde..e3967607cbbf 100644
--- a/src/Lean/Elab/Tactic/FalseOrByContra.lean
+++ b/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
diff --git a/tests/lean/run/omegaDischarger.lean b/tests/lean/run/omegaDischarger.lean
new file mode 100644
index 000000000000..0825d762ef36
--- /dev/null
+++ b/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]