m₁ m₂ : List Char
x✝ : Substring
h✝ : Valid x✝
e : (toString x✝).data = m₁ ++ m₂
l m r : List Char
h : ValidFor l m r x✝
⊢ ∀ (n : Nat), Substring.nextn x✝ n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len m₁ + utf8Len (List.take n m₂) }
m₁ m₂ : List Char
x✝ : Substring
h : Valid x✝
e : (toString x✝).data = m₁ ++ m₂
⊢ ∀ (n : Nat), Substring.nextn x✝ n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len m₁ + utf8Len (List.take 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 = m₁ ++ m₂
⊢ ∀ (n : Nat), Substring.nextn x✝ n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len m₁ + utf8Len (List.take n m₂) }
m₁ m₂ : List Char
x✝ : Substring
h✝ : Valid x✝
e : (toString x✝).data = m₁ ++ m₂
l m r : List Char
h : ValidFor l m r x✝
⊢ ∀ (n : Nat), Substring.nextn x✝ n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len m₁ + utf8Len (List.take n m₂) }
simp [h.toString] at e
m₁ m₂ : List Char
x✝ : Substring
h✝ : Valid x✝
l r : List Char
h : ValidFor l (m₁ ++ m₂) r x✝
⊢ ∀ (n : Nat), Substring.nextn x✝ n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len m₁ + utf8Len (List.take n m₂) }
m₁ m₂ : List Char
x✝ : Substring
h✝ : Valid x✝
l m r : List Char
h : ValidFor l m r x✝
e : m = m₁ ++ m₂
⊢ ∀ (n : Nat), Substring.nextn x✝ n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len m₁ + utf8Len (List.take n m₂) }
subst e
no goals
m₁ m₂ : List Char
x✝ : Substring
h✝ : Valid x✝
l r : List Char
h : ValidFor l (m₁ ++ m₂) r x✝
⊢ ∀ (n : Nat), Substring.nextn x✝ n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len m₁ + utf8Len (List.take n m₂) }
simp [h.nextn]