Trigger CI for leanprover/lean4#2783

Mathlib.lean

@@ -3585,13 +3585,13 @@ import Mathlib.Util.AssertNoSorry
 import Mathlib.Util.AtomM
 import Mathlib.Util.CompileInductive
 import Mathlib.Util.CountHeartbeats
+import Mathlib.Util.Delaborators
 import Mathlib.Util.DischargerAsTactic
 import Mathlib.Util.Export
 import Mathlib.Util.Imports
 import Mathlib.Util.IncludeStr
 import Mathlib.Util.LongNames
 import Mathlib.Util.MemoFix
-import Mathlib.Util.PiNotation
 import Mathlib.Util.Qq
 import Mathlib.Util.SleepHeartbeats
 import Mathlib.Util.Superscript

Mathlib/Data/Set/Basic.lean

@@ -7,6 +7,7 @@ import Mathlib.Order.SymmDiff
 import Mathlib.Logic.Function.Iterate
 import Mathlib.Tactic.Tauto
 import Mathlib.Tactic.ByContra
+import Mathlib.Util.Delaborators
 
 #align_import data.set.basic from "leanprover-community/mathlib"@"001ffdc42920050657fd45bd2b8bfbec8eaaeb29"
 

Mathlib/Util/PiNotation.lean → Mathlib/Util/Delaborators.lean

@@ -23,7 +23,7 @@ also be written as `(x : α) → β x`. -/
 -- A direct copy of forall notation but with `Π`/`Pi` instead of `∀`/`Forall`.
 @[term_parser]
 def piNotation := leading_parser:leadPrec
-  unicodeSymbol "Π" "Pi" >>
+  unicodeSymbol "Π" "PiType" >>
   many1 (ppSpace >> (binderIdent <|> bracketedBinder)) >>
   optType >> ", " >> termParser
 
@@ -60,6 +60,16 @@ def delabPi : Delab := whenPPOption Lean.getPPNotation do
     if x == y then `(∀ $x:ident ≤ $z, $body) else pure stx
   | `(Π ($i:ident : $_), $j:ident ∈ $s → $body) =>
     if i == j then `(Π $i:ident ∈ $s, $body) else pure stx
+  | `(∀ ($i:ident : $_), $j:ident ∉ $s → $body) =>
+    if i == j then `(∀ $i:ident ∉ $s, $body) else pure stx
+  | `(∀ ($i:ident : $_), $j:ident ⊆ $s → $body) =>
+    if i == j then `(∀ $i:ident ⊆ $s, $body) else pure stx
+  | `(∀ ($i:ident : $_), $j:ident ⊂ $s → $body) =>
+    if i == j then `(∀ $i:ident ⊂ $s, $body) else pure stx
+  | `(∀ ($i:ident : $_), $j:ident ⊇ $s → $body) =>
+    if i == j then `(∀ $i:ident ⊇ $s, $body) else pure stx
+  | `(∀ ($i:ident : $_), $j:ident ⊃ $s → $body) =>
+    if i == j then `(∀ $i:ident ⊃ $s, $body) else pure stx
   | _ => pure stx
 
 /-- Override the Lean 4 pi notation delaborator with one that uses `Π` and prints
@@ -122,9 +132,34 @@ def exists_delab : Delab := whenPPOption Lean.getPPNotation do
     | `(∃ $x:ident, $y:ident ≤ $z ∧ $body)
     | `(∃ ($x:ident : $_), $y:ident ≤ $z ∧ $body) =>
       if x == y then `(∃ $x:ident ≤ $z, $body) else pure stx
+    | `(∃ $x:ident, $y:ident ∉ $z ∧ $body)
+    | `(∃ ($x:ident : $_), $y:ident ∉ $z ∧ $body) => do
+      if x == y then `(∃ $x:ident ∉ $z, $body) else pure stx
+    | `(∃ $x:ident, $y:ident ⊆ $z ∧ $body)
+    | `(∃ ($x:ident : $_), $y:ident ⊆ $z ∧ $body) =>
+      if x == y then `(∃ $x:ident ⊆ $z, $body) else pure stx
+    | `(∃ $x:ident, $y:ident ⊂ $z ∧ $body)
+    | `(∃ ($x:ident : $_), $y:ident ⊂ $z ∧ $body) =>
+      if x == y then `(∃ $x:ident ⊂ $z, $body) else pure stx
+    | `(∃ $x:ident, $y:ident ⊇ $z ∧ $body)
+    | `(∃ ($x:ident : $_), $y:ident ⊇ $z ∧ $body) =>
+      if x == y then `(∃ $x:ident ⊇ $z, $body) else pure stx
+    | `(∃ $x:ident, $y:ident ⊃ $z ∧ $body)
+    | `(∃ ($x:ident : $_), $y:ident ⊃ $z ∧ $body) =>
+      if x == y then `(∃ $x:ident ⊃ $z, $body) else pure stx
     | _ => pure stx
-  -- Merging
   match stx with
   | `(∃ $group:bracketedExplicitBinders, ∃ $groups*, $body) => `(∃ $group $groups*, $body)
+  | `(∃ $b:binderIdent, ∃ $[$bs:binderIdent]*, $body) => `(∃ $b:binderIdent $[$bs]*, $body)
   | _ => pure stx
 end existential
+
+open Lean Lean.PrettyPrinter.Delaborator
+
+/-- Delaborator for `∉`. -/
+@[delab app.Not] def delab_not_in := whenPPOption Lean.getPPNotation do
+  let #[f] := (← SubExpr.getExpr).getAppArgs | failure
+  guard <| f.isAppOfArity ``Membership.mem 5
+  let stx₁ ← SubExpr.withAppArg <| SubExpr.withNaryArg 3 delab
+  let stx₂ ← SubExpr.withAppArg <| SubExpr.withNaryArg 4 delab
+  return ← `($stx₁ ∉ $stx₂)

test/delaborators.lean

@@ -1,5 +1,5 @@
 import Std.Tactic.GuardMsgs
-import Mathlib.Util.PiNotation
+import Mathlib.Util.Delaborators
 import Mathlib.Data.Set.Lattice
 
 section PiNotation
@@ -45,6 +45,48 @@ variable (P : Nat → Prop) (α : Nat → Type) (s : Set ℕ)
 #guard_msgs in
 #check ∀ x, x ∈ s → P x
 
+/-- info: ∀ x ∉ s, P x : Prop -/
+#guard_msgs in
+#check ∀ x ∉ s,P x
+
+/-- info: ∀ x ∉ s, P x : Prop -/
+#guard_msgs in
+#check ∀ x, x ∉ s → P x
+
+variable (Q : Set ℕ → Prop)
+
+/-- info: ∀ t ⊆ s, Q t : Prop -/
+#guard_msgs in
+#check ∀ t ⊆ s, Q t
+
+/-- info: ∀ t ⊆ s, Q t : Prop -/
+#guard_msgs in
+#check ∀ t, t ⊆ s → Q t
+
+/-- info: ∀ t ⊂ s, Q t : Prop -/
+#guard_msgs in
+#check ∀ t ⊂ s, Q t
+
+/-- info: ∀ t ⊂ s, Q t : Prop -/
+#guard_msgs in
+#check ∀ t, t ⊂ s → Q t
+
+/-- info: ∀ t ⊇ s, Q t : Prop -/
+#guard_msgs in
+#check ∀ t ⊇ s, Q t
+
+/-- info: ∀ t ⊇ s, Q t : Prop -/
+#guard_msgs in
+#check ∀ t, t ⊇ s → Q t
+
+/-- info: ∀ t ⊃ s, Q t : Prop -/
+#guard_msgs in
+#check ∀ t ⊃ s, Q t
+
+/-- info: ∀ t ⊃ s, Q t : Prop -/
+#guard_msgs in
+#check ∀ t, t ⊃ s → Q t
+
 /-- info: (x : ℕ) → α x : Type -/
 #guard_msgs in
 #check (x : Nat) → α x
@@ -103,6 +145,58 @@ section existential
 #guard_msgs in
 #check ∃ (i : Nat), i < 3 ∧ i = i
 
+variable (s : Set ℕ) (P : ℕ → Prop) (Q : Set ℕ → Prop)
+
+/-- info: ∃ x ∉ s, P x : Prop -/
+#guard_msgs in
+#check ∃ x ∉ s, P x
+
+/-- info: ∃ x ∉ s, P x : Prop -/
+#guard_msgs in
+#check ∃ x, x ∉ s ∧ P x
+
+variable (Q : Set ℕ → Prop)
+
+/-- info: ∃ t ⊆ s, Q t : Prop -/
+#guard_msgs in
+#check ∃ t ⊆ s, Q t
+
+/-- info: ∃ t ⊆ s, Q t : Prop -/
+#guard_msgs in
+#check ∃ t, t ⊆ s ∧ Q t
+
+/-- info: ∃ t ⊂ s, Q t : Prop -/
+#guard_msgs in
+#check ∃ t ⊂ s, Q t
+
+/-- info: ∃ t ⊂ s, Q t : Prop -/
+#guard_msgs in
+#check ∃ t, t ⊂ s ∧ Q t
+
+/-- info: ∃ t ⊇ s, Q t : Prop -/
+#guard_msgs in
+#check ∃ t ⊇ s, Q t
+
+/-- info: ∃ t ⊇ s, Q t : Prop -/
+#guard_msgs in
+#check ∃ t, t ⊇ s ∧ Q t
+
+/-- info: ∃ t ⊃ s, Q t : Prop -/
+#guard_msgs in
+#check ∃ t ⊃ s, Q t
+
+/-- info: ∃ t ⊃ s, Q t : Prop -/
+#guard_msgs in
+#check ∃ t, t ⊃ s ∧ Q t
+
+/-- info: ∃ n k, n = k : Prop -/
+#guard_msgs in
+#check ∃ n k, n = k
+
+/-- info: ∃ n k, n = k : Prop -/
+#guard_msgs in
+#check ∃ n, ∃ k, n = k
+
 end existential
 
 section prod

test/propose.lean

@@ -57,7 +57,7 @@ example (p : Nat × String) : True := by
 /--
 info: Try this: have : List.Disjoint M L := List.disjoint_symm w
 ---
-info: Try this: have : ¬a ∈ M := foo L M w m
+info: Try this: have : a ∉ M := foo L M w m
 -/
 #guard_msgs in
 example (K L M : List α) (w : L.Disjoint M) (m : a ∈ L) : True := by