chore: make proofs robust to incoming changes (#929)

leanprover-community · Aug 27, 2024 · e6d3a32 · e6d3a32
1 parent 31fb27d
commit e6d3a32
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean
@@ -586,7 +586,7 @@ theorem indexOf_mem_indexesOf [BEq α] [LawfulBEq α] {xs : List α} (m : x ∈
 theorem insertP_loop (a : α) (l r : List α) :
     insertP.loop p a l r = reverseAux r (insertP p a l) := by
   induction l generalizing r with simp [insertP, insertP.loop, cond]
-  | cons b l ih => rw [ih (b :: r), ih [b]]; split <;> rfl
+  | cons b l ih => rw [ih (b :: r), ih [b]]; split <;> simp
 
 @[simp] theorem insertP_nil (p : α → Bool) (a) : insertP p a [] = [a] := rfl
 

diff --git a/Batteries/Data/String/Lemmas.lean b/Batteries/Data/String/Lemmas.lean
@@ -59,7 +59,7 @@ private theorem ne_self_add_add_utf8Size : i ≠ i + (n + Char.utf8Size c) :=
 
 @[simp] theorem utf8Len_reverseAux (cs₁ cs₂) :
     utf8Len (cs₁.reverseAux cs₂) = utf8Len cs₁ + utf8Len cs₂ := by
-  induction cs₁ generalizing cs₂ <;> simp [*, ← Nat.add_assoc, Nat.add_right_comm]
+  induction cs₁ generalizing cs₂ <;> simp_all [← Nat.add_assoc, Nat.add_right_comm]
 
 @[simp] theorem utf8Len_reverse (cs) : utf8Len cs.reverse = utf8Len cs := utf8Len_reverseAux ..