-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem extract : ∀ {s}, ValidFor l m r s → ValidFor ml mm mr ⟨⟨m⟩, b, e⟩ →
    ∃ l' r', ValidFor l' mm r' (s.extract b e)
  | _, ⟨⟩, ⟨⟩ => by
    simp only [Substring.extract, ge_iff_le, Pos.mk_le_mk, List.append_assoc, utf8Len_append]
    split
    · next h =>
      rw [utf8Len_eq_zero.1 <| Nat.le_zero.1 <| Nat.add_le_add_iff_left.1 h]
      exact ⟨[], [], ⟨⟩⟩
    · next h =>
      refine ⟨l ++ ml, mr ++ r, .of_eq _ (by simp) ?_ ?_⟩ <;>
        simp only [Pos.add_byteIdx, Nat.min_eq_min, utf8Len_append]
          <;> rw [Nat.min_eq_right]
          <;> try simp [Nat.add_le_add_iff_left, Nat.le_add_right]
      rw [Nat.add_assoc]

Proof state:
l m r ml mm mr : List Char
b e : Pos
⊢ ∃ l' r',
    ValidFor l' mm r'
      ({ str := { data := l ++ (ml ++ mm ++ mr) ++ r }, startPos := { byteIdx := utf8Len l },
            stopPos := { byteIdx := utf8Len l + utf8Len (ml ++ mm ++ mr) } }.extract
        { byteIdx := utf8Len ml } { byteIdx := utf8Len ml + utf8Len mm })

Tactic:
simp only [Substring.extract, ge_iff_le, Pos.mk_le_mk, List.append_assoc, utf8Len_append]

Result:
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 :=
            { byteIdx := utf8Len l + (utf8Len ml + (utf8Len mm + utf8Len mr)) }.min
              ({ byteIdx := utf8Len l } + { byteIdx := utf8Len ml }),
          stopPos :=
            { byteIdx := utf8Len l + (utf8Len ml + (utf8Len mm + utf8Len mr)) }.min
              ({ byteIdx := utf8Len l } + { byteIdx := utf8Len ml + utf8Len mm }) })

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

Tactic:
rw [utf8Len_eq_zero.1 <| Nat.le_zero.1 <| Nat.add_le_add_iff_left.1 h]

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

Proof state:
case isFalse
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 :=
          { byteIdx := utf8Len l + (utf8Len ml + (utf8Len mm + utf8Len mr)) }.min
            ({ byteIdx := utf8Len l } + { byteIdx := utf8Len ml }),
        stopPos :=
          { byteIdx := utf8Len l + (utf8Len ml + (utf8Len mm + utf8Len mr)) }.min
            ({ byteIdx := utf8Len l } + { byteIdx := utf8Len ml + utf8Len mm }) }

Tactic:
next h =>
refine ⟨l ++ ml, mr ++ r, .of_eq _ (by simp) ?_ ?_⟩ <;>
  simp only [Pos.add_byteIdx, Nat.min_eq_min, utf8Len_append]
    <;> rw [Nat.min_eq_right]
    <;> try simp [Nat.add_le_add_iff_left, Nat.le_add_right]
rw [Nat.add_assoc]

Result:
no goals

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

Tactic:
next h =>
rw [utf8Len_eq_zero.1 <| Nat.le_zero.1 <| Nat.add_le_add_iff_left.1 h]
exact ⟨[], [], ⟨⟩⟩

Result:
no goals

Proof state:
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 :=
            { byteIdx := utf8Len l + (utf8Len ml + (utf8Len mm + utf8Len mr)) }.min
              ({ byteIdx := utf8Len l } + { byteIdx := utf8Len ml }),
          stopPos :=
            { byteIdx := utf8Len l + (utf8Len ml + (utf8Len mm + utf8Len mr)) }.min
              ({ byteIdx := utf8Len l } + { byteIdx := utf8Len ml + utf8Len mm }) })

Tactic:
split

Result:
case isTrue
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 isFalse
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 :=
          { byteIdx := utf8Len l + (utf8Len ml + (utf8Len mm + utf8Len mr)) }.min
            ({ byteIdx := utf8Len l } + { byteIdx := utf8Len ml }),
        stopPos :=
          { byteIdx := utf8Len l + (utf8Len ml + (utf8Len mm + utf8Len mr)) }.min
            ({ byteIdx := utf8Len l } + { byteIdx := utf8Len ml + utf8Len mm }) }

Proof state:
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 :=
            { byteIdx := utf8Len l + (utf8Len ml + (utf8Len mm + utf8Len mr)) }.min
              ({ byteIdx := utf8Len l } + { byteIdx := utf8Len ml }),
          stopPos :=
            { byteIdx := utf8Len l + (utf8Len ml + (utf8Len mm + utf8Len mr)) }.min
              ({ byteIdx := utf8Len l } + { byteIdx := utf8Len ml + utf8Len mm }) }.str.data =
    l ++ ml ++ mm ++ (mr ++ r)

Tactic:
simp

Result:
no goals

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

Tactic:
simp [Nat.add_le_add_iff_left, Nat.le_add_right]

Result:
no goals

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

Tactic:
rw [Nat.add_assoc]

Result:
no goals

Proof state:
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 :=
          { byteIdx := utf8Len l + (utf8Len ml + (utf8Len mm + utf8Len mr)) }.min
            ({ byteIdx := utf8Len l } + { byteIdx := utf8Len ml }),
        stopPos :=
          { byteIdx := utf8Len l + (utf8Len ml + (utf8Len mm + utf8Len mr)) }.min
            ({ byteIdx := utf8Len l } + { byteIdx := utf8Len ml + utf8Len mm }) }

Tactic:
refine ⟨l ++ ml, mr ++ r, .of_eq _ (by simp) ?_ ?_⟩ <;>
  simp only [Pos.add_byteIdx, Nat.min_eq_min, utf8Len_append]
    <;> rw [Nat.min_eq_right]
    <;> try simp [Nat.add_le_add_iff_left, Nat.le_add_right]

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

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

Tactic:
exact ⟨[], [], ⟨⟩⟩

Result:
no goals