-- Mathlib/Computability/EpsilonNFA.lean
theorem toεNFA_evalFrom_match (M : NFA α σ) (start : Set σ) :
    M.toεNFA.evalFrom start = M.evalFrom start

Proof state:
α : Type u
σ : Type v
M : NFA α σ
start : Set σ
⊢ M.toεNFA.stepSet = M.stepSet

Tactic:
ext S s

Result:
case h.h.h
α : Type u
σ : Type v
M : NFA α σ
start S : Set σ
s : α
x✝ : σ
⊢ x✝ ∈ M.toεNFA.stepSet S s ↔ x✝ ∈ M.stepSet S s

Proof state:
α : Type u
σ : Type v
M : NFA α σ
start : Set σ
this : M.toεNFA.stepSet = M.stepSet
⊢ List.foldl M.toεNFA.stepSet start = List.foldl M.stepSet start

Tactic:
rw [this]

Result:
no goals

Proof state:
case h.h.h
α : Type u
σ : Type v
M : NFA α σ
start S : Set σ
s : α
x✝ : σ
⊢ x✝ ∈ M.toεNFA.stepSet S s ↔ x✝ ∈ M.stepSet S s

Tactic:
simp only [stepSet, εNFA.stepSet, exists_prop, Set.mem_iUnion]

Result:
case h.h.h
α : Type u
σ : Type v
M : NFA α σ
start S : Set σ
s : α
x✝ : σ
⊢ (∃ i ∈ S, x✝ ∈ M.toεNFA.εClosure (M.toεNFA.step i (some s))) ↔ ∃ i ∈ S, x✝ ∈ M.step i s

Proof state:
case h.h.h.h
α : Type u
σ : Type v
M : NFA α σ
start S : Set σ
s : α
x✝ : σ
⊢ ∀ (a : σ), a ∈ S ∧ x✝ ∈ M.toεNFA.εClosure (M.toεNFA.step a (some s)) ↔ a ∈ S ∧ x✝ ∈ M.step a s

Tactic:
simp only [and_congr_right_iff]

Result:
case h.h.h.h
α : Type u
σ : Type v
M : NFA α σ
start S : Set σ
s : α
x✝ : σ
⊢ ∀ a ∈ S, x✝ ∈ M.toεNFA.εClosure (M.toεNFA.step a (some s)) ↔ x✝ ∈ M.step a s

Proof state:
α : Type u
σ : Type v
M : NFA α σ
start : Set σ
⊢ M.toεNFA.evalFrom start = M.evalFrom start

Tactic:
rw [evalFrom, εNFA.evalFrom, toεNFA_εClosure]

Result:
α : Type u
σ : Type v
M : NFA α σ
start : Set σ
⊢ List.foldl M.toεNFA.stepSet start = List.foldl M.stepSet start

Proof state:
α : Type u
σ : Type v
M : NFA α σ
start : Set σ
⊢ List.foldl M.toεNFA.stepSet start = List.foldl M.stepSet start

Tactic:
suffices εNFA.stepSet (toεNFA M) = stepSet M by rw [this]

Result:
α : Type u
σ : Type v
M : NFA α σ
start : Set σ
⊢ M.toεNFA.stepSet = M.stepSet

Proof state:
case h.h.h.h
α : Type u
σ : Type v
M : NFA α σ
start S : Set σ
s : α
x✝ a✝¹ : σ
a✝ : a✝¹ ∈ S
⊢ x✝ ∈ M.toεNFA.εClosure (M.toεNFA.step a✝¹ (some s)) ↔ x✝ ∈ M.step a✝¹ s

Tactic:
rw [M.toεNFA_εClosure]

Result:
case h.h.h.h
α : Type u
σ : Type v
M : NFA α σ
start S : Set σ
s : α
x✝ a✝¹ : σ
a✝ : a✝¹ ∈ S
⊢ x✝ ∈ M.toεNFA.step a✝¹ (some s) ↔ x✝ ∈ M.step a✝¹ s

Proof state:
case h.h.h.h
α : Type u
σ : Type v
M : NFA α σ
start S : Set σ
s : α
x✝ a✝¹ : σ
a✝ : a✝¹ ∈ S
⊢ x✝ ∈ M.toεNFA.step a✝¹ (some s) ↔ x✝ ∈ M.step a✝¹ s

Tactic:
rfl

Result:
no goals

Proof state:
case h.h.h
α : Type u
σ : Type v
M : NFA α σ
start S : Set σ
s : α
x✝ : σ
⊢ (∃ i ∈ S, x✝ ∈ M.toεNFA.εClosure (M.toεNFA.step i (some s))) ↔ ∃ i ∈ S, x✝ ∈ M.step i s

Tactic:
apply exists_congr

Result:
case h.h.h.h
α : Type u
σ : Type v
M : NFA α σ
start S : Set σ
s : α
x✝ : σ
⊢ ∀ (a : σ), a ∈ S ∧ x✝ ∈ M.toεNFA.εClosure (M.toεNFA.step a (some s)) ↔ a ∈ S ∧ x✝ ∈ M.step a s

Proof state:
case h.h.h.h
α : Type u
σ : Type v
M : NFA α σ
start S : Set σ
s : α
x✝ : σ
⊢ ∀ a ∈ S, x✝ ∈ M.toεNFA.εClosure (M.toεNFA.step a (some s)) ↔ x✝ ∈ M.step a s

Tactic:
intro _ _

Result:
case h.h.h.h
α : Type u
σ : Type v
M : NFA α σ
start S : Set σ
s : α
x✝ a✝¹ : σ
a✝ : a✝¹ ∈ S
⊢ x✝ ∈ M.toεNFA.εClosure (M.toεNFA.step a✝¹ (some s)) ↔ x✝ ∈ M.step a✝¹ s