theorem List.eq_of_append_eq (s₁ s₂ t₁ t₂ : List Char) (le : String.utf8Len s₁ ≤ String.utf8Len t₁) (eq : s₁ ++ s₂ = t₁ ++ t₂) : ∃ (u : List Char), s₁ ++ u = t₁ ∧ s₂ = u ++ t₂

theorem String.eq_of_append_eq {s₁ s₂ t₁ t₂ : String} (le : s₁.utf8ByteSize ≤ t₁.utf8ByteSize) (eq : s₁ ++ s₂ = t₁ ++ t₂) : ∃ (u : String), s₁ ++ u = t₁ ∧ s₂ = u ++ t₂

theorem String.empty_or_eq_singleton_append (s : String) : s = "" ∨ ∃ (c : Char), ∃ (t : String), s = singleton c ++ t

theorem Regex.Data.String.find_le_pos {s : String} {pos : s.Pos} {p : Char → Bool} : pos ≤ find pos p

theorem Regex.Data.String.find_soundness {s : String} {pos : s.Pos} {p : Char → Bool} : (∃ (h : find pos p ≠ s.endPos), p ((find pos p).get h) = true) ∨ find pos p = s.endPos

theorem Regex.Data.String.find_completeness {s : String} {pos pos' : s.Pos} {p : Char → Bool} (ge : pos ≤ pos') (lt : pos' < find pos p) : ¬p (pos'.get ⋯) = true