l mr lm r : List Char
e : lm ++ r = l ++ mr
h : utf8Len l ≤ utf8Len lm
⊢ ∃ l_1 m r,
    ValidFor l_1 m r
      { str := { data := l ++ mr }, startPos := { byteIdx := utf8Len l }, stopPos := { byteIdx := utf8Len lm } }
l mr lm r : List Char
e :
  lm ++ r =
    { str := { data := l ++ mr }, startPos := { byteIdx := utf8ByteSize.go l },
          stopPos := { byteIdx := utf8ByteSize.go lm } }.str.data
h :
  { str := { data := l ++ mr }, startPos := { byteIdx := utf8ByteSize.go l },
        stopPos := { byteIdx := utf8ByteSize.go lm } }.startPos ≤
    { str := { data := l ++ mr }, startPos := { byteIdx := utf8ByteSize.go l },
        stopPos := { byteIdx := utf8ByteSize.go lm } }.stopPos
⊢ ∃ l_1 m r,
    ValidFor l_1 m r
      { str := { data := l ++ mr }, startPos := { byteIdx := utf8ByteSize.go l },
        stopPos := { byteIdx := utf8ByteSize.go lm } }
simp at *
l mr lm r : List Char
e : lm ++ r = l ++ mr
h : utf8Len l ≤ utf8Len lm
this : ∃ c', lm = l ++ c' ∧ mr = c' ++ r
⊢ ∃ l_1 m r,
    ValidFor l_1 m r
      { str := { data := l ++ mr }, startPos := { byteIdx := utf8Len l }, stopPos := { byteIdx := utf8Len lm } }

case x
l mr lm r : List Char
e : lm ++ r = l ++ mr
h✝ : utf8Len l ≤ utf8Len lm
h : ∃ a', l = lm ++ a' ∧ r = a' ++ mr
⊢ ∃ c', lm = l ++ c' ∧ mr = c' ++ r
l mr lm r : List Char
e : lm ++ r = l ++ mr
h : utf8Len l ≤ utf8Len lm
⊢ ∃ l_1 m r,
    ValidFor l_1 m r
      { str := { data := l ++ mr }, startPos := { byteIdx := utf8Len l }, stopPos := { byteIdx := utf8Len lm } }
have := (or_iff_right_iff_imp.2 fun h => ?x).1 (List.append_eq_append_iff.1 e)
l mr lm r : List Char
e : lm ++ r = l ++ mr
h : utf8Len l ≤ utf8Len lm
this : ∃ c', lm = l ++ c' ∧ mr = c' ++ r
⊢ ∃ l_1 m r,
    ValidFor l_1 m r
      { str := { data := l ++ mr }, startPos := { byteIdx := utf8Len l }, stopPos := { byteIdx := utf8Len lm } }
l mr lm r : List Char
e : lm ++ r = l ++ mr
h : utf8Len l ≤ utf8Len lm
this : ∃ c', lm = l ++ c' ∧ mr = c' ++ r
⊢ ∃ l_1 m r,
    ValidFor l_1 m r
      { str := { data := l ++ mr }, startPos := { byteIdx := utf8Len l }, stopPos := { byteIdx := utf8Len lm } }

case x
l mr lm r : List Char
e : lm ++ r = l ++ mr
h✝ : utf8Len l ≤ utf8Len lm
h : ∃ a', l = lm ++ a' ∧ r = a' ++ mr
⊢ ∃ c', lm = l ++ c' ∧ mr = c' ++ r
case x =>
  match l, r, h with | _, _, ⟨m, rfl, rfl⟩ => ?_
  simp at h
  cases utf8Len_eq_zero.1 <| Nat.le_zero.1 (Nat.le_of_add_le_add_left (c := 0) h)
  exact ⟨[], by simp⟩
no goals
l mr lm r : List Char
e : lm ++ r = l ++ mr
h : utf8Len l ≤ utf8Len lm
this : ∃ c', lm = l ++ c' ∧ mr = c' ++ r
⊢ ∃ l_1 m r,
    ValidFor l_1 m r
      { str := { data := l ++ mr }, startPos := { byteIdx := utf8Len l }, stopPos := { byteIdx := utf8Len lm } }
match lm, mr, this with
| _, _, ⟨m, rfl, rfl⟩ => exact ⟨l, m, r, by simpa using ValidFor.mk⟩
l mr lm r : List Char
h✝ : ∃ a', l = lm ++ a' ∧ r = a' ++ mr
m : List Char
e : lm ++ (m ++ mr) = lm ++ m ++ mr
h : utf8Len (lm ++ m) ≤ utf8Len lm
⊢ ∃ c', lm = lm ++ m ++ c' ∧ mr = c' ++ (m ++ mr)
l mr lm r : List Char
e : lm ++ r = l ++ mr
h✝ : utf8Len l ≤ utf8Len lm
h : ∃ a', l = lm ++ a' ∧ r = a' ++ mr
⊢ ∃ c', lm = l ++ c' ∧ mr = c' ++ r
match l, r, h with | _, _, ⟨m, rfl, rfl⟩ => ?_
l mr lm r : List Char
h✝ : ∃ a', l = lm ++ a' ∧ r = a' ++ mr
m : List Char
e : lm ++ (m ++ mr) = lm ++ m ++ mr
h : utf8Len lm + utf8Len m ≤ utf8Len lm
⊢ ∃ c', lm = lm ++ m ++ c' ∧ mr = c' ++ (m ++ mr)
l mr lm r : List Char
h✝ : ∃ a', l = lm ++ a' ∧ r = a' ++ mr
m : List Char
e : lm ++ (m ++ mr) = lm ++ m ++ mr
h : utf8Len (lm ++ m) ≤ utf8Len lm
⊢ ∃ c', lm = lm ++ m ++ c' ∧ mr = c' ++ (m ++ mr)
simp at h
case refl
l mr lm r : List Char
h✝ : ∃ a', l = lm ++ a' ∧ r = a' ++ mr
e : lm ++ ([] ++ mr) = lm ++ [] ++ mr
h : utf8Len lm + utf8Len [] ≤ utf8Len lm
⊢ ∃ c', lm = lm ++ [] ++ c' ∧ mr = c' ++ ([] ++ mr)
l mr lm r : List Char
h✝ : ∃ a', l = lm ++ a' ∧ r = a' ++ mr
m : List Char
e : lm ++ (m ++ mr) = lm ++ m ++ mr
h : utf8Len lm + utf8Len m ≤ utf8Len lm
⊢ ∃ c', lm = lm ++ m ++ c' ∧ mr = c' ++ (m ++ mr)
cases utf8Len_eq_zero.1 <| Nat.le_zero.1 (Nat.le_of_add_le_add_left (c := 0) h)
no goals
case refl
l mr lm r : List Char
h✝ : ∃ a', l = lm ++ a' ∧ r = a' ++ mr
e : lm ++ ([] ++ mr) = lm ++ [] ++ mr
h : utf8Len lm + utf8Len [] ≤ utf8Len lm
⊢ ∃ c', lm = lm ++ [] ++ c' ∧ mr = c' ++ ([] ++ mr)
exact ⟨[], by simp⟩
no goals
l mr lm r : List Char
h✝ : ∃ a', l = lm ++ a' ∧ r = a' ++ mr
e : lm ++ ([] ++ mr) = lm ++ [] ++ mr
h : utf8Len lm + utf8Len [] ≤ utf8Len lm
⊢ lm = lm ++ [] ++ [] ∧ mr = [] ++ ([] ++ mr)
simp
no goals
l mr lm r : List Char
this : ∃ c', lm = l ++ c' ∧ mr = c' ++ r
m : List Char
e : l ++ m ++ r = l ++ (m ++ r)
h : utf8Len l ≤ utf8Len (l ++ m)
⊢ ∃ l_1 m_1 r_1,
    ValidFor l_1 m_1 r_1
      { str := { data := l ++ (m ++ r) }, startPos := { byteIdx := utf8Len l },
        stopPos := { byteIdx := utf8Len (l ++ m) } }
exact ⟨l, m, r, by simpa using ValidFor.mk⟩
no goals
l mr lm r : List Char
this : ∃ c', lm = l ++ c' ∧ mr = c' ++ r
m : List Char
e : l ++ m ++ r = l ++ (m ++ r)
h : utf8Len l ≤ utf8Len (l ++ m)
⊢ ValidFor l m r
    { str := { data := l ++ (m ++ r) }, startPos := { byteIdx := utf8Len l },
      stopPos := { byteIdx := utf8Len (l ++ m) } }
simpa using ValidFor.mk