-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem take : ∀ {s}, ValidFor l m r s → ∀ n, ValidFor l (m.take n) (m.drop n ++ r) (s.take n)
  | s, h, n => by
    have : Substring.nextn {..} .. = _ := h.nextn (m₁ := []) n
    simp at this
    simp only [Substring.take, this]
    simp only [h.str, List.append_assoc, h.startPos]
    rw [← List.take_append_drop n m] at h
    refine .of_eq _ ?_ (by simp) (by simp)
    conv => lhs; rw [← List.take_append_drop n m]
    simp [-List.take_append_drop, Nat.add_assoc]

Proof state:
l m r : List Char
s : Substring
n : Nat
h : ValidFor l (List.take n m ++ List.drop n m) r s
this : { str := s.str, startPos := s.startPos, stopPos := s.stopPos }.nextn n 0 = { byteIdx := utf8Len (List.take n m) }
⊢ { str := { data := l ++ (m ++ r) }, startPos := { byteIdx := utf8Len l },
          stopPos := { byteIdx := utf8Len l } + { byteIdx := utf8Len (List.take n m) } }.stopPos.byteIdx =
    utf8Len l + utf8Len (List.take n m)

Tactic:
simp

Result:
no goals

Proof state:
l m r : List Char
s : Substring
h : ValidFor l m r s
n : Nat
this :
  { str := s.str, startPos := s.startPos, stopPos := s.stopPos }.nextn n { byteIdx := utf8Len [] } =
    { byteIdx := utf8Len [] + utf8Len (List.take n m) }
⊢ ValidFor l (List.take n m) (List.drop n m ++ r) (s.take n)

Tactic:
simp at this

Result:
l m r : List Char
s : Substring
h : ValidFor l m r s
n : Nat
this : { str := s.str, startPos := s.startPos, stopPos := s.stopPos }.nextn n 0 = { byteIdx := utf8Len (List.take n m) }
⊢ ValidFor l (List.take n m) (List.drop n m ++ r) (s.take n)

Proof state:
l m r : List Char
s : Substring
n : Nat
h : ValidFor l (List.take n m ++ List.drop n m) r s
this : { str := s.str, startPos := s.startPos, stopPos := s.stopPos }.nextn n 0 = { byteIdx := utf8Len (List.take n m) }
⊢ ValidFor l (List.take n m) (List.drop n m ++ r)
    { str := { data := l ++ (m ++ r) }, startPos := { byteIdx := utf8Len l },
      stopPos := { byteIdx := utf8Len l } + { byteIdx := utf8Len (List.take n m) } }

Tactic:
refine .of_eq _ ?_ (by simp) (by simp)

Result:
l m r : List Char
s : Substring
n : Nat
h : ValidFor l (List.take n m ++ List.drop n m) r s
this : { str := s.str, startPos := s.startPos, stopPos := s.stopPos }.nextn n 0 = { byteIdx := utf8Len (List.take n m) }
⊢ { str := { data := l ++ (m ++ r) }, startPos := { byteIdx := utf8Len l },
          stopPos := { byteIdx := utf8Len l } + { byteIdx := utf8Len (List.take n m) } }.str.data =
    l ++ List.take n m ++ (List.drop n m ++ r)

Proof state:
l m r : List Char
s : Substring
n : Nat
h : ValidFor l (List.take n m ++ List.drop n m) r s
this : { str := s.str, startPos := s.startPos, stopPos := s.stopPos }.nextn n 0 = { byteIdx := utf8Len (List.take n m) }
⊢ { str := { data := l ++ (List.take n m ++ List.drop n m ++ r) }, startPos := { byteIdx := utf8Len l },
          stopPos :=
            { byteIdx := utf8Len l } +
              { byteIdx := utf8Len (List.take n (List.take n m ++ List.drop n m)) } }.str.data =
    l ++ List.take n m ++ (List.drop n m ++ r)

Tactic:
simp [-List.take_append_drop, Nat.add_assoc]

Result:
no goals

Proof state:
l m r : List Char
s : Substring
n : Nat
h : ValidFor l (List.take n m ++ List.drop n m) r s
this : { str := s.str, startPos := s.startPos, stopPos := s.stopPos }.nextn n 0 = { byteIdx := utf8Len (List.take n m) }
⊢ { str := { data := l ++ (m ++ r) }, startPos := { byteIdx := utf8Len l },
          stopPos := { byteIdx := utf8Len l } + { byteIdx := utf8Len (List.take n m) } }.str.data =
    l ++ List.take n m ++ (List.drop n m ++ r)

Tactic:
conv => lhs; rw [← List.take_append_drop n m]

Result:
l m r : List Char
s : Substring
n : Nat
h : ValidFor l (List.take n m ++ List.drop n m) r s
this : { str := s.str, startPos := s.startPos, stopPos := s.stopPos }.nextn n 0 = { byteIdx := utf8Len (List.take n m) }
⊢ { str := { data := l ++ (List.take n m ++ List.drop n m ++ r) }, startPos := { byteIdx := utf8Len l },
          stopPos :=
            { byteIdx := utf8Len l } +
              { byteIdx := utf8Len (List.take n (List.take n m ++ List.drop n m)) } }.str.data =
    l ++ List.take n m ++ (List.drop n m ++ r)

Proof state:
l m r : List Char
s : Substring
h : ValidFor l m r s
n : Nat
this : { str := s.str, startPos := s.startPos, stopPos := s.stopPos }.nextn n 0 = { byteIdx := utf8Len (List.take n m) }
⊢ ValidFor l (List.take n m) (List.drop n m ++ r) (s.take n)

Tactic:
simp only [Substring.take, this]

Result:
l m r : List Char
s : Substring
h : ValidFor l m r s
n : Nat
this : { str := s.str, startPos := s.startPos, stopPos := s.stopPos }.nextn n 0 = { byteIdx := utf8Len (List.take n m) }
⊢ ValidFor l (List.take n m) (List.drop n m ++ r)
    { str := s.str, startPos := s.startPos, stopPos := s.startPos + { byteIdx := utf8Len (List.take n m) } }

Proof state:
l m r : List Char
s : Substring
h : ValidFor l m r s
n : Nat
this : { str := s.str, startPos := s.startPos, stopPos := s.stopPos }.nextn n 0 = { byteIdx := utf8Len (List.take n m) }
⊢ ValidFor l (List.take n m) (List.drop n m ++ r)
    { str := { data := l ++ (m ++ r) }, startPos := { byteIdx := utf8Len l },
      stopPos := { byteIdx := utf8Len l } + { byteIdx := utf8Len (List.take n m) } }

Tactic:
rw [← List.take_append_drop n m] at h

Result:
l m r : List Char
s : Substring
n : Nat
h : ValidFor l (List.take n m ++ List.drop n m) r s
this : { str := s.str, startPos := s.startPos, stopPos := s.stopPos }.nextn n 0 = { byteIdx := utf8Len (List.take n m) }
⊢ ValidFor l (List.take n m) (List.drop n m ++ r)
    { str := { data := l ++ (m ++ r) }, startPos := { byteIdx := utf8Len l },
      stopPos := { byteIdx := utf8Len l } + { byteIdx := utf8Len (List.take n m) } }

Proof state:
l m r : List Char
s : Substring
h : ValidFor l m r s
n : Nat
this : { str := s.str, startPos := s.startPos, stopPos := s.stopPos }.nextn n 0 = { byteIdx := utf8Len (List.take n m) }
⊢ ValidFor l (List.take n m) (List.drop n m ++ r)
    { str := s.str, startPos := s.startPos, stopPos := s.startPos + { byteIdx := utf8Len (List.take n m) } }

Tactic:
simp only [h.str, List.append_assoc, h.startPos]

Result:
l m r : List Char
s : Substring
h : ValidFor l m r s
n : Nat
this : { str := s.str, startPos := s.startPos, stopPos := s.stopPos }.nextn n 0 = { byteIdx := utf8Len (List.take n m) }
⊢ ValidFor l (List.take n m) (List.drop n m ++ r)
    { str := { data := l ++ (m ++ r) }, startPos := { byteIdx := utf8Len l },
      stopPos := { byteIdx := utf8Len l } + { byteIdx := utf8Len (List.take n m) } }

Proof state:
l m r : List Char
s : Substring
n : Nat
h : ValidFor l (List.take n m ++ List.drop n m) r s
this : { str := s.str, startPos := s.startPos, stopPos := s.stopPos }.nextn n 0 = { byteIdx := utf8Len (List.take n m) }
⊢ { str := { data := l ++ (m ++ r) }, startPos := { byteIdx := utf8Len l },
          stopPos := { byteIdx := utf8Len l } + { byteIdx := utf8Len (List.take n m) } }.startPos.byteIdx =
    utf8Len l

Tactic:
simp

Result:
no goals

Proof state:
l m r : List Char
s : Substring
h : ValidFor l m r s
n : Nat
⊢ ValidFor l (List.take n m) (List.drop n m ++ r) (s.take n)

Tactic:
have : Substring.nextn {..} .. = _ := h.nextn (m₁ := []) n

Result:
l m r : List Char
s : Substring
h : ValidFor l m r s
n : Nat
this :
  { str := s.str, startPos := s.startPos, stopPos := s.stopPos }.nextn n { byteIdx := utf8Len [] } =
    { byteIdx := utf8Len [] + utf8Len (List.take n m) }
⊢ ValidFor l (List.take n m) (List.drop n m ++ r) (s.take n)