no goals
l m₂ r m₁ : List Char
x✝¹ : Substring
x✝ : ValidFor l (List.reverse m₁ ++ m₂) r x✝¹
⊢ Substring.prevn x✝¹ 0 { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len (List.drop 0 m₁) }
simp [Substring.prevn]
l m₂ r m₁ : List Char
s : Substring
h : ValidFor l (List.reverse m₁ ++ m₂) r s
n : Nat
⊢ Substring.prevn s n (Substring.prev s { byteIdx := utf8Len m₁ }) = { byteIdx := utf8Len (List.drop (n + 1) m₁) }
l m₂ r m₁ : List Char
s : Substring
h : ValidFor l (List.reverse m₁ ++ m₂) r s
n : Nat
⊢ Substring.prevn s (n + 1) { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len (List.drop (n + 1) m₁) }
simp [Substring.prevn]
no goals
l m₂ r m₁ : List Char
s : Substring
h : ValidFor l (List.reverse m₁ ++ m₂) r s
n : Nat
⊢ Substring.prevn s n (Substring.prev s { byteIdx := utf8Len m₁ }) = { byteIdx := utf8Len (List.drop (n + 1) m₁) }
match m₁ with
| [] => simp
| c::m₁ =>
  rw [List.reverse_cons, List.append_assoc] at h
  have := h.prev; simp at this; simp [this, h.prevn n]
no goals
l m₂ r m₁ : List Char
s : Substring
n : Nat
h : ValidFor l (List.reverse [] ++ m₂) r s
⊢ Substring.prevn s n (Substring.prev s { byteIdx := utf8Len [] }) = { byteIdx := utf8Len (List.drop (n + 1) []) }
simp
l m₂ r m₁✝ : List Char
s : Substring
n : Nat
c : Char
m₁ : List Char
h : ValidFor l (List.reverse m₁ ++ ([c] ++ m₂)) r s
⊢ Substring.prevn s n (Substring.prev s { byteIdx := utf8Len (c :: m₁) }) =
    { byteIdx := utf8Len (List.drop (n + 1) (c :: m₁)) }
l m₂ r m₁✝ : List Char
s : Substring
n : Nat
c : Char
m₁ : List Char
h : ValidFor l (List.reverse (c :: m₁) ++ m₂) r s
⊢ Substring.prevn s n (Substring.prev s { byteIdx := utf8Len (c :: m₁) }) =
    { byteIdx := utf8Len (List.drop (n + 1) (c :: m₁)) }
rw [List.reverse_cons, List.append_assoc] at h
l m₂ r m₁✝ : List Char
s : Substring
n : Nat
c : Char
m₁ : List Char
h : ValidFor l (List.reverse m₁ ++ ([c] ++ m₂)) r s
this : Substring.prev s { byteIdx := utf8Len (List.reverse m₁) + csize c } = { byteIdx := utf8Len (List.reverse m₁) }
⊢ Substring.prevn s n (Substring.prev s { byteIdx := utf8Len (c :: m₁) }) =
    { byteIdx := utf8Len (List.drop (n + 1) (c :: m₁)) }
l m₂ r m₁✝ : List Char
s : Substring
n : Nat
c : Char
m₁ : List Char
h : ValidFor l (List.reverse m₁ ++ ([c] ++ m₂)) r s
⊢ Substring.prevn s n (Substring.prev s { byteIdx := utf8Len (c :: m₁) }) =
    { byteIdx := utf8Len (List.drop (n + 1) (c :: m₁)) }
have := h.prev
l m₂ r m₁✝ : List Char
s : Substring
n : Nat
c : Char
m₁ : List Char
h : ValidFor l (List.reverse m₁ ++ ([c] ++ m₂)) r s
this : Substring.prev s { byteIdx := utf8Len m₁ + csize c } = { byteIdx := utf8Len m₁ }
⊢ Substring.prevn s n (Substring.prev s { byteIdx := utf8Len (c :: m₁) }) =
    { byteIdx := utf8Len (List.drop (n + 1) (c :: m₁)) }
l m₂ r m₁✝ : List Char
s : Substring
n : Nat
c : Char
m₁ : List Char
h : ValidFor l (List.reverse m₁ ++ ([c] ++ m₂)) r s
this : Substring.prev s { byteIdx := utf8Len (List.reverse m₁) + csize c } = { byteIdx := utf8Len (List.reverse m₁) }
⊢ Substring.prevn s n (Substring.prev s { byteIdx := utf8Len (c :: m₁) }) =
    { byteIdx := utf8Len (List.drop (n + 1) (c :: m₁)) }
simp at this
no goals
l m₂ r m₁✝ : List Char
s : Substring
n : Nat
c : Char
m₁ : List Char
h : ValidFor l (List.reverse m₁ ++ ([c] ++ m₂)) r s
this : Substring.prev s { byteIdx := utf8Len m₁ + csize c } = { byteIdx := utf8Len m₁ }
⊢ Substring.prevn s n (Substring.prev s { byteIdx := utf8Len (c :: m₁) }) =
    { byteIdx := utf8Len (List.drop (n + 1) (c :: m₁)) }
simp [this, h.prevn n]