l m r ml mm mr : List Char
b e : Pos
⊢ ∃ l' r',
    ValidFor l' mm r'
      (if utf8Len ml + utf8Len mm ≤ utf8Len ml then { str := "", startPos := 0, stopPos := 0 }
      else
        { str := { data := l ++ (ml ++ (mm ++ (mr ++ r))) },
          startPos :=
            Pos.min { byteIdx := utf8Len l + (utf8Len ml + (utf8Len mm + utf8Len mr)) }
              ({ byteIdx := utf8Len l } + { byteIdx := utf8Len ml }),
          stopPos :=
            Pos.min { byteIdx := utf8Len l + (utf8Len ml + (utf8Len mm + utf8Len mr)) }
              ({ byteIdx := utf8Len l } + { byteIdx := utf8Len ml + utf8Len mm }) })
l m r ml mm mr : List Char
b e : Pos
⊢ ∃ l' r',
    ValidFor l' mm r'
      (Substring.extract
        { str := { data := l ++ (ml ++ mm ++ mr) ++ r }, startPos := { byteIdx := utf8Len l },
          stopPos := { byteIdx := utf8Len l + utf8Len (ml ++ mm ++ mr) } }
        { byteIdx := utf8Len ml } { byteIdx := utf8Len ml + utf8Len mm })
simp [Substring.extract]
case inl
l m r ml mm mr : List Char
b e : Pos
h✝ : utf8Len ml + utf8Len mm ≤ utf8Len ml
⊢ ∃ l' r', ValidFor l' mm r' { str := "", startPos := 0, stopPos := 0 }

case inr
l m r ml mm mr : List Char
b e : Pos
h✝ : ¬utf8Len ml + utf8Len mm ≤ utf8Len ml
⊢ ∃ l' r',
    ValidFor l' mm r'
      { str := { data := l ++ (ml ++ (mm ++ (mr ++ r))) },
        startPos :=
          Pos.min { byteIdx := utf8Len l + (utf8Len ml + (utf8Len mm + utf8Len mr)) }
            ({ byteIdx := utf8Len l } + { byteIdx := utf8Len ml }),
        stopPos :=
          Pos.min { byteIdx := utf8Len l + (utf8Len ml + (utf8Len mm + utf8Len mr)) }
            ({ byteIdx := utf8Len l } + { byteIdx := utf8Len ml + utf8Len mm }) }
l m r ml mm mr : List Char
b e : Pos
⊢ ∃ l' r',
    ValidFor l' mm r'
      (if utf8Len ml + utf8Len mm ≤ utf8Len ml then { str := "", startPos := 0, stopPos := 0 }
      else
        { str := { data := l ++ (ml ++ (mm ++ (mr ++ r))) },
          startPos :=
            Pos.min { byteIdx := utf8Len l + (utf8Len ml + (utf8Len mm + utf8Len mr)) }
              ({ byteIdx := utf8Len l } + { byteIdx := utf8Len ml }),
          stopPos :=
            Pos.min { byteIdx := utf8Len l + (utf8Len ml + (utf8Len mm + utf8Len mr)) }
              ({ byteIdx := utf8Len l } + { byteIdx := utf8Len ml + utf8Len mm }) })
split
no goals
case inl
l m r ml mm mr : List Char
b e : Pos
h✝ : utf8Len ml + utf8Len mm ≤ utf8Len ml
⊢ ∃ l' r', ValidFor l' mm r' { str := "", startPos := 0, stopPos := 0 }
next h =>
rw [utf8Len_eq_zero.1 <| Nat.le_zero.1 <| (Nat.add_le_add_iff_le_left _ _ 0).1 h]
exact ⟨[], [], ⟨⟩⟩
l m r ml mm mr : List Char
b e : Pos
h : utf8Len ml + utf8Len mm ≤ utf8Len ml
⊢ ∃ l' r', ValidFor l' [] r' { str := "", startPos := 0, stopPos := 0 }
l m r ml mm mr : List Char
b e : Pos
h : utf8Len ml + utf8Len mm ≤ utf8Len ml
⊢ ∃ l' r', ValidFor l' mm r' { str := "", startPos := 0, stopPos := 0 }
rw [utf8Len_eq_zero.1 <| Nat.le_zero.1 <| (Nat.add_le_add_iff_le_left _ _ 0).1 h]
no goals
l m r ml mm mr : List Char
b e : Pos
h : utf8Len ml + utf8Len mm ≤ utf8Len ml
⊢ ∃ l' r', ValidFor l' [] r' { str := "", startPos := 0, stopPos := 0 }
exact ⟨[], [], ⟨⟩⟩
no goals
case inr
l m r ml mm mr : List Char
b e : Pos
h✝ : ¬utf8Len ml + utf8Len mm ≤ utf8Len ml
⊢ ∃ l' r',
    ValidFor l' mm r'
      { str := { data := l ++ (ml ++ (mm ++ (mr ++ r))) },
        startPos :=
          Pos.min { byteIdx := utf8Len l + (utf8Len ml + (utf8Len mm + utf8Len mr)) }
            ({ byteIdx := utf8Len l } + { byteIdx := utf8Len ml }),
        stopPos :=
          Pos.min { byteIdx := utf8Len l + (utf8Len ml + (utf8Len mm + utf8Len mr)) }
            ({ byteIdx := utf8Len l } + { byteIdx := utf8Len ml + utf8Len mm }) }
next h =>
refine ⟨l ++ ml, mr ++ r, .of_eq _ (by simp) ?_ ?_⟩ <;>
  simp [Nat.min_eq_min] <;> rw [Nat.min_eq_right] <;>
  simp [Nat.add_le_add_iff_le_left, Nat.le_add_right]
rw [Nat.add_assoc]
case refine_2
l m r ml mm mr : List Char
b e : Pos
h : ¬utf8Len ml + utf8Len mm ≤ utf8Len ml
⊢ utf8Len l + (utf8Len ml + utf8Len mm) = utf8Len l + utf8Len ml + utf8Len mm
l m r ml mm mr : List Char
b e : Pos
h : ¬utf8Len ml + utf8Len mm ≤ utf8Len ml
⊢ ∃ l' r',
    ValidFor l' mm r'
      { str := { data := l ++ (ml ++ (mm ++ (mr ++ r))) },
        startPos :=
          Pos.min { byteIdx := utf8Len l + (utf8Len ml + (utf8Len mm + utf8Len mr)) }
            ({ byteIdx := utf8Len l } + { byteIdx := utf8Len ml }),
        stopPos :=
          Pos.min { byteIdx := utf8Len l + (utf8Len ml + (utf8Len mm + utf8Len mr)) }
            ({ byteIdx := utf8Len l } + { byteIdx := utf8Len ml + utf8Len mm }) }
refine ⟨l ++ ml, mr ++ r, .of_eq _ (by simp) ?_ ?_⟩ <;>
  simp [Nat.min_eq_min] <;> rw [Nat.min_eq_right] <;>
  simp [Nat.add_le_add_iff_le_left, Nat.le_add_right]
no goals
case refine_2
l m r ml mm mr : List Char
b e : Pos
h : ¬utf8Len ml + utf8Len mm ≤ utf8Len ml
⊢ utf8Len l + (utf8Len ml + utf8Len mm) = utf8Len l + utf8Len ml + utf8Len mm
rw [Nat.add_assoc]
no goals
l m r ml mm mr : List Char
b e : Pos
h : ¬utf8Len ml + utf8Len mm ≤ utf8Len ml
⊢ { str := { data := l ++ (ml ++ (mm ++ (mr ++ r))) },
          startPos :=
            Pos.min { byteIdx := utf8Len l + (utf8Len ml + (utf8Len mm + utf8Len mr)) }
              ({ byteIdx := utf8Len l } + { byteIdx := utf8Len ml }),
          stopPos :=
            Pos.min { byteIdx := utf8Len l + (utf8Len ml + (utf8Len mm + utf8Len mr)) }
              ({ byteIdx := utf8Len l } + { byteIdx := utf8Len ml + utf8Len mm }) }.str.data =
    l ++ ml ++ mm ++ (mr ++ r)
simp