Theorem: Regex.NFA.pathIn.of_snoc_char (RegexCorrectness/NFA/Transition/Closure/Equivalence.lean)

State before:
nfa : NFA
i l : ℕ
cs : List Char
c : Char
start : ℕ
path : nfa.pathIn start i l (cs ++ [c])
⊢ ∃ j k, nfa.pathIn start i j cs ∧ k ∈ nfa.charStep j c ∧ l ∈ nfa.εClosure k
Tactic:
generalize h : cs ++ [c] = cs' at path
State after:
nfa : NFA
i l : ℕ
cs : List Char
c : Char
start : ℕ
cs' : List Char
h : cs ++ [c] = cs'
path : nfa.pathIn start i l cs'
⊢ ∃ j k, nfa.pathIn start i j cs ∧ k ∈ nfa.charStep j c ∧ l ∈ nfa.εClosure k

State before:
nfa : NFA
i l : ℕ
cs : List Char
c : Char
start : ℕ
cs' : List Char
h : cs ++ [c] = cs'
path : nfa.pathIn start i l cs'
⊢ ∃ j k, nfa.pathIn start i j cs ∧ k ∈ nfa.charStep j c ∧ l ∈ nfa.εClosure k
Tactic:
induction path generalizing cs with
| base _ => simp at h
| @step i j k cs₁ cs₂ step rest ih =>
  match snoc_eq_append h with
  | .inl ⟨h₁, h₂⟩ =>
    simp [h₁, h₂] at step rest
    have := step.nil_of_snoc
    simp [this] at *
    cases step with
    | charStep le _ step =>
      exact ⟨i, .base le, j, charStep_of_charStep step, εClosure_of_pathIn rest⟩
  | .inr ⟨cs₂', h₁, h₂⟩ =>
    have ⟨j', k', path', step', cls⟩ := ih h₂.symm
    exact ⟨j', k', h₁ ▸ .step step path', step', cls⟩
State after:
no goals

State before:
case base
nfa : NFA
i l : ℕ
c : Char
start : ℕ
cs' : List Char
i✝ : ℕ
h✝ : start ≤ i✝
cs : List Char
h : cs ++ [c] = []
⊢ ∃ j k, nfa.pathIn start i✝ j cs ∧ k ∈ nfa.charStep j c ∧ i✝ ∈ nfa.εClosure k
Tactic:
simp at h
State after:
no goals

State before:
case step
nfa : NFA
i✝ l : ℕ
c : Char
start : ℕ
cs' : List Char
i j k : ℕ
cs₁ cs₂ : List Char
step : nfa.stepIn start i j cs₁
rest : nfa.pathIn start j k cs₂
ih :
  ∀ {cs : List Char},
    cs ++ [c] = cs₂ → ∃ j_1 k_1, nfa.pathIn start j j_1 cs ∧ k_1 ∈ nfa.charStep j_1 c ∧ k ∈ nfa.εClosure k_1
cs : List Char
h : cs ++ [c] = cs₁ ++ cs₂
⊢ ∃ j k_1, nfa.pathIn start i j cs ∧ k_1 ∈ nfa.charStep j c ∧ k ∈ nfa.εClosure k_1
Tactic:
match snoc_eq_append h with
| .inl ⟨h₁, h₂⟩ =>
  simp [h₁, h₂] at step rest
  have := step.nil_of_snoc
  simp [this] at *
  cases step with
  | charStep le _ step =>
    exact ⟨i, .base le, j, charStep_of_charStep step, εClosure_of_pathIn rest⟩
| .inr ⟨cs₂', h₁, h₂⟩ =>
  have ⟨j', k', path', step', cls⟩ := ih h₂.symm
  exact ⟨j', k', h₁ ▸ .step step path', step', cls⟩
State after:
no goals

State before:
nfa : NFA
i✝ l : ℕ
c : Char
start : ℕ
cs' : List Char
i j k : ℕ
cs₁ cs₂ : List Char
step : nfa.stepIn start i j cs₁
rest : nfa.pathIn start j k cs₂
ih :
  ∀ {cs : List Char},
    cs ++ [c] = cs₂ → ∃ j_1 k_1, nfa.pathIn start j j_1 cs ∧ k_1 ∈ nfa.charStep j_1 c ∧ k ∈ nfa.εClosure k_1
cs : List Char
h : cs ++ [c] = cs₁ ++ cs₂
h₁ : cs₁ = cs ++ [c]
h₂ : cs₂ = []
⊢ ∃ j k_1, nfa.pathIn start i j cs ∧ k_1 ∈ nfa.charStep j c ∧ k ∈ nfa.εClosure k_1
Tactic:
simp [h₁, h₂] at step rest
State after:
nfa : NFA
i✝ l : ℕ
c : Char
start : ℕ
cs' : List Char
i j k : ℕ
cs₁ cs₂ : List Char
ih :
  ∀ {cs : List Char},
    cs ++ [c] = cs₂ → ∃ j_1 k_1, nfa.pathIn start j j_1 cs ∧ k_1 ∈ nfa.charStep j_1 c ∧ k ∈ nfa.εClosure k_1
cs : List Char
h : cs ++ [c] = cs₁ ++ cs₂
h₁ : cs₁ = cs ++ [c]
h₂ : cs₂ = []
step : nfa.stepIn start i j (cs ++ [c])
rest : nfa.pathIn start j k []
⊢ ∃ j k_1, nfa.pathIn start i j cs ∧ k_1 ∈ nfa.charStep j c ∧ k ∈ nfa.εClosure k_1

State before:
nfa : NFA
i✝ l : ℕ
c : Char
start : ℕ
cs' : List Char
i j k : ℕ
cs₁ cs₂ : List Char
ih :
  ∀ {cs : List Char},
    cs ++ [c] = cs₂ → ∃ j_1 k_1, nfa.pathIn start j j_1 cs ∧ k_1 ∈ nfa.charStep j_1 c ∧ k ∈ nfa.εClosure k_1
cs : List Char
h : cs ++ [c] = cs₁ ++ cs₂
h₁ : cs₁ = cs ++ [c]
h₂ : cs₂ = []
step : nfa.stepIn start i j (cs ++ [c])
rest : nfa.pathIn start j k []
⊢ ∃ j k_1, nfa.pathIn start i j cs ∧ k_1 ∈ nfa.charStep j c ∧ k ∈ nfa.εClosure k_1
Tactic:
have := step.nil_of_snoc
State after:
nfa : NFA
i✝ l : ℕ
c : Char
start : ℕ
cs' : List Char
i j k : ℕ
cs₁ cs₂ : List Char
ih :
  ∀ {cs : List Char},
    cs ++ [c] = cs₂ → ∃ j_1 k_1, nfa.pathIn start j j_1 cs ∧ k_1 ∈ nfa.charStep j_1 c ∧ k ∈ nfa.εClosure k_1
cs : List Char
h : cs ++ [c] = cs₁ ++ cs₂
h₁ : cs₁ = cs ++ [c]
h₂ : cs₂ = []
step : nfa.stepIn start i j (cs ++ [c])
rest : nfa.pathIn start j k []
this : cs = []
⊢ ∃ j k_1, nfa.pathIn start i j cs ∧ k_1 ∈ nfa.charStep j c ∧ k ∈ nfa.εClosure k_1

State before:
nfa : NFA
i✝ l : ℕ
c : Char
start : ℕ
cs' : List Char
i j k : ℕ
cs₁ cs₂ : List Char
ih :
  ∀ {cs : List Char},
    cs ++ [c] = cs₂ → ∃ j_1 k_1, nfa.pathIn start j j_1 cs ∧ k_1 ∈ nfa.charStep j_1 c ∧ k ∈ nfa.εClosure k_1
cs : List Char
h : cs ++ [c] = cs₁ ++ cs₂
h₁ : cs₁ = cs ++ [c]
h₂ : cs₂ = []
step : nfa.stepIn start i j (cs ++ [c])
rest : nfa.pathIn start j k []
this : cs = []
⊢ ∃ j k_1, nfa.pathIn start i j cs ∧ k_1 ∈ nfa.charStep j c ∧ k ∈ nfa.εClosure k_1
Tactic:
simp [this] at *
State after:
nfa : NFA
i✝ l : ℕ
c : Char
start : ℕ
cs' : List Char
i j k : ℕ
cs₁ cs₂ cs : List Char
h₂ : cs₂ = []
rest : nfa.pathIn start j k []
ih :
  ∀ {cs : List Char}, cs ++ [c] = cs₂ → ∃ j_1, nfa.pathIn start j j_1 cs ∧ ∃ x ∈ nfa.charStep j_1 c, k ∈ nfa.εClosure x
h : [c] = cs₁ ++ cs₂
h₁ : cs₁ = [c]
step : nfa.stepIn start i j [c]
this : True
⊢ ∃ j, nfa.pathIn start i j [] ∧ ∃ x ∈ nfa.charStep j c, k ∈ nfa.εClosure x

State before:
nfa : NFA
i✝ l : ℕ
c : Char
start : ℕ
cs' : List Char
i j k : ℕ
cs₁ cs₂ cs : List Char
h₂ : cs₂ = []
rest : nfa.pathIn start j k []
ih :
  ∀ {cs : List Char}, cs ++ [c] = cs₂ → ∃ j_1, nfa.pathIn start j j_1 cs ∧ ∃ x ∈ nfa.charStep j_1 c, k ∈ nfa.εClosure x
h : [c] = cs₁ ++ cs₂
h₁ : cs₁ = [c]
step : nfa.stepIn start i j [c]
this : True
⊢ ∃ j, nfa.pathIn start i j [] ∧ ∃ x ∈ nfa.charStep j c, k ∈ nfa.εClosure x
Tactic:
cases step with
| charStep le _ step =>
  exact ⟨i, .base le, j, charStep_of_charStep step, εClosure_of_pathIn rest⟩
State after:
no goals

State before:
case charStep
nfa : NFA
i✝ l : ℕ
c : Char
start : ℕ
cs' : List Char
i j k : ℕ
cs₁ cs₂ cs : List Char
h₂ : cs₂ = []
rest : nfa.pathIn start j k []
ih :
  ∀ {cs : List Char}, cs ++ [c] = cs₂ → ∃ j_1, nfa.pathIn start j j_1 cs ∧ ∃ x ∈ nfa.charStep j_1 c, k ∈ nfa.εClosure x
h : [c] = cs₁ ++ cs₂
h₁ : cs₁ = [c]
this : True
le : start ≤ i
h₂✝ : i < nfa.nodes.size
step : j ∈ nfa[i].charStep c
⊢ ∃ j, nfa.pathIn start i j [] ∧ ∃ x ∈ nfa.charStep j c, k ∈ nfa.εClosure x
Tactic:
exact ⟨i, .base le, j, charStep_of_charStep step, εClosure_of_pathIn rest⟩
State after:
no goals

State before:
nfa : NFA
i✝ l : ℕ
c : Char
start : ℕ
cs' : List Char
i j k : ℕ
cs₁ cs₂ : List Char
step : nfa.stepIn start i j cs₁
rest : nfa.pathIn start j k cs₂
ih :
  ∀ {cs : List Char},
    cs ++ [c] = cs₂ → ∃ j_1 k_1, nfa.pathIn start j j_1 cs ∧ k_1 ∈ nfa.charStep j_1 c ∧ k ∈ nfa.εClosure k_1
cs : List Char
h : cs ++ [c] = cs₁ ++ cs₂
cs₂' : List Char
h₁ : cs = cs₁ ++ cs₂'
h₂ : cs₂ = cs₂' ++ [c]
⊢ ∃ j k_1, nfa.pathIn start i j cs ∧ k_1 ∈ nfa.charStep j c ∧ k ∈ nfa.εClosure k_1
Tactic:
have ⟨j', k', path', step', cls⟩ := ih h₂.symm
State after:
nfa : NFA
i✝ l : ℕ
c : Char
start : ℕ
cs' : List Char
i j k : ℕ
cs₁ cs₂ : List Char
step : nfa.stepIn start i j cs₁
rest : nfa.pathIn start j k cs₂
ih :
  ∀ {cs : List Char},
    cs ++ [c] = cs₂ → ∃ j_1 k_1, nfa.pathIn start j j_1 cs ∧ k_1 ∈ nfa.charStep j_1 c ∧ k ∈ nfa.εClosure k_1
cs : List Char
h : cs ++ [c] = cs₁ ++ cs₂
cs₂' : List Char
h₁ : cs = cs₁ ++ cs₂'
h₂ : cs₂ = cs₂' ++ [c]
j' k' : ℕ
path' : nfa.pathIn start j j' cs₂'
step' : k' ∈ nfa.charStep j' c
cls : k ∈ nfa.εClosure k'
⊢ ∃ j k_1, nfa.pathIn start i j cs ∧ k_1 ∈ nfa.charStep j c ∧ k ∈ nfa.εClosure k_1

State before:
nfa : NFA
i✝ l : ℕ
c : Char
start : ℕ
cs' : List Char
i j k : ℕ
cs₁ cs₂ : List Char
step : nfa.stepIn start i j cs₁
rest : nfa.pathIn start j k cs₂
ih :
  ∀ {cs : List Char},
    cs ++ [c] = cs₂ → ∃ j_1 k_1, nfa.pathIn start j j_1 cs ∧ k_1 ∈ nfa.charStep j_1 c ∧ k ∈ nfa.εClosure k_1
cs : List Char
h : cs ++ [c] = cs₁ ++ cs₂
cs₂' : List Char
h₁ : cs = cs₁ ++ cs₂'
h₂ : cs₂ = cs₂' ++ [c]
j' k' : ℕ
path' : nfa.pathIn start j j' cs₂'
step' : k' ∈ nfa.charStep j' c
cls : k ∈ nfa.εClosure k'
⊢ ∃ j k_1, nfa.pathIn start i j cs ∧ k_1 ∈ nfa.charStep j c ∧ k ∈ nfa.εClosure k_1
Tactic:
exact ⟨j', k', h₁ ▸ .step step path', step', cls⟩
State after:
no goals

State before:
nfa : NFA
i l : ℕ
cs : List Char
c✝ : Char
start : ℕ
path : nfa.pathIn start i l (cs ++ [c✝])
cs₁ cs₂ cs₃ : List Char
c : Char
h : cs₁ ++ [c] = cs₂ ++ cs₃
⊢ cs₂ = cs₁ ++ [c] ∧ cs₃ = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ = cs₃' ++ [c]
Tactic:
cases cs₃ using List.list_reverse_induction with
| base =>
  simp at h
  exact .inl ⟨h.symm, rfl⟩
| ind cs₃ c' =>
  have : c = c' ∧ cs₁ = cs₂ ++ cs₃ := by
    have h₁ := congrArg List.reverse h
    simp at h₁
    have h₂ := congrArg List.reverse h₁.right
    simp at h₂
    exact ⟨h₁.left, h₂⟩
  simp [this]
State after:
no goals

State before:
case base
nfa : NFA
i l : ℕ
cs : List Char
c✝ : Char
start : ℕ
path : nfa.pathIn start i l (cs ++ [c✝])
cs₁ cs₂ : List Char
c : Char
h : cs₁ ++ [c] = cs₂ ++ []
⊢ cs₂ = cs₁ ++ [c] ∧ [] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ [] = cs₃' ++ [c]
Tactic:
simp at h
State after:
case base
nfa : NFA
i l : ℕ
cs : List Char
c✝ : Char
start : ℕ
path : nfa.pathIn start i l (cs ++ [c✝])
cs₁ cs₂ : List Char
c : Char
h : cs₁ ++ [c] = cs₂
⊢ cs₂ = cs₁ ++ [c] ∧ [] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ [] = cs₃' ++ [c]

State before:
case base
nfa : NFA
i l : ℕ
cs : List Char
c✝ : Char
start : ℕ
path : nfa.pathIn start i l (cs ++ [c✝])
cs₁ cs₂ : List Char
c : Char
h : cs₁ ++ [c] = cs₂
⊢ cs₂ = cs₁ ++ [c] ∧ [] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ [] = cs₃' ++ [c]
Tactic:
exact .inl ⟨h.symm, rfl⟩
State after:
no goals

State before:
case ind
nfa : NFA
i l : ℕ
cs : List Char
c✝ : Char
start : ℕ
path : nfa.pathIn start i l (cs ++ [c✝])
cs₁ cs₂ : List Char
c : Char
cs₃ : List Char
c' : Char
h : cs₁ ++ [c] = cs₂ ++ (cs₃ ++ [c'])
a✝ : cs₃ ++ [c'] = cs₃ → cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]
⊢ cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]
Tactic:
have : c = c' ∧ cs₁ = cs₂ ++ cs₃ := by
  have h₁ := congrArg List.reverse h
  simp at h₁
  have h₂ := congrArg List.reverse h₁.right
  simp at h₂
  exact ⟨h₁.left, h₂⟩
State after:
case ind
nfa : NFA
i l : ℕ
cs : List Char
c✝ : Char
start : ℕ
path : nfa.pathIn start i l (cs ++ [c✝])
cs₁ cs₂ : List Char
c : Char
cs₃ : List Char
c' : Char
h : cs₁ ++ [c] = cs₂ ++ (cs₃ ++ [c'])
a✝ : cs₃ ++ [c'] = cs₃ → cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]
this : c = c' ∧ cs₁ = cs₂ ++ cs₃
⊢ cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]

State before:
case ind
nfa : NFA
i l : ℕ
cs : List Char
c✝ : Char
start : ℕ
path : nfa.pathIn start i l (cs ++ [c✝])
cs₁ cs₂ : List Char
c : Char
cs₃ : List Char
c' : Char
h : cs₁ ++ [c] = cs₂ ++ (cs₃ ++ [c'])
a✝ : cs₃ ++ [c'] = cs₃ → cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]
this : c = c' ∧ cs₁ = cs₂ ++ cs₃
⊢ cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]
Tactic:
simp [this]
State after:
no goals

State before:
nfa : NFA
i l : ℕ
cs : List Char
c✝ : Char
start : ℕ
path : nfa.pathIn start i l (cs ++ [c✝])
cs₁ cs₂ : List Char
c : Char
cs₃ : List Char
c' : Char
h : cs₁ ++ [c] = cs₂ ++ (cs₃ ++ [c'])
a✝ : cs₃ ++ [c'] = cs₃ → cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]
⊢ c = c' ∧ cs₁ = cs₂ ++ cs₃
Tactic:
have h₁ := congrArg List.reverse h
State after:
nfa : NFA
i l : ℕ
cs : List Char
c✝ : Char
start : ℕ
path : nfa.pathIn start i l (cs ++ [c✝])
cs₁ cs₂ : List Char
c : Char
cs₃ : List Char
c' : Char
h : cs₁ ++ [c] = cs₂ ++ (cs₃ ++ [c'])
a✝ : cs₃ ++ [c'] = cs₃ → cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]
h₁ : (cs₁ ++ [c]).reverse = (cs₂ ++ (cs₃ ++ [c'])).reverse
⊢ c = c' ∧ cs₁ = cs₂ ++ cs₃

State before:
nfa : NFA
i l : ℕ
cs : List Char
c✝ : Char
start : ℕ
path : nfa.pathIn start i l (cs ++ [c✝])
cs₁ cs₂ : List Char
c : Char
cs₃ : List Char
c' : Char
h : cs₁ ++ [c] = cs₂ ++ (cs₃ ++ [c'])
a✝ : cs₃ ++ [c'] = cs₃ → cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]
h₁ : (cs₁ ++ [c]).reverse = (cs₂ ++ (cs₃ ++ [c'])).reverse
⊢ c = c' ∧ cs₁ = cs₂ ++ cs₃
Tactic:
simp at h₁
State after:
nfa : NFA
i l : ℕ
cs : List Char
c✝ : Char
start : ℕ
path : nfa.pathIn start i l (cs ++ [c✝])
cs₁ cs₂ : List Char
c : Char
cs₃ : List Char
c' : Char
h : cs₁ ++ [c] = cs₂ ++ (cs₃ ++ [c'])
a✝ : cs₃ ++ [c'] = cs₃ → cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]
h₁ : c = c' ∧ cs₁.reverse = cs₃.reverse ++ cs₂.reverse
⊢ c = c' ∧ cs₁ = cs₂ ++ cs₃

State before:
nfa : NFA
i l : ℕ
cs : List Char
c✝ : Char
start : ℕ
path : nfa.pathIn start i l (cs ++ [c✝])
cs₁ cs₂ : List Char
c : Char
cs₃ : List Char
c' : Char
h : cs₁ ++ [c] = cs₂ ++ (cs₃ ++ [c'])
a✝ : cs₃ ++ [c'] = cs₃ → cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]
h₁ : c = c' ∧ cs₁.reverse = cs₃.reverse ++ cs₂.reverse
⊢ c = c' ∧ cs₁ = cs₂ ++ cs₃
Tactic:
have h₂ := congrArg List.reverse h₁.right
State after:
nfa : NFA
i l : ℕ
cs : List Char
c✝ : Char
start : ℕ
path : nfa.pathIn start i l (cs ++ [c✝])
cs₁ cs₂ : List Char
c : Char
cs₃ : List Char
c' : Char
h : cs₁ ++ [c] = cs₂ ++ (cs₃ ++ [c'])
a✝ : cs₃ ++ [c'] = cs₃ → cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]
h₁ : c = c' ∧ cs₁.reverse = cs₃.reverse ++ cs₂.reverse
h₂ : cs₁.reverse.reverse = (cs₃.reverse ++ cs₂.reverse).reverse
⊢ c = c' ∧ cs₁ = cs₂ ++ cs₃

State before:
nfa : NFA
i l : ℕ
cs : List Char
c✝ : Char
start : ℕ
path : nfa.pathIn start i l (cs ++ [c✝])
cs₁ cs₂ : List Char
c : Char
cs₃ : List Char
c' : Char
h : cs₁ ++ [c] = cs₂ ++ (cs₃ ++ [c'])
a✝ : cs₃ ++ [c'] = cs₃ → cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]
h₁ : c = c' ∧ cs₁.reverse = cs₃.reverse ++ cs₂.reverse
h₂ : cs₁.reverse.reverse = (cs₃.reverse ++ cs₂.reverse).reverse
⊢ c = c' ∧ cs₁ = cs₂ ++ cs₃
Tactic:
simp at h₂
State after:
nfa : NFA
i l : ℕ
cs : List Char
c✝ : Char
start : ℕ
path : nfa.pathIn start i l (cs ++ [c✝])
cs₁ cs₂ : List Char
c : Char
cs₃ : List Char
c' : Char
h : cs₁ ++ [c] = cs₂ ++ (cs₃ ++ [c'])
a✝ : cs₃ ++ [c'] = cs₃ → cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]
h₁ : c = c' ∧ cs₁.reverse = cs₃.reverse ++ cs₂.reverse
h₂ : cs₁ = cs₂ ++ cs₃
⊢ c = c' ∧ cs₁ = cs₂ ++ cs₃

State before:
nfa : NFA
i l : ℕ
cs : List Char
c✝ : Char
start : ℕ
path : nfa.pathIn start i l (cs ++ [c✝])
cs₁ cs₂ : List Char
c : Char
cs₃ : List Char
c' : Char
h : cs₁ ++ [c] = cs₂ ++ (cs₃ ++ [c'])
a✝ : cs₃ ++ [c'] = cs₃ → cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]
h₁ : c = c' ∧ cs₁.reverse = cs₃.reverse ++ cs₂.reverse
h₂ : cs₁ = cs₂ ++ cs₃
⊢ c = c' ∧ cs₁ = cs₂ ++ cs₃
Tactic:
exact ⟨h₁.left, h₂⟩
State after:
no goals