b e : Pos
x✝ : Substring
h₁✝ : Valid x✝
h₂ : Valid { str := toString x✝, startPos := b, stopPos := e }
l m r : List Char
h₁ : ValidFor l m r x✝
⊢ toString (Substring.extract x✝ b e) = String.extract (toString x✝) b e
b e : Pos
x✝ : Substring
h₁ : Valid x✝
h₂ : Valid { str := toString x✝, startPos := b, stopPos := e }
⊢ toString (Substring.extract x✝ b e) = String.extract (toString x✝) b e
let ⟨l, m, r, h₁⟩ := h₁.validFor
b e : Pos
x✝ : Substring
h₁✝ : Valid x✝
l m : List Char
h₂ : Valid { str := { data := m }, startPos := b, stopPos := e }
r : List Char
h₁ : ValidFor l m r x✝
⊢ toString (Substring.extract x✝ b e) = String.extract (toString x✝) b e
b e : Pos
x✝ : Substring
h₁✝ : Valid x✝
h₂ : Valid { str := toString x✝, startPos := b, stopPos := e }
l m r : List Char
h₁ : ValidFor l m r x✝
⊢ toString (Substring.extract x✝ b e) = String.extract (toString x✝) b e
rw [h₁.toString] at h₂
b e : Pos
x✝ : Substring
h₁✝ : Valid x✝
l m : List Char
h₂✝ : Valid { str := { data := m }, startPos := b, stopPos := e }
r : List Char
h₁ : ValidFor l m r x✝
ml mm mr : List Char
h₂ : ValidFor ml mm mr { str := { data := m }, startPos := b, stopPos := e }
⊢ toString (Substring.extract x✝ b e) = String.extract (toString x✝) b e
b e : Pos
x✝ : Substring
h₁✝ : Valid x✝
l m : List Char
h₂ : Valid { str := { data := m }, startPos := b, stopPos := e }
r : List Char
h₁ : ValidFor l m r x✝
⊢ toString (Substring.extract x✝ b e) = String.extract (toString x✝) b e
let ⟨ml, mm, mr, h₂⟩ := h₂.validFor
b e : Pos
x✝ : Substring
h₁✝ : Valid x✝
l m : List Char
h₂✝ : Valid { str := { data := m }, startPos := b, stopPos := e }
r : List Char
h₁ : ValidFor l m r x✝
ml mm mr : List Char
h₂ : ValidFor ml mm mr { str := { data := m }, startPos := b, stopPos := e }
l' r' : List Char
h₃ : ValidFor l' mm r' (Substring.extract x✝ b e)
⊢ toString (Substring.extract x✝ b e) = String.extract (toString x✝) b e
b e : Pos
x✝ : Substring
h₁✝ : Valid x✝
l m : List Char
h₂✝ : Valid { str := { data := m }, startPos := b, stopPos := e }
r : List Char
h₁ : ValidFor l m r x✝
ml mm mr : List Char
h₂ : ValidFor ml mm mr { str := { data := m }, startPos := b, stopPos := e }
⊢ toString (Substring.extract x✝ b e) = String.extract (toString x✝) b e
have ⟨l', r', h₃⟩ := h₁.extract h₂
no goals
b e : Pos
x✝ : Substring
h₁✝ : Valid x✝
l m : List Char
h₂✝ : Valid { str := { data := m }, startPos := b, stopPos := e }
r : List Char
h₁ : ValidFor l m r x✝
ml mm mr : List Char
h₂ : ValidFor ml mm mr { str := { data := m }, startPos := b, stopPos := e }
l' r' : List Char
h₃ : ValidFor l' mm r' (Substring.extract x✝ b e)
⊢ toString (Substring.extract x✝ b e) = String.extract (toString x✝) b e
rw [h₃.toString, h₁.toString, ← h₂.toString, toString]