fix

Author: Rob23oba

Batteries/Data/String/Lemmas.lean

@@ -224,22 +224,20 @@ theorem utf8PrevAux_of_valid {cs cs' : List Char} {c : Char} {i p : Nat}
     simp only [utf8PrevAux, List.cons_append, utf8Len_cons, ← hp]
     rw [if_neg]
     case hnc =>
-      simp only [Pos.ext_iff]
-      rw [Nat.add_right_comm, Nat.add_left_comm]
-      apply ne_add_utf8Size_add_self
+      simp only [Pos.le_iff, pos_add_char]
+      grind [Char.utf8Size_pos]
     refine (utf8PrevAux_of_valid (by simp [Nat.add_assoc, Nat.add_left_comm])).trans ?_
     simp [Nat.add_assoc, Nat.add_comm]
 
 theorem prev_of_valid (cs : List Char) (c : Char) (cs' : List Char) :
     prev ⟨cs ++ c :: cs'⟩ ⟨utf8Len cs + c.utf8Size⟩ = ⟨utf8Len cs⟩ := by
   simp only [prev]
-  refine (if_neg (Pos.ne_of_gt add_utf8Size_pos)).trans ?_
   rw [utf8PrevAux_of_valid] <;> simp
 
 theorem prev_of_valid' (cs cs' : List Char) :
     prev ⟨cs ++ cs'⟩ ⟨utf8Len cs⟩ = ⟨utf8Len cs.dropLast⟩ := by
   match cs, cs.eq_nil_or_concat with
-  | _, .inl rfl => rfl
+  | _, .inl rfl => apply prev_zero
   | _, .inr ⟨cs, c, rfl⟩ => simp [prev_of_valid]
 
 theorem front_eq (s : String) : front s = s.1.headD default := by