Remove redundant hypotheses

Author: TwoFX

src/Init/Data/String/Lemmas/Basic.lean

@@ -27,4 +27,16 @@ theorem singleton_append_inj : singleton c ++ s = singleton d ++ t ↔ c = d ∧
 theorem push_inj : push s c = push t d ↔ s = t ∧ c = d := by
   simp [← toList_inj]
 
+@[simp]
+theorem append_eq_empty_iff {s t : String} : s ++ t = "" ↔ s = "" ∧ t = "" := by
+  rw [← toList_inj]; simp
+
+@[simp]
+theorem push_ne_empty : push s c ≠ "" := by
+  rw [ne_eq, ← toList_inj]; simp
+
+@[simp]
+theorem singleton_ne_empty {c : Char} : singleton c ≠ "" := by
+  simp [singleton]
+
 end String

src/Init/Data/String/Lemmas/Modify.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Init.Data.String.Modify
 import all Init.Data.String.Modify
+import Init.Data.String.Lemmas.Basic
 
 /-!
 # Lemmas for `Init.Data.String.Modify`
@@ -21,28 +22,28 @@ public section
 
 namespace String
 
--- TODO: `hp` actually follows from `h`.
 /-- You might want to invoke `ValidPos.Splits.exists_eq_singleton_append` to be able to apply this. -/
-theorem ValidPos.Splits.pastSet {s : String} {p : s.ValidPos} {t₁ t₂ : String} (hp : p ≠ s.endValidPos)
+theorem ValidPos.Splits.pastSet {s : String} {p : s.ValidPos} {t₁ t₂ : String}
     {c d : Char} (h : p.Splits t₁ (singleton c ++ t₂)) :
-    (p.pastSet d hp).Splits (t₁ ++ singleton d) t₂ := by
+    (p.pastSet d h.ne_endValidPos_of_singleton).Splits (t₁ ++ singleton d) t₂ := by
+  generalize h.ne_endValidPos_of_singleton = hp
   obtain ⟨rfl, rfl, rfl⟩ := by simpa using h.eq (p.splits_next_right hp)
   apply splits_pastSet
 
--- TODO: `hp` actually follows from `h`.
 /-- You might want to invoke `ValidPos.Splits.exists_eq_singleton_append` to be able to apply this. -/
-theorem ValidPos.Splits.pastModify {s : String} {p : s.ValidPos} {t₁ t₂ : String} (hp : p ≠ s.endValidPos)
+theorem ValidPos.Splits.pastModify {s : String} {p : s.ValidPos} {t₁ t₂ : String}
     {c : Char} (h : p.Splits t₁ (singleton c ++ t₂)) :
-    (p.pastModify f hp).Splits (t₁ ++ singleton (f (p.get hp))) t₂ :=
-  h.pastSet hp
+    (p.pastModify f h.ne_endValidPos_of_singleton).Splits
+    (t₁ ++ singleton (f (p.get h.ne_endValidPos_of_singleton))) t₂ :=
+  h.pastSet
 
 theorem toList_mapAux {f : Char → Char} {s : String} {p : s.ValidPos}
     (h : p.Splits t₁ t₂) : (mapAux f s p).toList = t₁.toList ++ t₂.toList.map f := by
   fun_induction mapAux generalizing t₁ t₂ with
   | case1 s => simp_all
   | case2 s p hp ih =>
     obtain ⟨c, rfl⟩ := h.exists_eq_singleton_append hp
-    simp [ih (h.pastModify hp)]
+    simp [ih h.pastModify]
 
 @[simp]
 theorem toList_map {f : Char → Char} {s : String} : (s.map f).toList = s.toList.map f := by

src/Init/Data/String/Lemmas/Splits.lean

@@ -143,10 +143,19 @@ theorem ValidPos.Splits.exists_eq_append_singleton {s : String} {p : s.ValidPos}
     (hp : p ≠ s.endValidPos) (h : (p.next hp).Splits t₁ t₂) : ∃ t₁', t₁ = t₁' ++ singleton (p.get hp) :=
   ⟨(s.replaceEnd p).copy, h.eq_left (p.splits_next hp)⟩
 
--- TODO: `hp` actually follows from `h`.
+theorem ValidPos.Splits.eq_endValidPos_iff {s : String} {p : s.ValidPos} (h : p.Splits t₁ t₂) :
+    p = s.endValidPos ↔ t₂ = "" :=
+  ⟨fun h' => h.eq_right (h' ▸ s.splits_endValidPos),
+   by rintro rfl; simp [ValidPos.ext_iff, h.offset_eq_rawEndPos, h.eq_append] ⟩
+
+theorem ValidPos.Splits.ne_endValidPos_of_singleton {s : String} {p : s.ValidPos}
+    (h : p.Splits t₁ (singleton c ++ t₂)) : p ≠ s.endValidPos := by
+  simp [h.eq_endValidPos_iff]
+
 /-- You might want to invoke `ValidPos.Splits.exists_eq_singleton_append` to be able to apply this. -/
-theorem ValidPos.Splits.next {s : String} {p : s.ValidPos} (h : p.Splits t₁ (singleton c ++ t₂))
-    (hp : p ≠ s.endValidPos) : (p.next hp).Splits (t₁ ++ singleton c) t₂ := by
+theorem ValidPos.Splits.next {s : String} {p : s.ValidPos}
+    (h : p.Splits t₁ (singleton c ++ t₂)) : (p.next h.ne_endValidPos_of_singleton).Splits (t₁ ++ singleton c) t₂ := by
+  generalize h.ne_endValidPos_of_singleton = hp
   obtain ⟨rfl, rfl, rfl⟩ := by simpa using h.eq (splits_next_right p hp)
   exact splits_next p hp