From 280525f1fccbe2e08ef3032ac02af30ebdebf728 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Wed, 10 Apr 2024 10:46:07 +0200
Subject: [PATCH] fix: omega: ignore levels in canonicalizer (#3853)

fixes #3848
---
 src/Lean/Meta/Canonicalizer.lean |  4 +++-
 tests/lean/run/issue3848.lean    | 12 ++++++++++++
 2 files changed, 15 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/issue3848.lean

diff --git a/src/Lean/Meta/Canonicalizer.lean b/src/Lean/Meta/Canonicalizer.lean
index 707f5fbde5..bb71561092 100644
--- a/src/Lean/Meta/Canonicalizer.lean
+++ b/src/Lean/Meta/Canonicalizer.lean
@@ -82,8 +82,10 @@ private partial def mkKey (e : Expr) : CanonM Key := do
     return key
   else
     let key ← match e with
-      | .sort .. | .fvar .. | .bvar .. | .const .. | .lit .. =>
+      | .sort .. | .fvar .. | .bvar .. | .lit .. =>
         pure { e := (← shareCommon e) }
+      | .const n ls =>
+        pure { e := (← shareCommon (.const n (List.replicate ls.length levelZero))) }
       | .mvar .. =>
         -- We instantiate assigned metavariables because the
         -- pretty-printer also instantiates them.
diff --git a/tests/lean/run/issue3848.lean b/tests/lean/run/issue3848.lean
new file mode 100644
index 0000000000..c4f0b23423
--- /dev/null
+++ b/tests/lean/run/issue3848.lean
@@ -0,0 +1,12 @@
+theorem sizeOf_snd_lt_sizeOf_list
+  {α : Type u} {β : Type v} [SizeOf α] [SizeOf β] {x : α × β} {xs : List (α × β)} :
+  x ∈ xs → sizeOf x.snd < 1 + sizeOf xs
+:= by
+  intro h
+  have h1 := List.sizeOf_lt_of_mem h
+  have h2 : sizeOf x = 1 + sizeOf x.1 + sizeOf x.2 := rfl
+  cases x; dsimp at *
+  omega -- this only works if  universe levels are normalizes by the omega canonicalizier
+
+-- another example
+theorem ex.{u,v} : sizeOf PUnit.{(max u v) + 1} = sizeOf PUnit.{max (u + 1) (v + 1)} := by omega