chore: bump Std dependency to leanprover-community/batteries#432 (#9094)

This covers these changes in Std: leanprover-community/batteries@6b4cf96...9dd24a3

* `Int.ofNat_natAbs_eq_of_nonneg` has become `Int.natAbs_of_nonneg` (and one argument has become implicit)
* `List.map_id''` and `List.map_id'` have exchanged names. (Yay naming things using primes!)
* Some meta functions have moved to Std and can be deleted here.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib/Control/Random.lean

@@ -132,7 +132,7 @@ instance : BoundedRandom m Int where
       Int.le_add_of_nonneg_left (Int.ofNat_zero_le z),
       Int.add_le_of_le_sub_right $ Int.le_trans
         (Int.ofNat_le.mpr h2)
-        (le_of_eq $ Int.ofNat_natAbs_eq_of_nonneg _ $ Int.sub_nonneg_of_le h)⟩
+        (le_of_eq $ Int.natAbs_of_nonneg $ Int.sub_nonneg_of_le h)⟩
 
 instance {n : Nat} : BoundedRandom m (Fin n) where
   randomR lo hi h _ := do

Mathlib/Data/Fintype/Card.lean

@@ -1227,7 +1227,7 @@ theorem List.exists_pw_disjoint_with_card {α : Type*} [Fintype α]
     intro a ha
     conv_rhs => rw [← List.map_id a]
     rw [List.map_pmap]
-    simp only [Fin.valEmbedding_apply, Fin.val_mk, List.pmap_eq_map, List.map_id'', List.map_id]
+    simp only [Fin.valEmbedding_apply, Fin.val_mk, List.pmap_eq_map, List.map_id', List.map_id]
   use l.map (List.map (Fintype.equivFin α).symm)
   constructor
   · -- length

Mathlib/Data/Int/ModEq.lean

@@ -315,7 +315,7 @@ theorem exists_unique_equiv (a : ℤ) {b : ℤ} (hb : 0 < b) :
 theorem exists_unique_equiv_nat (a : ℤ) {b : ℤ} (hb : 0 < b) : ∃ z : ℕ, ↑z < b ∧ ↑z ≡ a [ZMOD b] :=
   let ⟨z, hz1, hz2, hz3⟩ := exists_unique_equiv a hb
   ⟨z.natAbs, by
-    constructor <;> rw [ofNat_natAbs_eq_of_nonneg z hz1] <;> assumption⟩
+    constructor <;> rw [natAbs_of_nonneg hz1] <;> assumption⟩
 #align int.exists_unique_equiv_nat Int.exists_unique_equiv_nat
 
 theorem mod_mul_right_mod (a b c : ℤ) : a % (b * c) % b = a % b :=

Mathlib/Data/List/Basic.lean

@@ -1726,14 +1726,11 @@ theorem map_concat (f : α → β) (a : α) (l : List α) :
   induction l <;> [rfl; simp only [*, concat_eq_append, cons_append, map, map_append]]
 #align list.map_concat List.map_concat
 
-@[simp]
-theorem map_id'' (l : List α) : map (fun x => x) l = l :=
-  map_id _
-#align list.map_id'' List.map_id''
+#align list.map_id'' List.map_id'
 
-theorem map_id' {f : α → α} (h : ∀ x, f x = x) (l : List α) : map f l = l := by
+theorem map_id'' {f : α → α} (h : ∀ x, f x = x) (l : List α) : map f l = l := by
   simp [show f = id from funext h]
-#align list.map_id' List.map_id'
+#align list.map_id' List.map_id''
 
 theorem eq_nil_of_map_eq_nil {f : α → β} {l : List α} (h : map f l = nil) : l = nil :=
   eq_nil_of_length_eq_zero <| by rw [← length_map l f, h]; rfl

Mathlib/Data/List/BigOperators/Basic.lean

@@ -348,7 +348,7 @@ theorem prod_lt_prod_of_ne_nil [Preorder M] [CovariantClass M M (· * ·) (· <
 theorem prod_le_pow_card [Preorder M] [CovariantClass M M (Function.swap (· * ·)) (· ≤ ·)]
     [CovariantClass M M (· * ·) (· ≤ ·)] (l : List M) (n : M) (h : ∀ x ∈ l, x ≤ n) :
     l.prod ≤ n ^ l.length := by
-      simpa only [map_id'', map_const', prod_replicate] using prod_le_prod' h
+      simpa only [map_id', map_const', prod_replicate] using prod_le_prod' h
 #align list.prod_le_pow_card List.prod_le_pow_card
 #align list.sum_le_card_nsmul List.sum_le_card_nsmul
 

Mathlib/Data/List/Sublists.lean

@@ -175,7 +175,7 @@ theorem sublists_cons (a : α) (l : List α) :
 theorem sublists_concat (l : List α) (a : α) :
     sublists (l ++ [a]) = sublists l ++ map (fun x => x ++ [a]) (sublists l) := by
   rw [sublists_append, sublists_singleton, bind_eq_bind, cons_bind, cons_bind, nil_bind,
-     map_id' append_nil, append_nil]
+     map_id'' append_nil, append_nil]
 #align list.sublists_concat List.sublists_concat
 
 theorem sublists_reverse (l : List α) : sublists (reverse l) = map reverse (sublists' l) := by
@@ -189,7 +189,7 @@ theorem sublists_eq_sublists' (l : List α) : sublists l = map reverse (sublists
 #align list.sublists_eq_sublists' List.sublists_eq_sublists'
 
 theorem sublists'_reverse (l : List α) : sublists' (reverse l) = map reverse (sublists l) := by
-  simp only [sublists_eq_sublists', map_map, map_id' reverse_reverse, Function.comp]
+  simp only [sublists_eq_sublists', map_map, map_id'' reverse_reverse, Function.comp]
 #align list.sublists'_reverse List.sublists'_reverse
 
 theorem sublists'_eq_sublists (l : List α) : sublists' l = map reverse (sublists (reverse l)) := by

Mathlib/Data/Nat/Squarefree.lean

@@ -432,7 +432,7 @@ lemma prod_primeFactors_invOn_squarefree :
 
 theorem prod_factors_toFinset_of_squarefree {n : ℕ} (hn : Squarefree n) :
     ∏ p in n.factors.toFinset, p = n := by
-  rw [List.prod_toFinset _ hn.nodup_factors, List.map_id'', Nat.prod_factors hn.ne_zero]
+  rw [List.prod_toFinset _ hn.nodup_factors, List.map_id', Nat.prod_factors hn.ne_zero]
 
 end Nat
 

Mathlib/Init/Data/Int/CompLemmas.lean

@@ -95,7 +95,7 @@ theorem zero_le_ofNat (n : ℕ) : 0 ≤ ofNat n :=
 theorem ne_of_natAbs_ne_natAbs_of_nonneg {a b : ℤ} (ha : 0 ≤ a) (hb : 0 ≤ b)
     (h : natAbs a ≠ natAbs b) : a ≠ b := fun h => by
   have : (natAbs a : ℤ) = natAbs b := by
-    rwa [ofNat_natAbs_eq_of_nonneg _ ha, ofNat_natAbs_eq_of_nonneg _ hb]
+    rwa [natAbs_of_nonneg ha, natAbs_of_nonneg hb]
   injection this
   contradiction
 #align int.ne_of_nat_abs_ne_nat_abs_of_nonneg Int.ne_of_natAbs_ne_natAbs_of_nonneg

Mathlib/Lean/Expr/Basic.lean

@@ -200,44 +200,6 @@ def getAppApps (e : Expr) : Array Expr :=
   let nargs := e.getAppNumArgs
   getAppAppsAux e (mkArray nargs dummy) (nargs-1)
 
-/-- Turn an expression that is a natural number literal into a natural number. -/
-def natLit! : Expr → Nat
-  | lit (Literal.natVal v) => v
-  | _                      => panic! "nat literal expected"
-
-/-- Turn an expression that is a constructor of `Int` applied to a natural number literal
-into an integer. -/
-def intLit! (e : Expr) : Int :=
-  if e.isAppOfArity ``Int.ofNat 1 then
-    e.appArg!.natLit!
-  else if e.isAppOfArity ``Int.negOfNat 1 then
-    .negOfNat e.appArg!.natLit!
-  else
-    panic! "not a raw integer literal"
-
-/--
-Check if an expression is a "natural number in normal form",
-i.e. of the form `OfNat n`, where `n` matches `.lit (.natVal lit)` for some `lit`.
-and if so returns `lit`.
--/
--- Note that an `Expr.lit (.natVal n)` is not considered in normal form!
-def nat? (e : Expr) : Option Nat := do
-  guard <| e.isAppOfArity ``OfNat.ofNat 3
-  let lit (.natVal n) := e.appFn!.appArg! | none
-  n
-
-
-/--
-Check if an expression is an "integer in normal form",
-i.e. either a natural number in normal form, or the negation of one,
-and if so returns the integer.
--/
-def int? (e : Expr) : Option Int :=
-  if e.isAppOfArity ``Neg.neg 3 then
-    (- ·) <$> e.appArg!.nat?
-  else
-    e.nat?
-
 /--
 Check if an expression is a "rational in normal form",
 i.e. either an integer number in normal form,

Mathlib/Lean/Meta.lean

@@ -32,10 +32,6 @@ def «let» (g : MVarId) (h : Name) (v : Expr) (t : Option Expr := .none) :
     MetaM (FVarId × MVarId) := do
   (← g.define h (← t.getDM (inferType v)) v).intro1P
 
-/-- Short-hand for applying a constant to the goal. -/
-def applyConst (mvar : MVarId) (c : Name) (cfg : ApplyConfig := {}) : MetaM (List MVarId) := do
-  mvar.apply (← mkConstWithFreshMVarLevels c) cfg
-
 /-- Has the effect of `refine ⟨e₁,e₂,⋯, ?_⟩`.
 -/
 def existsi (mvar : MVarId) (es : List Expr) : MetaM MVarId := do
@@ -130,13 +126,6 @@ end Lean.MVarId
 
 namespace Lean.Meta
 
-/-- Return local hypotheses which are not "implementation detail", as `Expr`s. -/
-def getLocalHyps [Monad m] [MonadLCtx m] : m (Array Expr) := do
-  let mut hs := #[]
-  for d in ← getLCtx do
-    if !d.isImplementationDetail then hs := hs.push d.toExpr
-  return hs
-
 /-- Count how many local hypotheses appear in an expression. -/
 def countLocalHypsUsed [Monad m] [MonadLCtx m] [MonadMCtx m] (e : Expr) : m Nat := do
   let e' ← instantiateMVars e

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "6b4cf96c89e53cfcd73350bbcd90333a051ff4f0",
+   "rev": "9dd24a3493cceefa2bede383f21e4ef548990b68",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",