Update lean-toolchain for leanprover/lean4#9932

Author: leanprover-community-mathlib4-bot

Batteries/Data/Fin/Lemmas.lean

@@ -5,11 +5,26 @@ Authors: Mario Carneiro
 -/
 import Batteries.Data.Fin.Basic
 import Batteries.Util.ProofWanted
+import Batteries.Tactic.Alias
 
 namespace Fin
 
 attribute [norm_cast] val_last
 
+/-! ### foldl/foldr -/
+
+theorem foldl_assoc {op : α → α → α} [ha : Std.Associative op] {f : Fin n → α} {a₁ a₂} :
+    foldl n (fun x i => op x (f i)) (op a₁ a₂) = op a₁ (foldl n (fun x i => op x (f i)) a₂) := by
+  induction n generalizing a₂ with
+  | zero => rfl
+  | succ n ih => simp only [foldl_succ, ha.assoc, ih]
+
+theorem foldr_assoc {op : α → α → α} [ha : Std.Associative op] {f : Fin n → α} {a₁ a₂} :
+    foldr n (fun i x => op (f i) x) (op a₁ a₂) = op (foldr n (fun i x => op (f i) x) a₁) a₂ := by
+  induction n generalizing a₂ with
+  | zero => rfl
+  | succ n ih => simp only [foldr_succ, ha.assoc, ih]
+
 /-! ### clamp -/
 
 @[simp] theorem coe_clamp (n m : Nat) : (clamp n m : Nat) = min n m := rfl
@@ -21,14 +36,9 @@ attribute [norm_cast] val_last
 @[simp] theorem findSome?_one {f : Fin 1 → Option α} : findSome? f = f 0 := rfl
 
 theorem findSome?_succ {f : Fin (n+1) → Option α} :
-    findSome? f = (f 0 <|> findSome? fun i => f i.succ) := by
-  simp only [findSome?, foldl_succ]
-  cases f 0
-  · rw [Option.orElse_eq_orElse, Option.orElse_none, Option.orElse_none]
-  · simp only [Option.orElse_some, Option.orElse_eq_orElse, Option.orElse_none]
-    induction n with
-    | zero => rfl
-    | succ n ih => rw [foldl_succ, Option.orElse_some, ih (f := fun i => f i.succ)]
+    findSome? f = (f 0).or (findSome? fun i => f i.succ) := by
+  simp only [findSome?, foldl_succ, Option.orElse_eq_orElse, Option.orElse_eq_or]
+  exact Eq.trans (by cases (f 0) <;> rfl) foldl_assoc
 
 theorem findSome?_succ_of_some {f : Fin (n+1) → Option α} (h : f 0 = some x) :
     findSome? f = some x := by simp [findSome?_succ, h]
@@ -42,68 +52,67 @@ theorem findSome?_succ_of_none {f : Fin (n+1) → Option α} (h : f 0 = none) :
 theorem findSome?_succ_of_isNone {f : Fin (n+1) → Option α} (h : (f 0).isNone) :
     findSome? f = findSome? fun i => f i.succ := by simp_all [findSome?_succ_of_none]
 
-theorem exists_of_findSome?_eq_some {f : Fin n → Option α} (h : findSome? f = some x) :
-    ∃ i, f i = some x := by
+@[simp, grind =]
+theorem findSome?_eq_some_iff {f : Fin n → Option α} :
+    findSome? f = some a ↔ ∃ i, f i = some a ∧ ∀ j < i, f j = none := by
   induction n with
-  | zero => rw [findSome?_zero] at h; contradiction
+  | zero =>
+    simp only [findSome?_zero, (Option.some_ne_none _).symm, false_iff]
+    exact fun  ⟨i, _⟩ => i.elim0
   | succ n ih =>
-    rw [findSome?_succ] at h
-    match heq : f 0 with
-    | some x =>
-      rw [heq, Option.orElse_eq_orElse, Option.orElse_some] at h
-      exists 0
-      rw [heq, h]
-    | none =>
-      rw [heq, Option.orElse_eq_orElse, Option.orElse_none] at h
-      match ih h with | ⟨i, _⟩ => exists i.succ
+    simp only [findSome?_succ, Option.or_eq_some_iff, Fin.exists_fin_succ, Fin.forall_fin_succ,
+      not_lt_zero, false_implies, implies_true, and_true, succ_lt_succ_iff, succ_pos,
+      forall_const, ih, and_left_comm (b := f 0 = none), exists_and_left]
 
-theorem eq_none_of_findSome?_eq_none {f : Fin n → Option α} (h : findSome? f = none) (i) :
-    f i = none := by
+@[simp, grind =] theorem findSome?_eq_none_iff {f : Fin n → Option α} :
+    findSome? f = none ↔ ∀ i, f i = none := by
   induction n with
-  | zero => cases i; contradiction
+  | zero =>
+    simp only [findSome?_zero, true_iff]
+    exact fun i => i.elim0
   | succ n ih =>
-    rw [findSome?_succ] at h
-    match heq : f 0 with
-    | some x =>
-      rw [heq, Option.orElse_eq_orElse, Option.orElse_some] at h
-      contradiction
-    | none =>
-      rw [heq, Option.orElse_eq_orElse, Option.orElse_none] at h
-      cases i using Fin.cases with
-      | zero => exact heq
-      | succ i => exact ih h i
-
-@[simp] theorem findSome?_isSome_iff {f : Fin n → Option α} :
-    (findSome? f).isSome ↔ ∃ i, (f i).isSome := by
-  simp only [Option.isSome_iff_exists]
-  constructor
-  · intro ⟨x, hx⟩
-    match exists_of_findSome?_eq_some hx with
-    | ⟨i, hi⟩ => exists i, x
-  · intro ⟨i, x, hix⟩
-    match h : findSome? f with
-    | some x => exists x
-    | none => rw [eq_none_of_findSome?_eq_none h i] at hix; contradiction
-
-@[simp] theorem findSome?_eq_none_iff {f : Fin n → Option α} :
-    findSome? f = none ↔ ∀ i, f i = none := by
-  constructor
-  · exact eq_none_of_findSome?_eq_none
-  · intro hf
-    match h : findSome? f with
-    | none => rfl
-    | some x =>
-      match exists_of_findSome?_eq_some h with
-      | ⟨i, h⟩ => rw [hf] at h; contradiction
-
-theorem findSome?_isNone_iff {f : Fin n → Option α} :
+    simp only [findSome?_succ, Option.or_eq_none_iff, ih, forall_fin_succ]
+
+theorem isNone_findSome?_iff {f : Fin n → Option α} :
     (findSome? f).isNone ↔ ∀ i, (f i).isNone := by simp
 
+@[deprecated (since := "2025-09-28")]
+alias findSome?_isNone_iff := isNone_findSome?_iff
+
+@[simp] theorem isSome_findSome?_iff {f : Fin n → Option α} :
+    (findSome? f).isSome ↔ ∃ i, (f i).isSome := by
+  cases h : findSome? f with (simp only [findSome?_eq_none_iff, findSome?_eq_some_iff] at h; grind)
+
+@[deprecated (since := "2025-09-28")]
+alias findSome?_isSome_iff := isSome_findSome?_iff
+
+theorem exists_minimal_of_findSome?_eq_some {f : Fin n → Option α}
+    (h : findSome? f = some x) : ∃ i, f i = some x ∧ ∀ j < i, f j = none :=
+  findSome?_eq_some_iff.1 h
+
+theorem exists_eq_some_of_findSome?_eq_some {f : Fin n → Option α}
+    (h : findSome? f = some x) : ∃ i, f i = some x := by grind
+
+@[deprecated (since := "2025-09-28")]
+alias exists_of_findSome?_eq_some := exists_eq_some_of_findSome?_eq_some
+
+theorem eq_none_of_findSome?_eq_none {f : Fin n → Option α} (h : findSome? f = none) (i) :
+    f i = none := findSome?_eq_none_iff.1 h i
+
+theorem exists_isSome_of_isSome_findSome? {f : Fin n → Option α} (h : (findSome? f).isSome) :
+    ∃ i, (f i).isSome := isSome_findSome?_iff.1 h
+
+theorem isNone_of_isNone_findSome? {f : Fin n → Option α} (h : (findSome? f).isNone) :
+    (f i).isNone := isNone_findSome?_iff.1 h i
+
+theorem isSome_findSome?_of_isSome {f : Fin n → Option α} (h : (f i).isSome) :
+    (findSome? f).isSome := isSome_findSome?_iff.2 ⟨_, h⟩
+
 theorem map_findSome? (f : Fin n → Option α) (g : α → β) :
-    (findSome? f).map g = findSome? (Option.map g ∘ f) := by
+    (findSome? f).map g = findSome? (Option.map g <| f ·) := by
   induction n with
   | zero => rfl
-  | succ n ih => simp [findSome?_succ, Function.comp_def, Option.map_or, ih]
+  | succ n ih => simp [findSome?_succ, Option.map_or, ih]
 
 theorem findSome?_guard {p : Fin n → Bool} : findSome? (Option.guard p) = find? p := rfl
 
@@ -123,38 +132,62 @@ theorem findSome?_eq_findSome?_finRange (f : Fin n → Option α) :
 
 theorem find?_succ {p : Fin (n+1) → Bool} :
     find? p = if p 0 then some 0 else (find? fun i => p i.succ).map Fin.succ := by
-  simp only [find?, findSome?_succ, Option.guard]
-  split <;> simp [map_findSome?, Function.comp_def, Option.guard]
+  simp only [find?, findSome?_succ, Option.guard, fun a => apply_ite (Option.or · a),
+    Option.some_or, Option.none_or, map_findSome?, Option.map_if]
 
-theorem eq_true_of_find?_eq_some {p : Fin n → Bool} (h : find? p = some i) : p i = true := by
-  match exists_of_findSome?_eq_some h with
-  | ⟨i, hi⟩ =>
-    simp only [Option.guard] at hi
-    split at hi
-    · cases hi; assumption
-    · contradiction
+@[simp, grind =]
+theorem find?_eq_some_iff {p : Fin n → Bool} :
+    find? p = some i ↔ p i ∧ ∀ j, j < i → p j = false := by simp [find?, and_assoc]
 
-theorem eq_false_of_find?_eq_none {p : Fin n → Bool} (h : find? p = none) (i) : p i = false := by
-  have hi := eq_none_of_findSome?_eq_none h i
-  simp only [Option.guard] at hi
-  split at hi
-  · contradiction
-  · simp [*]
+theorem isSome_find?_iff {p : Fin n → Bool} :
+    (find? p).isSome ↔ ∃ i, p i := by simp [find?]
 
-theorem find?_isSome_iff {p : Fin n → Bool} : (find? p).isSome ↔ ∃ i, p i := by
-  simp [find?]
+@[deprecated (since := "2025-09-28")]
+alias find?_isSome_iff := isSome_find?_iff
 
-theorem find?_isNone_iff {p : Fin n → Bool} : (find? p).isNone ↔ ∀ i, ¬ p i := by
-  simp [find?]
+@[simp, grind =]
+theorem find?_eq_none_iff {p : Fin n → Bool} : find? p = none ↔ ∀ i, p i = false := by simp [find?]
 
-proof_wanted find?_eq_some_iff {p : Fin n → Bool} : find? p = some i ↔ p i ∧ ∀ j, j < i → ¬ p j
+theorem isNone_find?_iff {p : Fin n → Bool} : (find? p).isNone ↔ ∀ i, p i = false := by simp [find?]
 
-theorem find?_eq_none_iff {p : Fin n → Bool} : find? p = none ↔ ∀ i, ¬ p i := by
-  rw [← find?_isNone_iff, Option.isNone_iff_eq_none]
+@[deprecated (since := "2025-09-28")]
+alias find?_isNone_iff := isNone_find?_iff
 
-theorem find?_eq_find?_finRange {p : Fin n → Bool} : find? p = (List.finRange n).find? p := by
-  induction n with
-  | zero => rfl
-  | succ n ih =>
-    rw [find?_succ, List.finRange_succ, List.find?_cons]
-    split <;> simp [Function.comp_def, *]
+theorem eq_true_of_find?_eq_some {p : Fin n → Bool} (h : find? p = some i) : p i :=
+    (find?_eq_some_iff.mp h).1
+
+theorem eq_false_of_find?_eq_some_of_lt {p : Fin n → Bool} (h : find? p = some i) :
+    ∀ j < i, p j = false := (find?_eq_some_iff.mp h).2
+
+theorem eq_false_of_find?_eq_none {p : Fin n → Bool} (h : find? p = none) (i) :
+    p i = false := find?_eq_none_iff.1 h i
+
+theorem exists_eq_true_of_isSome_find? {p : Fin n → Bool} (h : (find? p).isSome) :
+    ∃ i, p i := isSome_find?_iff.1 h
+
+theorem eq_false_of_isNone_find? {p : Fin n → Bool}  (h : (find? p).isNone) : p i = false :=
+  isNone_find?_iff.1 h i
+
+theorem isSome_find?_of_eq_true {p : Fin n → Bool}  (h : p i) :
+    (find? p).isSome := isSome_find?_iff.2 ⟨_, h⟩
+
+theorem get_find?_eq_true {p : Fin n → Bool} (h : (find? p).isSome) : p ((find? p).get h) :=
+  eq_true_of_find?_eq_some (Option.some_get _).symm
+
+theorem get_find?_minimal {p : Fin n → Bool}  (h : (find? p).isSome) :
+    ∀ j, j < (find? p).get h → p j = false :=
+  eq_false_of_find?_eq_some_of_lt (Option.some_get _).symm
+
+theorem find?_eq_find?_finRange {p : Fin n → Bool} : find? p = (List.finRange n).find? p :=
+  (findSome?_eq_findSome?_finRange _).trans (List.findSome?_guard)
+
+/-! ### exists -/
+
+theorem exists_eq_true_iff_exists_minimal_eq_true (p : Fin n → Bool):
+    (∃ i, p i) ↔ ∃ i, p i ∧ ∀ j < i, p j = false := by
+  cases h : find? p <;> grind
+
+theorem exists_iff_exists_minimal (p : Fin n → Prop) [DecidablePred p] :
+    (∃ i, p i) ↔ ∃ i, p i ∧ ∀ j < i, ¬ p j := by
+  simpa only [decide_eq_true_iff, decide_eq_false_iff_not] using
+    exists_eq_true_iff_exists_minimal_eq_true (p ·)

Batteries/Data/String/Lemmas.lean

@@ -133,7 +133,7 @@ theorem Valid.le_endPos : ∀ {s p}, Valid s p → p ≤ endPos s
 end Pos
 
 theorem endPos_eq_zero (s : String) : endPos s = 0 ↔ s = "" := by
-  simp [String.ext_iff, ← utf8Len_eq_zero, Pos.ext_iff, endPos]
+  simp [Pos.ext_iff, endPos]
 
 theorem isEmpty_iff (s : String) : isEmpty s ↔ s = "" :=
   (beq_iff_eq ..).trans (endPos_eq_zero _)
@@ -793,10 +793,6 @@ theorem takeWhileAux_of_valid (p : Char → Bool) : ∀ l m r,
     cases p c <;> simp
     simpa [← Nat.add_assoc, Nat.add_right_comm] using takeWhileAux_of_valid p (l++[c]) m r
 
-@[simp]
-theorem data_eq_nil_iff (s : String) : s.data = [] ↔ s = "" :=
-  ⟨fun h => ext (id h), congrArg data⟩
-
 @[simp]
 theorem map_eq_empty_iff (s : String) (f : Char → Char) : (s.map f) = "" ↔ s = "" := by
   simp only [map_eq, ← data_eq_nil_iff, String.mk_eq_asString, List.data_asString,

README.md

@@ -75,12 +75,13 @@ Batteries PRs often affect Mathlib, a key component of the Lean ecosystem.
 When Batteries changes in a significant way, Mathlib must adapt promptly.
 When necessary, Batteries contributors are expected to either create an adaptation PR on Mathlib, or ask for assistance for and to collaborate with this necessary process.
 
-Every Batteries PR has an automatically created Mathlib branch called `batteries-pr-testing-N` where `N` is the number of the Batteries PR.
+Every Batteries PR has an automatically created [Mathlib Nightly Testing](https://github.com/leanprover-community/mathlib4-nightly-testing/) branch called `batteries-pr-testing-N` where `N` is the number of the Batteries PR.
 This is a clone of Mathlib where the Batteries requirement points to the Batteries PR branch instead of the main branch.
 Batteries uses this branch to check whether the Batteries PR needs Mathlib adaptations.
 A tag `builds-mathlib` will be issued when this branch needs no adaptation; a tag `breaks-mathlib` will be issued when the branch does need an adaptation.
 
 The first step in creating an adaptation PR is to switch to the `batteries-pr-testing-N` branch and push changes to that branch until the Mathlib CI process works.
+You may need to ask for write access to [Mathlib Nightly Testing](https://github.com/leanprover-community/mathlib4-nightly-testing/) to do that.
 Changes to the Batteries PR will be integrated automatically as you work on this process.
 Do not redirect the Batteries requirement to main until the Batteries PR is merged.
 Please ask questions to Batteries and Mathlib maintainers if you run into issues with this process.

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4-pr-releases:pr-release-9932-1c79aac
+leanprover/lean4-pr-releases:pr-release-9932-843181b