Theorem: String.Iterator.ValidFor.exists_cons_of_not_atEnd (RegexCorrectness/Data/String.lean)

State before:
l r : List Char
it : Iterator
v : ValidFor l r it
h : ¬it.atEnd = true
⊢ ∃ r', r = it.curr :: r'
Tactic:
have := v.atEnd
State after:
l r : List Char
it : Iterator
v : ValidFor l r it
h : ¬it.atEnd = true
this : it.atEnd = true ↔ r = []
⊢ ∃ r', r = it.curr :: r'

State before:
l r : List Char
it : Iterator
v : ValidFor l r it
h : ¬it.atEnd = true
this : it.atEnd = true ↔ r = []
⊢ ∃ r', r = it.curr :: r'
Tactic:
simp [h] at this
State after:
l r : List Char
it : Iterator
v : ValidFor l r it
h : ¬it.atEnd = true
this : ¬r = []
⊢ ∃ r', r = it.curr :: r'

State before:
l r : List Char
it : Iterator
v : ValidFor l r it
h : ¬it.atEnd = true
this : ¬r = []
⊢ ∃ r', r = it.curr :: r'
Tactic:
have ⟨c, r', heq⟩ := List.exists_cons_of_ne_nil this
State after:
l r : List Char
it : Iterator
v : ValidFor l r it
h : ¬it.atEnd = true
this : ¬r = []
c : Char
r' : List Char
heq : r = c :: r'
⊢ ∃ r', r = it.curr :: r'

State before:
l r : List Char
it : Iterator
v : ValidFor l r it
h : ¬it.atEnd = true
this : ¬r = []
c : Char
r' : List Char
heq : r = c :: r'
⊢ ∃ r', r = it.curr :: r'
Tactic:
subst heq
State after:
l : List Char
it : Iterator
h : ¬it.atEnd = true
c : Char
r' : List Char
v : ValidFor l (c :: r') it
this : ¬c :: r' = []
⊢ ∃ r'_1, c :: r' = it.curr :: r'_1

State before:
l : List Char
it : Iterator
h : ¬it.atEnd = true
c : Char
r' : List Char
v : ValidFor l (c :: r') it
this : ¬c :: r' = []
⊢ ∃ r'_1, c :: r' = it.curr :: r'_1
Tactic:
have := v.curr
State after:
l : List Char
it : Iterator
h : ¬it.atEnd = true
c : Char
r' : List Char
v : ValidFor l (c :: r') it
this✝ : ¬c :: r' = []
this : it.curr = (c :: r').headD default
⊢ ∃ r'_1, c :: r' = it.curr :: r'_1

State before:
l : List Char
it : Iterator
h : ¬it.atEnd = true
c : Char
r' : List Char
v : ValidFor l (c :: r') it
this✝ : ¬c :: r' = []
this : it.curr = (c :: r').headD default
⊢ ∃ r'_1, c :: r' = it.curr :: r'_1
Tactic:
simp at this
State after:
l : List Char
it : Iterator
h : ¬it.atEnd = true
c : Char
r' : List Char
v : ValidFor l (c :: r') it
this✝ : ¬c :: r' = []
this : it.curr = c
⊢ ∃ r'_1, c :: r' = it.curr :: r'_1

State before:
l : List Char
it : Iterator
h : ¬it.atEnd = true
c : Char
r' : List Char
v : ValidFor l (c :: r') it
this✝ : ¬c :: r' = []
this : it.curr = c
⊢ ∃ r'_1, c :: r' = it.curr :: r'_1
Tactic:
subst this
State after:
l : List Char
it : Iterator
h : ¬it.atEnd = true
r' : List Char
v : ValidFor l (it.curr :: r') it
this : ¬it.curr :: r' = []
⊢ ∃ r'_1, it.curr :: r' = it.curr :: r'_1

State before:
l : List Char
it : Iterator
h : ¬it.atEnd = true
r' : List Char
v : ValidFor l (it.curr :: r') it
this : ¬it.curr :: r' = []
⊢ ∃ r'_1, it.curr :: r' = it.curr :: r'_1
Tactic:
exact ⟨r', rfl⟩
State after:
no goals