merge nightly-testing

leanprover-community · Aug 17, 2024 · 61bf963 · 61bf963
2 parents 50a68a2 + 1e44ccd
commit 61bf963
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 4 deletions.
diff --git a/Batteries/Data/List/Basic.lean b/Batteries/Data/List/Basic.lean
@@ -542,7 +542,7 @@ theorem sections_eq_nil_of_isEmpty : ∀ {L}, L.any isEmpty → @sections α L =
   | l :: L, h => by
     simp only [any, foldr, Bool.or_eq_true] at h
     match l, h with
-    | [], .inl rfl => simp; induction sections L <;> simp [*]
+    | [], .inl rfl => simp
     | l, .inr h => simp [sections, sections_eq_nil_of_isEmpty h]
 
 @[csimp] theorem sections_eq_sectionsTR : @sections = @sectionsTR := by

diff --git a/Batteries/Data/RBMap/Lemmas.lean b/Batteries/Data/RBMap/Lemmas.lean
@@ -1185,7 +1185,9 @@ theorem contains_iff_findEntry? {t : RBMap α β cmp} :
 
 theorem contains_iff_find? {t : RBMap α β cmp} :
     t.contains x ↔ ∃ v, t.find? x = some v := by
-  simp [contains_iff_findEntry?, find?, and_comm, exists_comm]
+  simp only [contains_iff_findEntry?, Prod.exists, find?, Option.map_eq_some', and_comm,
+    exists_eq_left]
+  rw [exists_comm]
 
 theorem size_eq (t : RBMap α β cmp) : t.size = t.toList.length := RBNode.size_eq
 

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-08-12
+leanprover/lean4:nightly-2024-08-16
diff --git a/test/where.lean b/test/where.lean
@@ -2,7 +2,7 @@ import Batteries.Tactic.Where
 
 -- Return to pristine state
 set_option linter.missingDocs false
-set_option internal.minimalSnapshots false
+set_option internal.cmdlineSnapshots false
 
 /-- info: -- In root namespace with initial scope -/
 #guard_msgs in #where
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:nightly-2024-08-12
		leanprover/lean4:nightly-2024-08-16