Trigger CI for leanprover/lean4#3756

Std/CodeAction/Deprecated.lean

@@ -32,7 +32,7 @@ def deprecatedCodeActionProvider : CodeActionProvider := fun params snap => do
   for m in snap.msgLog.msgs do
     if m.data.isDeprecationWarning then
       if h : _ then
-        msgs := msgs.push (snap.cmdState.messages.msgs[i]'h)
+        msgs := msgs.push (snap.cmdState.messages.msgs[i])
     i := i + 1
   if msgs.isEmpty then return #[]
   let start := doc.meta.text.lspPosToUtf8Pos params.range.start

Std/Data/Array/Lemmas.lean

@@ -9,8 +9,6 @@ import Std.Data.Array.Basic
 import Std.Tactic.SeqFocus
 import Std.Util.ProofWanted
 
-local macro_rules | `($x[$i]'$h) => `(getElem $x $i $h)
-
 @[simp] theorem getElem_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a i) :
     a[i] = a[i.1] := rfl
 
@@ -20,16 +18,10 @@ local macro_rules | `($x[$i]'$h) => `(getElem $x $i $h)
 @[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) :
-    (mkArray n v)[i]'h = v := by simp [Array.getElem_eq_data_get]
+    (mkArray n v)[i] = v := by simp [Array.getElem_eq_data_get]
 
 namespace Array
 
@@ -93,21 +85,27 @@ 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]
 
 @[simp] theorem data_set (a : Array α) (i v) : (a.set i v).data = a.data.set i.1 v := rfl
 
 theorem get_set_eq (a : Array α) (i : Fin a.size) (v : α) :
-    (a.set i v)[i.1]'(by simp [i.2]) = v := by
+    (a.set i v)[i.1] = v := by
   simp only [set, getElem_eq_data_get, List.get_set_eq]
 
 theorem get?_set_eq (a : Array α) (i : Fin a.size) (v : α) :
@@ -130,7 +128,7 @@ theorem get_set (a : Array α) (i : Fin a.size) (j : Nat) (hj : j < a.size) (v :
   simp only [set, getElem_eq_data_get, List.get_set_ne _ h]
 
 theorem getElem_setD (a : Array α) (i : Nat) (v : α) (h : i < (setD a i v).size) :
-  (setD a i v)[i]'h = v := by
+  (setD a i v)[i] = v := by
   simp at h
   simp only [setD, h, dite_true, get_set, ite_true]
 
@@ -186,7 +184,7 @@ theorem eq_push_pop_back_of_size_ne_zero [Inhabited α] {as : Array α} (h : as.
 
 theorem eq_push_of_size_ne_zero {as : Array α} (h : as.size ≠ 0) :
     ∃ (bs : Array α) (c : α), as = bs.push c :=
-  let _ : Inhabited α := ⟨as[0]'(Nat.zero_lt_of_ne_zero h)⟩
+  let _ : Inhabited α := ⟨as[0]⟩
   ⟨as.pop, as.back, eq_push_pop_back_of_size_ne_zero h⟩
 
 theorem size_eq_length_data (as : Array α) : as.size = as.data.length := rfl
@@ -428,9 +426,9 @@ theorem map_eq_foldl (as : Array α) (f : α → β) :
 theorem map_induction (as : Array α) (f : α → β) (motive : Nat → Prop) (h0 : motive 0)
     (p : Fin as.size → β → Prop) (hs : ∀ i, motive i.1 → p i (f as[i]) ∧ motive (i+1)) :
     motive as.size ∧
-      ∃ eq : (as.map f).size = as.size, ∀ i h, p ⟨i, h⟩ ((as.map f)[i]'(eq ▸ h)) := by
+      ∃ eq : (as.map f).size = as.size, ∀ i h, p ⟨i, h⟩ ((as.map f)[i]) := by
   have t := foldl_induction (as := as) (β := Array β)
-    (motive := fun i arr => motive i ∧ arr.size = i ∧ ∀ i h2, p i (arr[i.1]'h2))
+    (motive := fun i arr => motive i ∧ arr.size = i ∧ ∀ i h2, p i arr[i.1])
     (init := #[]) (f := fun r a => r.push (f a)) ?_ ?_
   obtain ⟨m, eq, w⟩ := t
   · refine ⟨m, by simpa [map_eq_foldl] using eq, ?_⟩
@@ -454,11 +452,11 @@ theorem map_induction (as : Array α) (f : α → β) (motive : Nat → Prop) (h
 
 theorem map_spec (as : Array α) (f : α → β) (p : Fin as.size → β → Prop)
     (hs : ∀ i, p i (f as[i])) :
-    ∃ eq : (as.map f).size = as.size, ∀ i h, p ⟨i, h⟩ ((as.map f)[i]'(eq ▸ h)) := by
+    ∃ eq : (as.map f).size = as.size, ∀ i h, p ⟨i, h⟩ ((as.map f)[i]) := by
   simpa using map_induction as f (fun _ => True) trivial p (by simp_all)
 
 @[simp] theorem getElem_map (f : α → β) (as : Array α) (i : Nat) (h) :
-    ((as.map f)[i]'h) = f (as[i]'(size_map .. ▸ h)) := by
+    ((as.map f)[i]) = f (as[i]'(size_map .. ▸ h)) := by
   have := map_spec as f (fun i b => b = f (as[i]))
   simp only [implies_true, true_implies] at this
   obtain ⟨eq, w⟩ := this
@@ -473,10 +471,10 @@ theorem mapIdx_induction (as : Array α) (f : Fin as.size → α → β)
     (p : Fin as.size → β → Prop)
     (hs : ∀ i, motive i.1 → p i (f i as[i]) ∧ motive (i + 1)) :
     motive as.size ∧ ∃ eq : (Array.mapIdx as f).size = as.size,
-      ∀ i h, p ⟨i, h⟩ ((Array.mapIdx as f)[i]'(eq ▸ h)) := by
+      ∀ i h, p ⟨i, h⟩ ((Array.mapIdx as f)[i]) := by
   let rec go {bs i j h} (h₁ : j = bs.size) (h₂ : ∀ i h h', p ⟨i, h⟩ bs[i]) (hm : motive j) :
     let arr : Array β := Array.mapIdxM.map (m := Id) as f i j h bs
-    motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ (arr[i]'(eq ▸ h)) := by
+    motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i] := by
     induction i generalizing j bs with simp [mapIdxM.map]
     | zero =>
       have := (Nat.zero_add _).symm.trans h
@@ -496,7 +494,7 @@ theorem mapIdx_induction (as : Array α) (f : Fin as.size → α → β)
 theorem mapIdx_spec (as : Array α) (f : Fin as.size → α → β)
     (p : Fin as.size → β → Prop) (hs : ∀ i, p i (f i as[i])) :
     ∃ eq : (Array.mapIdx as f).size = as.size,
-      ∀ i h, p ⟨i, h⟩ ((Array.mapIdx as f)[i]'(eq ▸ h)) :=
+      ∀ i h, p ⟨i, h⟩ ((Array.mapIdx as f)[i]) :=
   (mapIdx_induction _ _ (fun _ => True) trivial p fun _ _ => ⟨hs .., trivial⟩).2
 
 @[simp] theorem size_mapIdx (a : Array α) (f : Fin a.size → α → β) : (a.mapIdx f).size = a.size :=
@@ -505,9 +503,10 @@ theorem mapIdx_spec (as : Array α) (f : Fin as.size → α → β)
 @[simp] theorem size_zipWithIndex (as : Array α) : as.zipWithIndex.size = as.size :=
   Array.size_mapIdx _ _
 
-@[simp] theorem getElem_mapIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat) (h) :
+@[simp] theorem getElem_mapIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat)
+    (h : i < (mapIdx a f).size) :
     haveI : i < a.size := by simp_all
-    (a.mapIdx f)[i]'h = f ⟨i, this⟩ a[i] :=
+    (a.mapIdx f)[i] = f ⟨i, this⟩ a[i] :=
   (mapIdx_spec _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i _
 
 /-! ### modify -/

Std/Data/Array/Monadic.lean

@@ -34,7 +34,7 @@ theorem SatisfiesM_mapM [Monad m] [LawfulMonad m] (as : Array α) (f : α → m
     (p : Fin as.size → β → Prop)
     (hs : ∀ i, motive i.1 → SatisfiesM (p i · ∧ motive (i + 1)) (f as[i])) :
     SatisfiesM
-      (fun arr => motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ (arr[i]'(eq ▸ h)))
+      (fun arr => motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i])
       (Array.mapM f as) := by
   rw [mapM_eq_foldlM]
   refine SatisfiesM_foldlM (m := m) (β := Array β)
@@ -51,7 +51,7 @@ theorem SatisfiesM_mapM' [Monad m] [LawfulMonad m] (as : Array α) (f : α → m
     (p : Fin as.size → β → Prop)
     (hs : ∀ i, SatisfiesM (p i) (f as[i])) :
     SatisfiesM
-      (fun arr => ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ (arr[i]'(eq ▸ h)))
+      (fun arr => ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i])
       (Array.mapM f as) :=
   (SatisfiesM_mapM _ _ (fun _ => True) trivial _ (fun _ h => (hs _).imp (⟨·, h⟩))).imp (·.2)
 
@@ -130,11 +130,11 @@ theorem SatisfiesM_mapIdxM [Monad m] [LawfulMonad m] (as : Array α) (f : Fin as
     (p : Fin as.size → β → Prop)
     (hs : ∀ i, motive i.1 → SatisfiesM (p i · ∧ motive (i + 1)) (f i as[i])) :
     SatisfiesM
-      (fun arr => motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ (arr[i]'(eq ▸ h)))
+      (fun arr => motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i])
       (Array.mapIdxM as f) := by
   let rec go {bs i j h} (h₁ : j = bs.size) (h₂ : ∀ i h h', p ⟨i, h⟩ bs[i]) (hm : motive j) :
     SatisfiesM
-      (fun arr => motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ (arr[i]'(eq ▸ h)))
+      (fun arr => motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i])
       (Array.mapIdxM.map as f i j h bs) := by
     induction i generalizing j bs with simp [mapIdxM.map]
     | zero =>

Std/Data/HashMap/WF.lean

@@ -69,7 +69,7 @@ theorem reinsertAux_size [Hashable α] (data : Buckets α β) (a : α) (b : β)
 theorem reinsertAux_WF [BEq α] [Hashable α] {data : Buckets α β} {a : α} {b : β} (H : data.WF)
     (h₁ : ∀ [PartialEquivBEq α] [LawfulHashable α],
       haveI := mkIdx data.2 (hash a).toUSize
-      (data.val[this.1]'this.2).All fun x _ => ¬(a == x)) :
+      data.val[this.1].All fun x _ => ¬(a == x)) :
     (reinsertAux data a b).WF :=
   H.update (.cons h₁) fun
     | _, _, .head .. => rfl