pretty-printer for not equal

Game/Metadata.lean

@@ -13,6 +13,7 @@ import Game.Tactic.Rfl
 import Game.Tactic.Rw
 import Game.Tactic.Apply
 import Game.Tactic.Use
+import Game.Tactic.Ne
 import Game.Tactic.Xyzzy
 -- import Std.Tactic.RCases
 -- import Game.Tactic.Have

Game/Tactic/Ne.lean

@@ -0,0 +1,15 @@
+import Lean
+
+/-!
+A pretty-printer that displays `¬ (a = b)` as `a ≠ b`.
+-/
+
+open Lean PrettyPrinter Delaborator SubExpr
+
+@[delab app.Not] def delab_not_mem :=
+  whenPPOption Lean.getPPNotation do
+  let #[f] := (← SubExpr.getExpr).getAppArgs | failure
+  unless f.getAppFn matches .const `Eq _ do failure
+  let stx₁ ← SubExpr.withAppArg <| SubExpr.withNaryArg 1 delab
+  let stx₂ ← SubExpr.withAppArg <| SubExpr.withNaryArg 2 delab
+  return ← `($stx₁ ≠ $stx₂)

test/ne.lean

@@ -0,0 +1,14 @@
+import Game.Metadata
+
+example (a : ℕ) : a = 0 ∨ ¬ (a = 0) := by
+  by_cases h : a = 0
+  · left
+    exact h
+  · right
+    -- here the goal should show `h : a ≠ 0`
+    exact h
+
+-- set_option pp.all true in
+example (a : ℕ) : ¬ (a = 0) ↔ a ≠ 0 := by
+  -- both should be displayed the same way
+  rfl