no goals
l m₁ m₂ r : List Char
x✝¹ : Substring
x✝ : ValidFor l (m₁ ++ m₂) r x✝¹
⊢ Substring.nextn x✝¹ 0 { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len m₁ + utf8Len (List.take 0 m₂) }
simp [Substring.nextn]
l m₁ m₂ r : List Char
s : Substring
h : ValidFor l (m₁ ++ m₂) r s
n : Nat
⊢ Substring.nextn s n (Substring.next s { byteIdx := utf8Len m₁ }) =
    { byteIdx := utf8Len m₁ + utf8Len (List.take (n + 1) m₂) }
l m₁ m₂ r : List Char
s : Substring
h : ValidFor l (m₁ ++ m₂) r s
n : Nat
⊢ Substring.nextn s (n + 1) { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len m₁ + utf8Len (List.take (n + 1) m₂) }
simp [Substring.nextn]
no goals
l m₁ m₂ r : List Char
s : Substring
h : ValidFor l (m₁ ++ m₂) r s
n : Nat
⊢ Substring.nextn s n (Substring.next s { byteIdx := utf8Len m₁ }) =
    { byteIdx := utf8Len m₁ + utf8Len (List.take (n + 1) m₂) }
match m₂ with
| [] => simp at h; simp [h.next_stop, h.nextn_stop]
| c::m₂ =>
  rw [h.next]
  have := @nextn l (m₁ ++ [c]) m₂ r s (by simp [h]) n
  simp at this; rw [this]; simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm]
l m₁ m₂ r : List Char
s : Substring
n : Nat
h : ValidFor l m₁ r s
⊢ Substring.nextn s n (Substring.next s { byteIdx := utf8Len m₁ }) =
    { byteIdx := utf8Len m₁ + utf8Len (List.take (n + 1) []) }
l m₁ m₂ r : List Char
s : Substring
n : Nat
h : ValidFor l (m₁ ++ []) r s
⊢ Substring.nextn s n (Substring.next s { byteIdx := utf8Len m₁ }) =
    { byteIdx := utf8Len m₁ + utf8Len (List.take (n + 1) []) }
simp at h
no goals
l m₁ m₂ r : List Char
s : Substring
n : Nat
h : ValidFor l m₁ r s
⊢ Substring.nextn s n (Substring.next s { byteIdx := utf8Len m₁ }) =
    { byteIdx := utf8Len m₁ + utf8Len (List.take (n + 1) []) }
simp [h.next_stop, h.nextn_stop]
l m₁ m₂✝ r : List Char
s : Substring
n : Nat
c : Char
m₂ : List Char
h : ValidFor l (m₁ ++ c :: m₂) r s
⊢ Substring.nextn s n { byteIdx := utf8Len m₁ + csize c } =
    { byteIdx := utf8Len m₁ + utf8Len (List.take (n + 1) (c :: m₂)) }
l m₁ m₂✝ r : List Char
s : Substring
n : Nat
c : Char
m₂ : List Char
h : ValidFor l (m₁ ++ c :: m₂) r s
⊢ Substring.nextn s n (Substring.next s { byteIdx := utf8Len m₁ }) =
    { byteIdx := utf8Len m₁ + utf8Len (List.take (n + 1) (c :: m₂)) }
rw [h.next]
l m₁ m₂✝ r : List Char
s : Substring
n : Nat
c : Char
m₂ : List Char
h : ValidFor l (m₁ ++ c :: m₂) r s
this :
  Substring.nextn s n { byteIdx := utf8Len (m₁ ++ [c]) } = { byteIdx := utf8Len (m₁ ++ [c]) + utf8Len (List.take n m₂) }
⊢ Substring.nextn s n { byteIdx := utf8Len m₁ + csize c } =
    { byteIdx := utf8Len m₁ + utf8Len (List.take (n + 1) (c :: m₂)) }
l m₁ m₂✝ r : List Char
s : Substring
n : Nat
c : Char
m₂ : List Char
h : ValidFor l (m₁ ++ c :: m₂) r s
⊢ Substring.nextn s n { byteIdx := utf8Len m₁ + csize c } =
    { byteIdx := utf8Len m₁ + utf8Len (List.take (n + 1) (c :: m₂)) }
have := @nextn l (m₁ ++ [c]) m₂ r s (by simp [h]) n
l m₁ m₂✝ r : List Char
s : Substring
n : Nat
c : Char
m₂ : List Char
h : ValidFor l (m₁ ++ c :: m₂) r s
this :
  Substring.nextn s n { byteIdx := utf8Len m₁ + csize c } =
    { byteIdx := utf8Len m₁ + csize c + utf8Len (List.take n m₂) }
⊢ Substring.nextn s n { byteIdx := utf8Len m₁ + csize c } =
    { byteIdx := utf8Len m₁ + utf8Len (List.take (n + 1) (c :: m₂)) }
l m₁ m₂✝ r : List Char
s : Substring
n : Nat
c : Char
m₂ : List Char
h : ValidFor l (m₁ ++ c :: m₂) r s
this :
  Substring.nextn s n { byteIdx := utf8Len (m₁ ++ [c]) } = { byteIdx := utf8Len (m₁ ++ [c]) + utf8Len (List.take n m₂) }
⊢ Substring.nextn s n { byteIdx := utf8Len m₁ + csize c } =
    { byteIdx := utf8Len m₁ + utf8Len (List.take (n + 1) (c :: m₂)) }
simp at this
l m₁ m₂✝ r : List Char
s : Substring
n : Nat
c : Char
m₂ : List Char
h : ValidFor l (m₁ ++ c :: m₂) r s
this :
  Substring.nextn s n { byteIdx := utf8Len m₁ + csize c } =
    { byteIdx := utf8Len m₁ + csize c + utf8Len (List.take n m₂) }
⊢ { byteIdx := utf8Len m₁ + csize c + utf8Len (List.take n m₂) } =
    { byteIdx := utf8Len m₁ + utf8Len (List.take (n + 1) (c :: m₂)) }
l m₁ m₂✝ r : List Char
s : Substring
n : Nat
c : Char
m₂ : List Char
h : ValidFor l (m₁ ++ c :: m₂) r s
this :
  Substring.nextn s n { byteIdx := utf8Len m₁ + csize c } =
    { byteIdx := utf8Len m₁ + csize c + utf8Len (List.take n m₂) }
⊢ Substring.nextn s n { byteIdx := utf8Len m₁ + csize c } =
    { byteIdx := utf8Len m₁ + utf8Len (List.take (n + 1) (c :: m₂)) }
rw [this]
no goals
l m₁ m₂✝ r : List Char
s : Substring
n : Nat
c : Char
m₂ : List Char
h : ValidFor l (m₁ ++ c :: m₂) r s
this :
  Substring.nextn s n { byteIdx := utf8Len m₁ + csize c } =
    { byteIdx := utf8Len m₁ + csize c + utf8Len (List.take n m₂) }
⊢ { byteIdx := utf8Len m₁ + csize c + utf8Len (List.take n m₂) } =
    { byteIdx := utf8Len m₁ + utf8Len (List.take (n + 1) (c :: m₂)) }
simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm]
no goals
l m₁ m₂✝ r : List Char
s : Substring
n : Nat
c : Char
m₂ : List Char
h : ValidFor l (m₁ ++ c :: m₂) r s
⊢ ValidFor l (m₁ ++ [c] ++ m₂) r s
simp [h]