-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem validFor : ∀ {s}, Valid s → ∃ l m r, ValidFor l m r s
  | ⟨⟨_⟩, ⟨_⟩, ⟨_⟩⟩, ⟨⟨l, mr, rfl, rfl⟩, ⟨lm, r, e, rfl⟩, h⟩ => by
    simp only [utf8ByteSize.go_eq, Pos.mk_le_mk] at *
    have := (or_iff_right_iff_imp.2 fun h => ?x).1 (List.append_eq_append_iff.1 e)
    case x =>
      match l, r, h with | _, _, ⟨m, rfl, rfl⟩ => ?_
      simp only [utf8Len_append] at h
      cases utf8Len_eq_zero.1 <| Nat.le_zero.1 (Nat.le_of_add_le_add_left (c := 0) h)
      exact ⟨[], by simp⟩
    match lm, mr, this with
    | _, _, ⟨m, rfl, rfl⟩ => exact ⟨l, m, r, by simpa using ValidFor.mk⟩

Proof state:
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)

Tactic:
exact ⟨[], by simp⟩

Result:
no goals

Proof state:
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 } }

Tactic:
match lm, mr, this with
| _, _, ⟨m, rfl, rfl⟩ => exact ⟨l, m, r, by simpa using ValidFor.mk⟩

Result:
no goals

Proof state:
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 } }

Tactic:
have := (or_iff_right_iff_imp.2 fun h => ?x).1 (List.append_eq_append_iff.1 e)

Result:
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

Proof state:
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

Tactic:
match l, r, h with | _, _, ⟨m, rfl, rfl⟩ => ?_

Result:
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)

Proof state:
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) } }

Tactic:
simpa using ValidFor.mk

Result:
no goals

Proof state:
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

Tactic:
case x =>
  match l, r, h with | _, _, ⟨m, rfl, rfl⟩ => ?_
  simp only [utf8Len_append] at h
  cases utf8Len_eq_zero.1 <| Nat.le_zero.1 (Nat.le_of_add_le_add_left (c := 0) h)
  exact ⟨[], by simp⟩

Result:
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 } }

Proof state:
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) } }

Tactic:
exact ⟨l, m, r, by simpa using ValidFor.mk⟩

Result:
no goals

Proof state:
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 } }

Tactic:
simp only [utf8ByteSize.go_eq, Pos.mk_le_mk] at *

Result:
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 } }

Proof state:
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)

Tactic:
simp only [utf8Len_append] at h

Result:
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)

Proof state:
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)

Tactic:
simp

Result:
no goals

Proof state:
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)

Tactic:
cases utf8Len_eq_zero.1 <| Nat.le_zero.1 (Nat.le_of_add_le_add_left (c := 0) h)

Result:
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)