m₂ m₁ : List Char
x✝ : Substring
h✝ : Valid x✝
e : (toString x✝).data = List.reverse m₁ ++ m₂
l m r : List Char
h : ValidFor l m r x✝
⊢ ∀ (n : Nat), Substring.prevn x✝ n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len (List.drop n m₁) }
m₂ m₁ : List Char
x✝ : Substring
h : Valid x✝
e : (toString x✝).data = List.reverse m₁ ++ m₂
⊢ ∀ (n : Nat), Substring.prevn x✝ n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len (List.drop n m₁) }
let ⟨l, m, r, h⟩ := h.validFor
m₂ m₁ : List Char
x✝ : Substring
h✝ : Valid x✝
l m r : List Char
h : ValidFor l m r x✝
e : m = List.reverse m₁ ++ m₂
⊢ ∀ (n : Nat), Substring.prevn x✝ n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len (List.drop n m₁) }
m₂ m₁ : List Char
x✝ : Substring
h✝ : Valid x✝
e : (toString x✝).data = List.reverse m₁ ++ m₂
l m r : List Char
h : ValidFor l m r x✝
⊢ ∀ (n : Nat), Substring.prevn x✝ n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len (List.drop n m₁) }
simp [h.toString] at e
m₂ m₁ : List Char
x✝ : Substring
h✝ : Valid x✝
l r : List Char
h : ValidFor l (List.reverse m₁ ++ m₂) r x✝
⊢ ∀ (n : Nat), Substring.prevn x✝ n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len (List.drop n m₁) }
m₂ m₁ : List Char
x✝ : Substring
h✝ : Valid x✝
l m r : List Char
h : ValidFor l m r x✝
e : m = List.reverse m₁ ++ m₂
⊢ ∀ (n : Nat), Substring.prevn x✝ n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len (List.drop n m₁) }
subst e
no goals
m₂ m₁ : List Char
x✝ : Substring
h✝ : Valid x✝
l r : List Char
h : ValidFor l (List.reverse m₁ ++ m₂) r x✝
⊢ ∀ (n : Nat), Substring.prevn x✝ n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len (List.drop n m₁) }
simp [h.prevn]