chore: adaptations for nightly-2024-11-20

Mathlib/Analysis/Calculus/FDeriv/Mul.lean

@@ -690,7 +690,7 @@ theorem HasFDerivWithinAt.list_prod' {l : List ι} {x : E}
         smulRight (f' l[i]) ((l.drop (.succ i)).map (f · x)).prod) s x := by
   simp only [← List.finRange_map_get l, List.map_map]
   refine .congr_fderiv (hasFDerivAt_list_prod_finRange'.comp_hasFDerivWithinAt x
-    (hasFDerivWithinAt_pi.mpr fun i ↦ h l[i] (l.get_mem i i.isLt))) ?_
+    (hasFDerivWithinAt_pi.mpr fun i ↦ h l[i] (l.getElem_mem i.isLt))) ?_
   ext m
   simp [← List.map_map]
 

Mathlib/Combinatorics/Enumerative/Composition.lean

@@ -150,15 +150,15 @@ theorem sum_blocksFun : ∑ i, c.blocksFun i = n := by
   conv_rhs => rw [← c.blocks_sum, ← ofFn_blocksFun, sum_ofFn]
 
 theorem blocksFun_mem_blocks (i : Fin c.length) : c.blocksFun i ∈ c.blocks :=
-  get_mem _ _ _
+  getElem_mem _
 
 @[simp]
 theorem one_le_blocks {i : ℕ} (h : i ∈ c.blocks) : 1 ≤ i :=
   c.blocks_pos h
 
 @[simp]
 theorem one_le_blocks' {i : ℕ} (h : i < c.length) : 1 ≤ c.blocks[i] :=
-  c.one_le_blocks (get_mem (blocks c) i h)
+  c.one_le_blocks (getElem_mem h)
 
 @[simp]
 theorem blocks_pos' (i : ℕ) (h : i < c.length) : 0 < c.blocks[i] :=

Mathlib/Data/Finset/Sort.lean

@@ -113,7 +113,7 @@ theorem sorted_zero_eq_min'_aux (s : Finset α) (h : 0 < (s.sort (· ≤ ·)).le
     obtain ⟨i, hi⟩ : ∃ i, l.get i = s.min' H := List.mem_iff_get.1 this
     rw [← hi]
     exact (s.sort_sorted (· ≤ ·)).rel_get_of_le (Nat.zero_le i)
-  · have : l.get ⟨0, h⟩ ∈ s := (Finset.mem_sort (α := α) (· ≤ ·)).1 (List.get_mem l 0 h)
+  · have : l.get ⟨0, h⟩ ∈ s := (Finset.mem_sort (α := α) (· ≤ ·)).1 (List.getElem_mem h)
     exact s.min'_le _ this
 
 theorem sorted_zero_eq_min' {s : Finset α} {h : 0 < (s.sort (· ≤ ·)).length} :
@@ -130,7 +130,7 @@ theorem sorted_last_eq_max'_aux (s : Finset α)
   let l := s.sort (· ≤ ·)
   apply le_antisymm
   · have : l.get ⟨(s.sort (· ≤ ·)).length - 1, h⟩ ∈ s :=
-      (Finset.mem_sort (α := α) (· ≤ ·)).1 (List.get_mem l _ h)
+      (Finset.mem_sort (α := α) (· ≤ ·)).1 (List.getElem_mem h)
     exact s.le_max' _ this
   · have : s.max' H ∈ l := (Finset.mem_sort (α := α) (· ≤ ·)).mpr (s.max'_mem H)
     obtain ⟨i, hi⟩ : ∃ i, l.get i = s.max' H := List.mem_iff_get.1 this

Mathlib/Data/List/Cycle.lean

@@ -217,7 +217,7 @@ theorem prev_ne_cons_cons (y z : α) (h : x ∈ y :: z :: l) (hy : x ≠ y) (hz
   · rw [prev, dif_neg hy, if_neg hz]
 
 theorem next_mem (h : x ∈ l) : l.next x h ∈ l :=
-  nextOr_mem (get_mem _ _ _)
+  nextOr_mem (getElem_mem _)
 
 theorem prev_mem (h : x ∈ l) : l.prev x h ∈ l := by
   cases' l with hd tl
@@ -233,7 +233,7 @@ theorem prev_mem (h : x ∈ l) : l.prev x h ∈ l := by
       · exact mem_cons_of_mem _ (hl _ _)
 
 theorem next_get (l : List α) (h : Nodup l) (i : Fin l.length) :
-    next l (l.get i) (get_mem _ _ _) =
+    next l (l.get i) (getElem_mem _) =
       l.get ⟨(i + 1) % l.length, Nat.mod_lt _ (i.1.zero_le.trans_lt i.2)⟩ :=
   match l, h, i with
   | [], _, i => by simpa using i.2
@@ -254,7 +254,7 @@ theorem next_get (l : List α) (h : Nodup l) (i : Fin l.length) :
     · subst hi'
       rw [next_getLast_cons]
       · simp [hi', get]
-      · rw [get_cons_succ]; exact get_mem _ _ _
+      · rw [get_cons_succ]; exact getElem_mem _
       · exact hx'
       · simp [getLast_eq_getElem]
       · exact hn.of_cons
@@ -271,12 +271,12 @@ theorem next_get (l : List α) (h : Nodup l) (i : Fin l.length) :
         intro h
         have := nodup_iff_injective_get.1 hn h
         simp at this; simp [this] at hi'
-      · rw [get_cons_succ]; exact get_mem _ _ _
+      · rw [get_cons_succ]; exact getElem_mem _
 
 -- Unused variable linter incorrectly reports that `h` is unused here.
 set_option linter.unusedVariables false in
 theorem prev_get (l : List α) (h : Nodup l) (i : Fin l.length) :
-    prev l (l.get i) (get_mem _ _ _) =
+    prev l (l.get i) (getElem_mem _) =
       l.get ⟨(i + (l.length - 1)) % l.length, Nat.mod_lt _ i.pos⟩ :=
   match l with
   | [] => by simpa using i.2

Mathlib/Data/List/NodupEquivFin.lean

@@ -49,7 +49,7 @@ variable [DecidableEq α]
 the set of elements of `l`. -/
 @[simps]
 def getEquiv (l : List α) (H : Nodup l) : Fin (length l) ≃ { x // x ∈ l } where
-  toFun i := ⟨get l i, get_mem l i i.2⟩
+  toFun i := ⟨get l i, getElem_mem i.2⟩
   invFun x := ⟨indexOf (↑x) l, indexOf_lt_length.2 x.2⟩
   left_inv i := by simp only [List.get_indexOf, eq_self_iff_true, Fin.eta, Subtype.coe_mk, H]
   right_inv x := by simp

Mathlib/Data/List/Sym.lean

@@ -170,7 +170,7 @@ theorem dedup_sym2 [DecidableEq α] (xs : List α) : xs.sym2.dedup = xs.dedup.sy
     obtain hm | hm := Decidable.em (x ∈ xs)
     · rw [dedup_cons_of_mem hm, ← ih, dedup_cons_of_mem,
         List.Subset.dedup_append_right (map_mk_sublist_sym2 _ _ hm).subset]
-      refine mem_append_of_mem_left _ ?_
+      refine mem_append_left _ ?_
       rw [mem_map]
       exact ⟨_, hm, Sym2.eq_swap⟩
     · rw [dedup_cons_of_not_mem hm, List.sym2, map_cons, ← ih, dedup_cons_of_not_mem, cons_append,

Mathlib/Data/List/TFAE.lean

@@ -62,7 +62,7 @@ theorem tfae_of_cycle {a b} {l : List Prop} (h_chain : List.Chain (· → ·) a
 
 theorem TFAE.out {l} (h : TFAE l) (n₁ n₂) {a b} (h₁ : List.get? l n₁ = some a := by rfl)
     (h₂ : List.get? l n₂ = some b := by rfl) : a ↔ b :=
-  h _ (List.get?_mem h₁) _ (List.get?_mem h₂)
+  h _ (List.mem_of_get? h₁) _ (List.mem_of_get? h₂)
 
 /-- If `P₁ x ↔ ... ↔ Pₙ x` for all `x`, then `(∀ x, P₁ x) ↔ ... ↔ (∀ x, Pₙ x)`.
 Note: in concrete cases, Lean has trouble finding the list `[P₁, ..., Pₙ]` from the list

Mathlib/Data/Vector/Mem.lean

@@ -22,9 +22,7 @@ namespace Vector
 variable {α β : Type*} {n : ℕ} (a a' : α)
 
 @[simp]
-theorem get_mem (i : Fin n) (v : Vector α n) : v.get i ∈ v.toList := by
-  rw [get_eq_get]
-  exact List.get_mem _ _ _
+theorem get_mem (i : Fin n) (v : Vector α n) : v.get i ∈ v.toList := List.getElem_mem _
 
 theorem mem_iff_get (v : Vector α n) : a ∈ v.toList ↔ ∃ i, v.get i = a := by
   simp only [List.mem_iff_get, Fin.exists_iff, Vector.get_eq_get]

Mathlib/Lean/Meta/KAbstractPositions.lean

@@ -71,7 +71,7 @@ def viewKAbstractSubExpr (e : Expr) (pos : SubExpr.Pos) : MetaM (Option (Expr ×
   if subExpr.hasLooseBVars then
     return none
   let positions ← kabstractPositions subExpr e
-  let some n := positions.getIdx? pos | unreachable!
+  let some n := positions.indexOf? pos | unreachable!
   return some (subExpr, if positions.size == 1 then none else some (n + 1))
 
 /-- Determine whether the result of abstracting `subExpr` from `e` at position `pos` results

Mathlib/NumberTheory/ClassNumber/AdmissibleAbsoluteValue.lean

@@ -102,7 +102,7 @@ theorem exists_approx_aux (n : ℕ) (h : abv.IsAdmissible) :
       /-- This proof was nicer prior to https://github.com/leanprover/lean4/pull/4400.
       Please feel welcome to improve it, by avoiding use of `List.get` in favour of `GetElem`. -/
       have : ∀ i h, t ((Finset.univ.filter fun x ↦ t x = s).toList.get ⟨i, h⟩) = s := fun i h ↦
-        (Finset.mem_filter.mp (Finset.mem_toList.mp (List.get_mem _ i h))).2
+        (Finset.mem_filter.mp (Finset.mem_toList.mp (List.getElem_mem h))).2
       simp only [Nat.succ_eq_add_one, Finset.length_toList, List.get_eq_getElem] at this
       simp only [Nat.succ_eq_add_one, List.get_eq_getElem, Fin.coe_castLE]
       rw [this _ (Nat.lt_of_le_of_lt (Nat.le_of_lt_succ i₁.2) hs),

Mathlib/Tactic/CC/Addition.lean

@@ -390,7 +390,7 @@ partial def mkCongrProofCore (lhs rhs : Expr) (heqProofs : Bool) : CCM Expr := d
       guard (kindsIt[0]! matches .eq)
       let some p ← getEqProof (lhsArgs[i]'hi.2) (rhsArgs[i]'(ha.symm ▸ hi.2)) | failure
       lemmaArgs := lemmaArgs.push p
-    kindsIt := kindsIt.eraseIdx 0
+    kindsIt := kindsIt.eraseIdx! 0
   let mut r := mkAppN specLemma.proof lemmaArgs
   if specLemma.heqResult && !heqProofs then
     r ← mkAppM ``eq_of_heq #[r]

Mathlib/Tactic/FBinop.lean

@@ -185,14 +185,18 @@ private def toExprCore (t : Tree) : TermElabM Expr := do
   | .term _ trees e =>
     modifyInfoState (fun s => { s with trees := s.trees ++ trees }); return e
   | .binop ref f lhs rhs =>
-    withRef ref <| withInfoContext' ref (mkInfo := mkTermInfo .anonymous ref) do
+    withRef ref <| withInfoContext' ref (mkInfo := mkTermInfo .anonymous ref) (do
       let lhs ← toExprCore lhs
       let mut rhs ← toExprCore rhs
-      mkBinOp f lhs rhs
+      mkBinOp f lhs rhs)
+      -- FIXME the signature of withInfoContext' has changed, not sure yet what to put here:
+      (do failure)
   | .macroExpansion macroName stx stx' nested =>
-    withRef stx <| withInfoContext' stx (mkInfo := mkTermInfo macroName stx) do
+    withRef stx <| withInfoContext' stx (mkInfo := mkTermInfo macroName stx) (do
       withMacroExpansion stx stx' do
-        toExprCore nested
+        toExprCore nested)
+      -- FIXME the signature of withInfoContext' has changed, not sure yet what to put here:
+      (do failure)
 
 /-- Try to coerce elements in the tree to `maxS` when needed. -/
 private def applyCoe (t : Tree) (maxS : SRec) : TermElabM Tree := do

Mathlib/Tactic/Linarith/Frontend.lean

@@ -277,7 +277,7 @@ def runLinarith (cfg : LinarithConfig) (prefType : Option Expr) (g : MVarId)
       if let some t := prefType then
         let (i, vs) ← hyp_set.find t
         proveFalseByLinarith cfg.transparency cfg.oracle cfg.discharger g vs <|>
-        findLinarithContradiction cfg g ((hyp_set.eraseIdx i).toList.map (·.2))
+        findLinarithContradiction cfg g ((hyp_set.eraseIdxIfInBounds i).toList.map (·.2))
       else findLinarithContradiction cfg g (hyp_set.toList.map (·.2))
   let mut preprocessors := cfg.preprocessors
   if cfg.splitNe then

Mathlib/Tactic/Linter/PPRoundtrip.lean

@@ -60,7 +60,7 @@ def polishSource (s : String) : String × Array Nat :=
   let preWS := split.foldl (init := #[]) fun p q =>
     let txt := q.trimLeft.length
     (p.push (q.length - txt)).push txt
-  let preWS := preWS.eraseIdx 0
+  let preWS := preWS.eraseIdx! 0
   let s := (split.map .trimLeft).filter (· != "")
   (" ".intercalate (s.filter (!·.isEmpty)), preWS)
 

Mathlib/Tactic/MoveAdd.lean

@@ -195,7 +195,8 @@ def reorderUsing (toReorder : List α) (instructions : List (α × Bool)) : List
   let uToReorder := (uniquify toReorder).toArray
   let reorder := uToReorder.qsort fun x y =>
     match uInstructions.find? (Prod.fst · == x), uInstructions.find? (Prod.fst · == y) with
-      | none, none => (uToReorder.getIdx? x).get! ≤ (uToReorder.getIdx? y).get!
+      | none, none =>
+        ((uToReorder.indexOf? x).map Fin.val).get! ≤ ((uToReorder.indexOf? y).map Fin.val).get!
       | _, _ => weight uInstructions x ≤ weight uInstructions y
   (reorder.map Prod.fst).toList
 

Mathlib/Tactic/ToAdditive/Frontend.lean

@@ -866,7 +866,7 @@ def additivizeLemmas {m : Type → Type} [Monad m] [MonadError m] [MonadLiftT Co
   for (nm, lemmas) in names.zip auxLemmas do
     unless lemmas.size == nLemmas do
       throwError "{names[0]!} and {nm} do not generate the same number of {desc}."
-  for (srcLemmas, tgtLemmas) in auxLemmas.zip <| auxLemmas.eraseIdx 0 do
+  for (srcLemmas, tgtLemmas) in auxLemmas.zip <| auxLemmas.eraseIdx! 0 do
     for (srcLemma, tgtLemma) in srcLemmas.zip tgtLemmas do
       insertTranslation srcLemma tgtLemma
 

Mathlib/Tactic/Variable.lean

@@ -159,7 +159,7 @@ partial def completeBinders' (maxSteps : Nat) (gas : Nat)
     (binders : TSyntaxArray ``bracketedBinder)
     (toOmit : Array Bool) (i : Nat) :
     TermElabM (TSyntaxArray ``bracketedBinder × Array Bool) := do
-  if 0 < gas && i < binders.size then
+  if h : 0 < gas ∧ i < binders.size then
     let binder := binders[i]!
     trace[«variable?»] "\
       Have {(← getLCtx).getFVarIds.size} fvars and {(← getLocalInstances).size} local instances. \
@@ -176,7 +176,7 @@ partial def completeBinders' (maxSteps : Nat) (gas : Nat)
           in binders since they are generated by pretty printing unsatisfied dependencies.\n\n\
           Current variable command:{indentD (← `(command| variable $binders'*))}\n\n\
           Local context for the unsatisfied dependency:{goalMsg}"
-      let binders := binders.insertAt! i binder'
+      let binders := binders.insertIdx i binder'
       completeBinders' maxSteps (gas - 1) checkRedundant binders toOmit i
     else
       let lctx ← getLCtx

Mathlib/Testing/Plausible/Functions.lean

@@ -202,7 +202,7 @@ theorem List.applyId_zip_eq [DecidableEq α] {xs ys : List α} (h₀ : List.Nodu
         simp only [getElem?_cons_succ, zip_cons_cons, applyId_cons] at h₂ ⊢
         rw [if_neg]
         · apply xs_ih <;> solve_by_elim [Nat.succ.inj]
-        · apply h₀; apply List.getElem?_mem h₂
+        · apply h₀; apply List.mem_of_getElem? h₂
 
 theorem applyId_mem_iff [DecidableEq α] {xs ys : List α} (h₀ : List.Nodup xs) (h₁ : xs ~ ys)
     (x : α) : List.applyId.{u} (xs.zip ys) x ∈ ys ↔ x ∈ xs := by

lake-manifest.json

@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0fc755a2a762bd228db724df926de7d3e2306a34",
+   "rev": "a75e35f6cb83e773231f793d1cd8112e41804934",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "24d0b61ede545901e80ee866a3609f9e78080034",
+   "rev": "0c995c64c9c8e4186e24f85d5d61bc404b378ba6",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9762792852464bf9591f6cccfe44f14b3ef54b25",
+   "rev": "9b9f4d0406d00baaae62d1a717b5aa854a2ae51d",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2024-11-19
+leanprover/lean4:nightly-2024-11-20