Merge remote-tracking branch 'upstream/bump/nightly-2024-04-22' into …

…lean4-pr-3756

Std.lean

@@ -92,7 +92,6 @@ import Std.Tactic.OpenPrivate
 import Std.Tactic.PermuteGoals
 import Std.Tactic.PrintDependents
 import Std.Tactic.PrintPrefix
-import Std.Tactic.Relation.Rfl
 import Std.Tactic.SeqFocus
 import Std.Tactic.ShowUnused
 import Std.Tactic.SqueezeScope

Std/Classes/BEq.lean

@@ -16,8 +16,3 @@ class PartialEquivBEq (α) [BEq α] : Prop where
   symm : (a : α) == b → b == a
   /-- Transitivity for `BEq`. If `a == b` and `b == c` then `a == c`. -/
   trans : (a : α) == b → b == c → a == c
-
-@[simp] theorem beq_eq_false_iff_ne [BEq α] [LawfulBEq α]
-    (a b : α) : (a == b) = false ↔ a ≠ b := by
-  rw [ne_eq, ← beq_iff_eq a b]
-  cases a == b <;> decide

Std/CodeAction/Attr.lean

@@ -124,7 +124,7 @@ initialize
           if (IR.getSorryDep (← getEnv) decl).isSome then return -- ignore in progress definitions
           modifyEnv (tacticSeqCodeActionExt.addEntry · (decl, ← mkTacticSeqCodeAction decl))
         else
-          let args ← args.mapM resolveGlobalConstNoOverloadWithInfo
+          let args ← args.mapM realizeGlobalConstNoOverloadWithInfo
           if (IR.getSorryDep (← getEnv) decl).isSome then return -- ignore in progress definitions
           modifyEnv (tacticCodeActionExt.addEntry · (⟨decl, args⟩, ← mkTacticCodeAction decl))
       | _ => pure ()

Std/CodeAction/Deprecated.lean

@@ -29,8 +29,8 @@ def deprecatedCodeActionProvider : CodeActionProvider := fun params snap => do
   let mut i := 0
   let doc ← readDoc
   let mut msgs := #[]
-  for diag in snap.interactiveDiags do
-    if let some #[.deprecated] := diag.tags? then
+  for m in snap.msgLog.msgs do
+    if m.data.isDeprecationWarning then
       if h : _ then
         msgs := msgs.push (snap.cmdState.messages.msgs[i])
     i := i + 1

Std/Data/Array/Basic.lean

@@ -161,11 +161,11 @@ namespace Subarray
 The empty subarray.
 -/
 protected def empty : Subarray α where
-  as := #[]
+  array := #[]
   start := 0
   stop := 0
-  h₁ := Nat.le_refl 0
-  h₂ := Nat.le_refl 0
+  start_le_stop := Nat.le_refl 0
+  stop_le_array_size := Nat.le_refl 0
 
 instance : EmptyCollection (Subarray α) :=
   ⟨Subarray.empty⟩
@@ -198,7 +198,7 @@ def popHead? (as : Subarray α) : Option (α × Subarray α) :=
       let tail :=
         { as with
           start := as.start + 1
-          h₁ := Nat.le_of_lt_succ $ Nat.succ_lt_succ h  }
+          start_le_stop := Nat.le_of_lt_succ $ Nat.succ_lt_succ h }
       some (head, tail)
     else
       none

Std/Data/Array/Lemmas.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Authors: Mario Carneiro, Gabriel Ebner
 -/
-import Std.Data.Nat.Lemmas
 import Std.Data.List.Lemmas
 import Std.Data.Array.Init.Lemmas
 import Std.Data.Array.Basic
@@ -20,12 +19,6 @@ import Std.Util.ProofWanted
 @[simp] theorem getElem!_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n)
     [Decidable (Dom a i)] [Inhabited Elem] : a[i]! = a[i.1]! := rfl
 
-theorem getElem?_pos [GetElem Cont Idx Elem Dom]
-    (a : Cont) (i : Idx) (h : Dom a i) [Decidable (Dom a i)] : a[i]? = a[i] := dif_pos h
-
-theorem getElem?_neg [GetElem Cont Idx Elem Dom]
-    (a : Cont) (i : Idx) (h : ¬Dom a i) [Decidable (Dom a i)] : a[i]? = none := dif_neg h
-
 @[simp] theorem mkArray_data (n : Nat) (v : α) : (mkArray n v).data = List.replicate n v := rfl
 
 @[simp] theorem getElem_mkArray (n : Nat) (v : α) (h : i < (mkArray n v).size) :
@@ -93,13 +86,19 @@ theorem get?_push_eq (a : Array α) (x : α) : (a.push x)[a.size]? = some x := b
   rw [getElem?_pos, get_push_eq]
 
 theorem get?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x else a[i]? := by
-  split
-  . next heq => rw [heq, getElem?_pos, get_push_eq]
-  · next hne =>
+  match Nat.lt_trichotomy i a.size with
+  | Or.inl g =>
+    have h1 : i < a.size + 1 := by omega
+    have h2 : i ≠ a.size := by omega
+    simp [getElem?, size_push, g, h1, h2, get_push_lt]
+  | Or.inr (Or.inl heq) =>
+    simp [heq, getElem?_pos, get_push_eq]
+  | Or.inr (Or.inr g) =>
     simp only [getElem?, size_push]
-    split <;> split <;> try simp only [*, get_push_lt]
-    · next p q => exact Or.elim (Nat.eq_or_lt_of_le (Nat.le_of_lt_succ p)) hne q
-    · next p q => exact p (Nat.lt.step q)
+    have h1 : ¬ (i < a.size) := by omega
+    have h2 : ¬ (i < a.size + 1) := by omega
+    have h3 : i ≠ a.size := by omega
+    simp [h1, h2, h3]
 
 @[simp] theorem get?_size {a : Array α} : a[a.size]? = none := by
   simp only [getElem?, Nat.lt_irrefl, dite_false]

Std/Data/Array/Match.lean

@@ -3,7 +3,6 @@ Copyright (c) 2023 F. G. Dorais. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: F. G. Dorais
 -/
-import Std.Data.Nat.Lemmas
 
 namespace Array
 

Std/Data/Array/Merge.lean

@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
 
-import Std.Data.Nat.Lemmas
-
 namespace Array
 
 /--

Std/Data/BinomialHeap/Basic.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura, Jannis Limperg, Mario Carneiro
 -/
 import Std.Classes.Order
 import Std.Control.ForInStep.Basic
-import Std.Data.Nat.Lemmas
 
 namespace Std
 namespace BinomialHeap

Std/Data/BitVec/Lemmas.lean

@@ -3,10 +3,7 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joe Hendrix
 -/
-import Std.Data.Bool
-import Std.Data.Fin.Lemmas
-import Std.Data.Nat.Lemmas
-import Std.Util.ProofWanted
+import Std.Tactic.Alias
 
 namespace BitVec
 

Std/Data/ByteArray.lean

@@ -3,6 +3,7 @@ Copyright (c) 2023 François G. Dorais. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: François G. Dorais
 -/
+import Std.Data.Array.Init.Lemmas
 import Std.Data.Array.Lemmas
 
 namespace ByteArray

Std/Data/HashMap/WF.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Std.Data.HashMap.Basic
-import Std.Data.List.Lemmas
 import Std.Data.Array.Lemmas
+import Std.Data.Nat.Lemmas
 
 namespace Std.HashMap
 namespace Imp

Std/Data/Int.lean

@@ -1,4 +1,3 @@
 import Std.Data.Int.DivMod
-import Std.Data.Int.Gcd
 import Std.Data.Int.Lemmas
 import Std.Data.Int.Order