import all

RELEASES.md

@@ -8,15 +8,10 @@ This file contains work-in-progress notes for the upcoming release, as well as p
 Please check the [releases](https://github.com/leanprover/lean4/releases) page for the current status
 of each version.
 
-v4.16.0
-----------
-
-Development in progress.
-
 v4.15.0
 ----------
 
-Release candidate, release notes will be copied from the branch `releases/v4.15.0` once completed.
+Development in progress.
 
 v4.14.0
 ----------
@@ -93,7 +88,7 @@ v4.13.0
   * [#4768](https://github.com/leanprover/lean4/pull/4768) fixes a parse error when `..` appears with a `.` on the next line
 
 * Metaprogramming
-  * [#3090](https://github.com/leanprover/lean4/pull/3090) handles level parameters in `Meta.evalExpr` (@eric-wieser)
+  * [#3090](https://github.com/leanprover/lean4/pull/3090) handles level parameters in `Meta.evalExpr` (@eric-wieser)  
   * [#5401](https://github.com/leanprover/lean4/pull/5401) instance for `Inhabited (TacticM α)` (@alexkeizer)
   * [#5412](https://github.com/leanprover/lean4/pull/5412) expose Kernel.check for debugging purposes
   * [#5556](https://github.com/leanprover/lean4/pull/5556) improves the "invalid projection" type inference error in `inferType`.

debug.log

@@ -0,0 +1 @@
+[0829/202002.254:ERROR:crashpad_client_win.cc(868)] not connected

script/mathlib-bench

@@ -1,12 +0,0 @@
-#! /bin/env bash
-# Open a Mathlib4 PR for benchmarking a given Lean 4 PR
-
-set -euo pipefail
-
-[ $# -eq 1 ] || (echo "usage: $0 <lean4 PR #>"; exit 1)
-
-LEAN_PR=$1
-PR_RESPONSE=$(gh api repos/leanprover-community/mathlib4/pulls -X POST -f head=lean-pr-testing-$LEAN_PR -f base=nightly-testing -f title="leanprover/lean4#$LEAN_PR benchmarking" -f draft=true -f body="ignore me")
-PR_NUMBER=$(echo "$PR_RESPONSE" | jq '.number')
-echo "opened https://github.com/leanprover-community/mathlib4/pull/$PR_NUMBER"
-gh api repos/leanprover-community/mathlib4/issues/$PR_NUMBER/comments -X POST -f body="!bench" > /dev/null

src/CMakeLists.txt

@@ -10,7 +10,7 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
-set(LEAN_VERSION_MINOR 16)
+set(LEAN_VERSION_MINOR 15)
 set(LEAN_VERSION_PATCH 0)
 set(LEAN_VERSION_IS_RELEASE 0)  # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")

src/Init/Data/Array/Lemmas.lean

@@ -59,14 +59,6 @@ namespace List
 
 open Array
 
-theorem toArray_inj {a b : List α} (h : a.toArray = b.toArray) : a = b := by
-  cases a with
-  | nil => simpa using h
-  | cons a as =>
-    cases b with
-    | nil => simp at h
-    | cons b bs => simpa using h
-
 @[simp] theorem size_toArrayAux {a : List α} {b : Array α} :
     (a.toArrayAux b).size = b.size + a.length := by
   simp [size]
@@ -404,11 +396,6 @@ namespace Array
 
 /-! ## Preliminaries -/
 
-/-! ### toList -/
-
-theorem toList_inj {a b : Array α} (h : a.toList = b.toList) : a = b := by
-  cases a; cases b; simpa using h
-
 /-! ### empty -/
 
 @[simp] theorem empty_eq {xs : Array α} : #[] = xs ↔ xs = #[] := by

src/Init/Data/UInt/Bitwise.lean

@@ -1,39 +1,25 @@
 /-
 Copyright (c) 2024 Lean FRO, LLC. All Rights Reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel, Mac Malone
+Authors: Markus Himmel
 -/
 prelude
-import Init.Data.UInt.Lemmas
+import Init.Data.UInt.Basic
 import Init.Data.Fin.Bitwise
 import Init.Data.BitVec.Lemmas
 
 set_option hygiene false in
-macro "declare_bitwise_uint_theorems" typeName:ident bits:term:arg : command =>
+macro "declare_bitwise_uint_theorems" typeName:ident : command =>
 `(
 namespace $typeName
 
-@[simp] protected theorem toBitVec_and (a b : $typeName) : (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec := rfl
-@[simp] protected theorem toBitVec_or (a b : $typeName) : (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec := rfl
-@[simp] protected theorem toBitVec_xor (a b : $typeName) : (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec := rfl
-@[simp] protected theorem toBitVec_shiftLeft (a b : $typeName) : (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % $bits) := rfl
-@[simp] protected theorem toBitVec_shiftRight (a b : $typeName) : (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % $bits) := rfl
-
-@[simp] protected theorem toNat_and (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.toNat := by simp [toNat]
-@[simp] protected theorem toNat_or (a b : $typeName) : (a ||| b).toNat = a.toNat ||| b.toNat := by simp [toNat]
-@[simp] protected theorem toNat_xor (a b : $typeName) : (a ^^^ b).toNat = a.toNat ^^^ b.toNat := by simp [toNat]
-@[simp] protected theorem toNat_shiftLeft (a b : $typeName) : (a <<< b).toNat = a.toNat <<< (b.toNat % $bits) % 2 ^ $bits := by simp [toNat]
-@[simp] protected theorem toNat_shiftRight (a b : $typeName) : (a >>> b).toNat = a.toNat >>> (b.toNat % $bits) := by simp [toNat]
-
-open $typeName (toNat_and) in
-@[deprecated toNat_and (since := "2024-11-28")]
-protected theorem and_toNat (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.toNat := BitVec.toNat_and ..
+@[simp] protected theorem and_toNat (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.toNat := BitVec.toNat_and ..
 
 end $typeName
 )
 
-declare_bitwise_uint_theorems UInt8 8
-declare_bitwise_uint_theorems UInt16 16
-declare_bitwise_uint_theorems UInt32 32
-declare_bitwise_uint_theorems UInt64 64
-declare_bitwise_uint_theorems USize System.Platform.numBits
+declare_bitwise_uint_theorems UInt8
+declare_bitwise_uint_theorems UInt16
+declare_bitwise_uint_theorems UInt32
+declare_bitwise_uint_theorems UInt64
+declare_bitwise_uint_theorems USize

src/Init/Data/Vector/Lemmas.lean

@@ -11,15 +11,6 @@ import Init.Data.Vector.Basic
 Lemmas about `Vector α n`
 -/
 
-namespace Array
-
-theorem toVector_inj {a b : Array α} (h₁ : a.size = b.size) (h₂ : a.toVector.cast h₁ = b.toVector) : a = b := by
-  ext i ih₁ ih₂
-  · exact h₁
-  · simpa using congrArg (fun a => a[i]) h₂
-
-end Array
-
 namespace Vector
 
 @[simp] theorem getElem_mk {data : Array α} {size : data.size = n} {i : Nat} (h : i < n) :
@@ -248,11 +239,6 @@ theorem length_toList {α n} (xs : Vector α n) : xs.toList.length = n := by sim
 theorem getElem_toList {α n} (xs : Vector α n) (i : Nat) (h : i < xs.toList.length) :
     xs.toList[i] = xs[i]'(by simpa using h) := by simp
 
-theorem toList_inj {a b : Vector α n} (h : a.toList = b.toList) : a = b := by
-  rcases a with ⟨⟨a⟩, ha⟩
-  rcases b with ⟨⟨b⟩, hb⟩
-  simpa using h
-
 /-! ### Decidable quantifiers. -/
 
 theorem forall_zero_iff {P : Vector α 0 → Prop} :

src/Lean/Elab/Tactic/Omega/Frontend.lean

@@ -228,7 +228,6 @@ partial def asLinearComboImpl (e : Expr) : OmegaM (LinearCombo × OmegaM Expr ×
     | .app (.app (.app (.app (.const ``Prod.mk [u, v]) _) _) x) y =>
       rewrite e (mkApp4 (.const ``Prod.snd_mk [u, v]) α x β y)
     | _ => mkAtomLinearCombo e
-  | (``Int.negSucc, #[n]) => rewrite e (mkApp (.const ``Int.negSucc_eq []) n)
   | _ => mkAtomLinearCombo e
 where
   /--

src/Lean/Linter/Deprecated.lean

@@ -51,8 +51,8 @@ def checkDeprecated [Monad m] [MonadEnv m] [MonadLog m] [AddMessageContext m] [M
   if getLinterValue linter.deprecated (← getOptions) then
     let some attr := deprecatedAttr.getParam? (← getEnv) declName | pure ()
     logWarning <| .tagged ``deprecatedAttr <|
-      m!"`{.ofConstName declName true}` has been deprecated" ++ match attr.text? with
+      s!"`{declName}` has been deprecated" ++ match attr.text? with
       | some text => s!": {text}"
       | none => match attr.newName? with
-        | some newName => m!": use `{.ofConstName newName true}` instead"
+        | some newName => s!": use `{newName}` instead"
         | none => ""

src/Lean/Meta/CtorRecognizer.lean

@@ -35,27 +35,11 @@ def isConstructorApp? (e : Expr) : MetaM (Option ConstructorVal) := do
 
 /--
 Similar to `isConstructorApp?`, but uses `whnf`.
-It also uses `isOffset?` for `Nat`.
-
-See also `Lean.Meta.constructorApp'?`.
 -/
 def isConstructorApp'? (e : Expr) : MetaM (Option ConstructorVal) := do
-  if let some (_, k) ← isOffset? e then
-    if k = 0 then
-      return none
-    else
-      let .ctorInfo val ← getConstInfo ``Nat.succ | return none
-      return some val
-  else if let some r ← isConstructorApp? e then
+  if let some r ← isConstructorApp? e then
     return r
-  else try
-    /-
-    We added the `try` block here because `whnf` fails at terms `n ^ m`
-    when `m` is a big numeral, and `n` is a numeral. This is a little bit hackish.
-    -/
-    isConstructorApp? (← whnf e)
-  catch _ =>
-    return none
+  isConstructorApp? (← whnf e)
 
 /--
 Returns `true`, if `e` is constructor application of builtin literal defeq to
@@ -86,9 +70,7 @@ def constructorApp? (e : Expr) : MetaM (Option (ConstructorVal × Array Expr)) :
 
 /--
 Similar to `constructorApp?`, but on failure it puts `e` in WHNF and tries again.
-It also uses `isOffset?` for `Nat`.
-
-See also `Lean.Meta.isConstructorApp'?`.
+It also `isOffset?`
 -/
 def constructorApp'? (e : Expr) : MetaM (Option (ConstructorVal × Array Expr)) := do
   if let some (e, k) ← isOffset? e then

src/Lean/Server/Completion/SyntheticCompletion.lean

@@ -100,6 +100,20 @@ private def findSyntheticIdentifierCompletion?
       HoverInfo.after
   some { hoverInfo, ctx, info := .id stx id danglingDot info.lctx none }
 
+private partial def getIndentationAmount (fileMap : FileMap) (line : Nat) : Nat := Id.run do
+  let lineStartPos := fileMap.lineStart line
+  let lineEndPos := fileMap.lineStart (line + 1)
+  let mut it : String.Iterator := ⟨fileMap.source, lineStartPos⟩
+  let mut indentationAmount := 0
+  while it.pos < lineEndPos do
+    let c := it.curr
+    if c = ' ' || c = '\t' then
+      indentationAmount := indentationAmount + 1
+    else
+      break
+    it := it.next
+  return indentationAmount
+
 private partial def isCursorOnWhitespace (fileMap : FileMap) (hoverPos : String.Pos) : Bool :=
   fileMap.source.atEnd hoverPos || (fileMap.source.get hoverPos).isWhitespace
 
@@ -113,10 +127,15 @@ private partial def isSyntheticTacticCompletion
     (cmdStx   : Syntax)
     : Bool := Id.run do
   let hoverFilePos := fileMap.toPosition hoverPos
-  go hoverFilePos cmdStx 0
+  let mut hoverLineIndentation := getIndentationAmount fileMap hoverFilePos.line
+  if hoverFilePos.column < hoverLineIndentation then
+    -- Ignore trailing whitespace after the cursor
+    hoverLineIndentation := hoverFilePos.column
+  go hoverFilePos hoverLineIndentation cmdStx 0
 where
   go
       (hoverFilePos : Position)
+      (hoverLineIndentation : Nat)
       (stx : Syntax)
       (leadingWs : Nat)
       : Bool := Id.run do
@@ -129,7 +148,7 @@ where
         return false
       let mut wsBeforeArg := leadingWs
       for arg in stx.getArgs do
-        if go hoverFilePos arg wsBeforeArg then
+        if go hoverFilePos hoverLineIndentation arg wsBeforeArg then
           return true
         -- We must account for the whitespace before an argument because the syntax nodes we use
         -- to identify tactic blocks only start *after* the whitespace following a `by`, and we
@@ -139,7 +158,7 @@ where
         wsBeforeArg := arg.getTrailingSize
       return isCompletionInEmptyTacticBlock stx
         || isCompletionAfterSemicolon stx
-        || isCompletionOnTacticBlockIndentation hoverFilePos stx
+        || isCompletionOnTacticBlockIndentation hoverFilePos hoverLineIndentation stx
     | _, _ =>
       -- Empty tactic blocks typically lack ranges since they do not contain any tokens.
       -- We do not perform more precise range checking in this case because we assume that empty
@@ -150,17 +169,24 @@ where
 
   isCompletionOnTacticBlockIndentation
       (hoverFilePos : Position)
+      (hoverLineIndentation : Nat)
       (stx : Syntax)
       : Bool := Id.run do
+    let isCursorInIndentation := hoverFilePos.column <= hoverLineIndentation
+    if ! isCursorInIndentation then
+      -- Do not trigger tactic completion at the end of a properly indented tactic block line since
+      -- that line might already have entered term mode by that point.
+      return false
     let some tacticsNode := getTacticsNode? stx
       | return false
     let some firstTacticPos := tacticsNode.getPos?
       | return false
-    let firstTacticColumn := fileMap.toPosition firstTacticPos |>.column
+    let firstTacticLine := fileMap.toPosition firstTacticPos |>.line
+    let firstTacticIndentation := getIndentationAmount fileMap firstTacticLine
     -- This ensures that we do not accidentally provide tactic completions in a term mode proof -
     -- tactic completions are only provided at the same indentation level as the other tactics in
     -- that tactic block.
-    let isCursorInTacticBlock := hoverFilePos.column == firstTacticColumn
+    let isCursorInTacticBlock := hoverLineIndentation == firstTacticIndentation
     return isCursorInProperWhitespace fileMap hoverPos && isCursorInTacticBlock
 
   isCompletionAfterSemicolon (stx : Syntax) : Bool := Id.run do
@@ -289,6 +315,10 @@ private def isSyntheticStructFieldCompletion
     return false
 
   let hoverFilePos := fileMap.toPosition hoverPos
+  let mut hoverLineIndentation := getIndentationAmount fileMap hoverFilePos.line
+  if hoverFilePos.column < hoverLineIndentation then
+    -- Ignore trailing whitespace after the cursor
+    hoverLineIndentation := hoverFilePos.column
 
   return Option.isSome <| findWithLeadingToken? (stx := cmdStx) fun leadingToken? stx => Id.run do
     let some leadingToken := leadingToken?
@@ -325,10 +355,14 @@ private def isSyntheticStructFieldCompletion
     let isCompletionOnIndentation := Id.run do
       if ! isCursorInProperWhitespace then
         return false
+      let isCursorInIndentation := hoverFilePos.column <= hoverLineIndentation
+      if ! isCursorInIndentation then
+        return false
       let some firstFieldPos := stx.getPos?
         | return false
-      let firstFieldColumn := fileMap.toPosition firstFieldPos |>.column
-      let isCursorInBlock := hoverFilePos.column == firstFieldColumn
+      let firstFieldLine := fileMap.toPosition firstFieldPos |>.line
+      let firstFieldIndentation := getIndentationAmount fileMap firstFieldLine
+      let isCursorInBlock := hoverLineIndentation == firstFieldIndentation
       return isCursorInBlock
     return isCompletionOnIndentation
 

src/Std/Data/DHashMap/Internal/Index.lean

@@ -46,11 +46,19 @@ cf. https://github.com/leanprover/lean4/issues/4157
 @[irreducible, inline] def mkIdx (sz : Nat) (h : 0 < sz) (hash : UInt64) :
     { u : USize // u.toNat < sz } :=
   ⟨(scrambleHash hash).toUSize &&& (sz.toUSize - 1), by
-    -- This proof is a good test for our USize API
+    -- Making this proof significantly less painful will be a good test for our USize API
     by_cases h' : sz < USize.size
-    · rw [USize.toNat_and, USize.toNat_sub_of_le, USize.toNat_ofNat_of_lt h']
-      · exact Nat.lt_of_le_of_lt Nat.and_le_right (Nat.sub_lt h (by simp))
-      · simp [USize.le_iff_toNat_le, Nat.mod_eq_of_lt h', Nat.succ_le_of_lt h]
+    · rw [USize.and_toNat, ← USize.ofNat_one, USize.toNat_sub_of_le, USize.toNat_ofNat_of_lt]
+      · refine Nat.lt_of_le_of_lt Nat.and_le_right (Nat.sub_lt h ?_)
+        rw [USize.toNat_ofNat_of_lt]
+        · exact Nat.one_pos
+        · exact Nat.lt_of_le_of_lt h h'
+      · exact h'
+      · rw [USize.le_def, BitVec.le_def]
+        change _ ≤ (_ % _)
+        rw [Nat.mod_eq_of_lt h', USize.ofNat, BitVec.toNat_ofNat, Nat.mod_eq_of_lt]
+        · exact h
+        · exact Nat.lt_of_le_of_lt h h'
     · exact Nat.lt_of_lt_of_le (USize.toNat_lt_size _) (Nat.le_of_not_lt h')⟩
 
 end Std.DHashMap.Internal

tests/lean/interactive/completionStructureInstance.lean

@@ -74,11 +74,11 @@ example : S := {
 --^ textDocument/completion
 }
 
-example : S :=
-  { foo := 1
-     } -- All field completions expected
-  --^ textDocument/completion
-
+example : S := {
+  foo := 1
+    -- All field completions expected
+--^ textDocument/completion
+}
 
 example : S := { foo := 1,  } -- All field completions expected
                          --^ textDocument/completion

tests/lean/interactive/completionStructureInstance.lean.expected.out

@@ -416,7 +416,7 @@
     "cPos": 0}}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file:///completionStructureInstance.lean"},
- "position": {"line": 78, "character": 4}}
+ "position": {"line": 78, "character": 2}}
 {"items":
  [{"sortText": "0",
    "label": "bar",
@@ -425,7 +425,7 @@
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionStructureInstance.lean"},
-     "position": {"line": 78, "character": 4}},
+     "position": {"line": 78, "character": 2}},
     "cPos": 0}},
   {"sortText": "1",
    "label": "barfoo",
@@ -434,7 +434,7 @@
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionStructureInstance.lean"},
-     "position": {"line": 78, "character": 4}},
+     "position": {"line": 78, "character": 2}},
     "cPos": 0}},
   {"sortText": "2",
    "label": "foo",
@@ -443,7 +443,7 @@
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionStructureInstance.lean"},
-     "position": {"line": 78, "character": 4}},
+     "position": {"line": 78, "character": 2}},
     "cPos": 0}},
   {"sortText": "3",
    "label": "foobar",
@@ -452,7 +452,7 @@
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionStructureInstance.lean"},
-     "position": {"line": 78, "character": 4}},
+     "position": {"line": 78, "character": 2}},
     "cPos": 0}}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file:///completionStructureInstance.lean"},

tests/lean/interactive/completionTactics.lean

@@ -113,8 +113,3 @@ example : True := by {
     -- All tactic completions expected
 --^ textDocument/completion
 }
-
-example : True := by
-  { skip -- All tactic completions expected
-     }
-  --^ textDocument/completion

tests/lean/interactive/completionTactics.lean.expected.out

@@ -1472,89 +1472,3 @@
      "position": {"line": 112, "character": 2}},
     "cPos": 0}}],
  "isIncomplete": true}
-{"textDocument": {"uri": "file:///completionTactics.lean"},
- "position": {"line": 118, "character": 4}}
-{"items":
- [{"sortText": "0",
-   "label": "exact",
-   "kind": 14,
-   "documentation": {"value": "Another docstring ", "kind": "markdown"},
-   "data":
-   {"params":
-    {"textDocument": {"uri": "file:///completionTactics.lean"},
-     "position": {"line": 118, "character": 4}},
-    "cPos": 0}},
-  {"sortText": "1",
-   "label": "Lean.Parser.Tactic.introMatch",
-   "kind": 14,
-   "documentation":
-   {"value":
-    "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-    "kind": "markdown"},
-   "data":
-   {"params":
-    {"textDocument": {"uri": "file:///completionTactics.lean"},
-     "position": {"line": 118, "character": 4}},
-    "cPos": 0}},
-  {"sortText": "2",
-   "label": "Lean.Parser.Tactic.match",
-   "kind": 14,
-   "documentation":
-   {"value":
-    "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
-    "kind": "markdown"},
-   "data":
-   {"params":
-    {"textDocument": {"uri": "file:///completionTactics.lean"},
-     "position": {"line": 118, "character": 4}},
-    "cPos": 0}},
-  {"sortText": "3",
-   "label": "Lean.Parser.Tactic.nestedTactic",
-   "kind": 14,
-   "data":
-   {"params":
-    {"textDocument": {"uri": "file:///completionTactics.lean"},
-     "position": {"line": 118, "character": 4}},
-    "cPos": 0}},
-  {"sortText": "4",
-   "label": "Lean.Parser.Tactic.open",
-   "kind": 14,
-   "documentation":
-   {"value":
-    "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
-    "kind": "markdown"},
-   "data":
-   {"params":
-    {"textDocument": {"uri": "file:///completionTactics.lean"},
-     "position": {"line": 118, "character": 4}},
-    "cPos": 0}},
-  {"sortText": "5",
-   "label": "Lean.Parser.Tactic.set_option",
-   "kind": 14,
-   "documentation":
-   {"value":
-    "`set_option opt val in tacs` (the tactic) acts like `set_option opt val` at the command level,\nbut it sets the option only within the tactics `tacs`. ",
-    "kind": "markdown"},
-   "data":
-   {"params":
-    {"textDocument": {"uri": "file:///completionTactics.lean"},
-     "position": {"line": 118, "character": 4}},
-    "cPos": 0}},
-  {"sortText": "6",
-   "label": "Lean.Parser.Tactic.unknown",
-   "kind": 14,
-   "data":
-   {"params":
-    {"textDocument": {"uri": "file:///completionTactics.lean"},
-     "position": {"line": 118, "character": 4}},
-    "cPos": 0}},
-  {"sortText": "7",
-   "label": "skip",
-   "kind": 14,
-   "documentation": {"value": "A docstring ", "kind": "markdown"},
-   "data":
-   {"params":
-    {"textDocument": {"uri": "file:///completionTactics.lean"},
-     "position": {"line": 118, "character": 4}},
-    "cPos": 0}}],
- "isIncomplete": true}

tests/lean/run/5064.lean

@@ -1,27 +0,0 @@
-/-!
-# Make sure `injection` tactic can handle `0 = n + 1`
-https://github.com/leanprover/lean4/issues/5064
--/
-
-/-!
-Motivating example from #5064.
-This failed when generating the splitter theorem for `thingy`.
--/
-
-def thingy : List (Nat ⊕ Nat) → List Bool
-  | Sum.inr (_n + 2) :: l => thingy l
-  | _ => []
-  termination_by l => l.length
-
-/-- info: ⊢ [] = [] -/
-#guard_msgs in
-theorem thingy_empty : thingy [] = [] := by
-  unfold thingy
-  trace_state
-  rfl
-
-/-!
-Test using `injection` directly.
--/
-example (n : Nat) (h : 0 = n + 1) : False := by
-  with_reducible injection h

tests/lean/run/omega.lean

@@ -466,12 +466,6 @@ example (z : Int) : z.toNat = 0 ↔ z ≤ 0 := by
 example (z : Int) (a : Fin z.toNat) (h : 0 ≤ z) : ↑↑a ≤ z := by
   omega
 
-/-! ### Int.negSucc
-Make sure we aren't stopped by stray `Int.negSucc` terms.
--/
-
-example (x : Int) (h : Int.negSucc 0 < x ∧ x < 1) : x = 0 := by omega
-
 /-! ### BitVec -/
 open BitVec