From 74eae578e32b13c63d4edffff8530bc26211fb97 Mon Sep 17 00:00:00 2001
From: Anthony DeRossi <aderossi@bu.edu>
Date: Sat, 28 Dec 2024 21:58:54 -0500
Subject: [PATCH 01/18] feat(Computability/EpsilonNFA): define path relation
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

`Path` enables path-based reasoning in proofs involving `εNFA`.
---
 Mathlib/Computability/EpsilonNFA.lean | 134 +++++++++++++++++++++++++-
 1 file changed, 133 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Computability/EpsilonNFA.lean b/Mathlib/Computability/EpsilonNFA.lean
index 63bf7127e644f..67e66f9097873 100644
--- a/Mathlib/Computability/EpsilonNFA.lean
+++ b/Mathlib/Computability/EpsilonNFA.lean
@@ -1,9 +1,10 @@
 /-
 Copyright (c) 2021 Fox Thomson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Fox Thomson, Yaël Dillies
+Authors: Fox Thomson, Yaël Dillies, Anthony DeRossi
 -/
 import Mathlib.Computability.NFA
+import Mathlib.Data.List.ReduceOption
 
 /-!
 # Epsilon Nondeterministic Finite Automata
@@ -63,6 +64,18 @@ theorem εClosure_empty : M.εClosure ∅ = ∅ :=
 theorem εClosure_univ : M.εClosure univ = univ :=
   eq_univ_of_univ_subset <| subset_εClosure _ _
 
+theorem mem_εClosure_choice_iff (s : σ) (S : Set σ) :
+    s ∈ M.εClosure S ↔ ∃ t ∈ S, s ∈ M.εClosure {t} := by
+  constructor
+  · intro h
+    induction' h with s _ _ _ _ _ ih
+    · tauto
+    · obtain ⟨s, _, _⟩ := ih
+      use s
+      solve_by_elim [εClosure.step]
+  · intro ⟨_, _, h⟩
+    induction' h <;> subst_vars <;> solve_by_elim [εClosure.step]
+
 /-- `M.stepSet S a` is the union of the ε-closure of `M.step s a` for all `s ∈ S`. -/
 def stepSet (S : Set σ) (a : α) : Set σ :=
   ⋃ s ∈ S, M.εClosure (M.step s a)
@@ -103,6 +116,19 @@ theorem evalFrom_empty (x : List α) : M.evalFrom ∅ x = ∅ := by
   · rw [evalFrom_nil, εClosure_empty]
   · rw [evalFrom_append_singleton, ih, stepSet_empty]
 
+theorem mem_evalFrom_choice_iff (s : σ) (S : Set σ) (x : List α) :
+    s ∈ M.evalFrom S x ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} x := by
+  induction' x using List.reverseRecOn with _ _ ih generalizing s
+  · exact mem_εClosure_choice_iff _ _ _
+  · simp only [evalFrom_append_singleton, mem_stepSet_iff]
+    constructor <;> intro h
+    · obtain ⟨_, h, _⟩ := h
+      rw [ih] at h
+      tauto
+    · obtain ⟨_, ht, _, h, _⟩ := h
+      have := (ih _).mpr ⟨_, ht, h⟩
+      tauto
+
 /-- `M.eval x` computes all possible paths through `M` with input `x` starting at an element of
 `M.start`. -/
 def eval :=
@@ -124,6 +150,112 @@ theorem eval_append_singleton (x : List α) (a : α) : M.eval (x ++ [a]) = M.ste
 def accepts : Language α :=
   { x | ∃ S ∈ M.accept, S ∈ M.eval x }
 
+/-- An `M.Path` represents a traversal in `M` from a start state to an end state by following a list
+  of transitions in order. -/
+inductive Path : σ → σ → List (Option α) → Prop
+  | nil : ∀ s, Path s s []
+  | cons (t s u : σ) (a : Option α) (x : List (Option α)) :
+      t ∈ M.step s a → Path t u x → Path s u (a :: x)
+
+theorem Path_nil_eq (s t : σ) : M.Path s t [] → s = t := by
+  intro h
+  cases h
+  rfl
+
+theorem Path_singleton_iff (s t : σ) (a : Option α) : M.Path s t [a] ↔ t ∈ M.step s a:= by
+  constructor
+  · intro h
+    cases' h with _ _ _ _ _ _ _ h
+    apply Path_nil_eq at h
+    subst t
+    assumption
+  · tauto
+
+theorem Path_append_iff (s u : σ) (x y : List (Option α)) :
+    M.Path s u (x ++ y) ↔ ∃ t, M.Path s t x ∧ M.Path t u y := by
+  constructor
+  · induction' x with _ _ ih generalizing s
+    · rw [List.nil_append]
+      tauto
+    · intro h
+      cases' h with _ _ _ _ _ _ _ h
+      obtain ⟨_, _, _⟩ := ih _ h
+      tauto
+  · intro ⟨_, hx, _⟩
+    induction' x generalizing s <;> cases hx <;> tauto
+
+theorem εClosure_Path_iff (s₁ s₂ : σ) :
+    s₂ ∈ M.εClosure {s₁} ↔ ∃ n, M.Path s₁ s₂ (List.replicate n none) := by
+  constructor
+  · intro h
+    induction' h with t _ _ _ _ _ ih
+    · use 0
+      subst t
+      apply Path.nil
+    · obtain ⟨n, _⟩ := ih
+      use n + 1
+      rw [List.replicate_add, Path_append_iff]
+      tauto
+  · intro ⟨n, h⟩
+    induction' n generalizing s₂
+    · rw [List.replicate_zero] at h
+      apply Path_nil_eq at h
+      solve_by_elim
+    · simp_rw [List.replicate_add, Path_append_iff, List.replicate_one, Path_singleton_iff] at h
+      obtain ⟨_, _, h⟩ := h
+      solve_by_elim [εClosure.step]
+
+theorem evalFrom_Path_iff (s₁ s₂ : σ) (x : List α) :
+    s₂ ∈ M.evalFrom {s₁} x ↔ ∃ x', x'.reduceOption = x ∧ M.Path s₁ s₂ x' := by
+  induction' x using List.reverseRecOn with _ a ih generalizing s₂
+  · rw [evalFrom_nil, εClosure_Path_iff]
+    constructor
+    · intro ⟨n, _⟩
+      use List.replicate n none
+      rw [List.reduceOption_replicate_of_none]
+      trivial
+    · intro ⟨_, hx⟩
+      rw [List.reduceOption_eq_nil_replicate_iff] at hx
+      obtain ⟨⟨_, ⟨⟩⟩, _⟩ := hx
+      tauto
+  · rw [evalFrom_append_singleton, mem_stepSet_iff]
+    constructor
+    · intro ⟨_, ht, h⟩
+      obtain ⟨x', _, _⟩ := (ih _).mp ht
+      rw [mem_εClosure_choice_iff] at h
+      obtain ⟨_, _, h⟩ := h
+      rw [εClosure_Path_iff] at h
+      obtain ⟨n, _⟩ := h
+      use x' ++ some a :: List.replicate n none
+      rw [List.reduceOption_append, List.reduceOption_cons_of_some,
+        List.reduceOption_replicate_of_none, Path_append_iff]
+      tauto
+    · intro ⟨_, hx, h⟩
+      rw [← List.concat_eq_append, List.reduceOption_eq_concat_iff] at hx
+      obtain ⟨_, _, ⟨⟩, _, hx₂⟩ := hx
+      rw [List.reduceOption_eq_nil_replicate_iff] at hx₂
+      obtain ⟨_, ⟨⟩⟩ := hx₂
+      rw [Path_append_iff] at h
+      obtain ⟨t, _, _ | _⟩ := h
+      use t
+      rw [mem_εClosure_choice_iff, ih]
+      simp_rw [εClosure_Path_iff]
+      tauto
+
+theorem accepts_Path_iff (x : List α) :
+    x ∈ M.accepts ↔
+      ∃ s₁ s₂ x', s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.Path s₁ s₂ x' := by
+  constructor
+  · intro ⟨_, _, h⟩
+    rw [eval, mem_evalFrom_choice_iff] at h
+    obtain ⟨_, _, h⟩ := h
+    rw [evalFrom_Path_iff] at h
+    tauto
+  · intro ⟨_, _, _, hs₁, _, h⟩
+    have := (M.evalFrom_Path_iff _ _ _).mpr ⟨_, h⟩
+    have := (M.mem_evalFrom_choice_iff _ _ _).mpr ⟨_, hs₁, this⟩
+    tauto
+
 /-! ### Conversions between `εNFA` and `NFA` -/
 
 

From 4aade4c45026ecb15287cdaa7cde465ed09f0c7f Mon Sep 17 00:00:00 2001
From: Anthony DeRossi <aderossi@bu.edu>
Date: Sat, 11 Jan 2025 07:16:29 -0500
Subject: [PATCH 02/18] Fix for changes in #20644

Theorems were renamed.
---
 Mathlib/Computability/EpsilonNFA.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Computability/EpsilonNFA.lean b/Mathlib/Computability/EpsilonNFA.lean
index 67e66f9097873..4cf85337f9cc2 100644
--- a/Mathlib/Computability/EpsilonNFA.lean
+++ b/Mathlib/Computability/EpsilonNFA.lean
@@ -212,10 +212,10 @@ theorem evalFrom_Path_iff (s₁ s₂ : σ) (x : List α) :
     constructor
     · intro ⟨n, _⟩
       use List.replicate n none
-      rw [List.reduceOption_replicate_of_none]
+      rw [List.reduceOption_replicate_none]
       trivial
     · intro ⟨_, hx⟩
-      rw [List.reduceOption_eq_nil_replicate_iff] at hx
+      rw [List.reduceOption_eq_nil_iff] at hx
       obtain ⟨⟨_, ⟨⟩⟩, _⟩ := hx
       tauto
   · rw [evalFrom_append_singleton, mem_stepSet_iff]
@@ -228,12 +228,12 @@ theorem evalFrom_Path_iff (s₁ s₂ : σ) (x : List α) :
       obtain ⟨n, _⟩ := h
       use x' ++ some a :: List.replicate n none
       rw [List.reduceOption_append, List.reduceOption_cons_of_some,
-        List.reduceOption_replicate_of_none, Path_append_iff]
+        List.reduceOption_replicate_none, Path_append_iff]
       tauto
     · intro ⟨_, hx, h⟩
       rw [← List.concat_eq_append, List.reduceOption_eq_concat_iff] at hx
       obtain ⟨_, _, ⟨⟩, _, hx₂⟩ := hx
-      rw [List.reduceOption_eq_nil_replicate_iff] at hx₂
+      rw [List.reduceOption_eq_nil_iff] at hx₂
       obtain ⟨_, ⟨⟩⟩ := hx₂
       rw [Path_append_iff] at h
       obtain ⟨t, _, _ | _⟩ := h

From ec24b4cb36ff297db75fb907c878cd1f2b78b971 Mon Sep 17 00:00:00 2001
From: Anthony DeRossi <aderossi@bu.edu>
Date: Sat, 18 Jan 2025 17:32:52 -0500
Subject: [PATCH 03/18] Clean up theorem statements

Theorems are renamed to use `snake_case` and remove `_iff` suffixes, and
arguments are made implicit. `@[simp]` is also added where applicable.
---
 Mathlib/Computability/EpsilonNFA.lean | 58 ++++++++++++++-------------
 1 file changed, 30 insertions(+), 28 deletions(-)

diff --git a/Mathlib/Computability/EpsilonNFA.lean b/Mathlib/Computability/EpsilonNFA.lean
index 4cf85337f9cc2..8953ae1e7140c 100644
--- a/Mathlib/Computability/EpsilonNFA.lean
+++ b/Mathlib/Computability/EpsilonNFA.lean
@@ -64,7 +64,7 @@ theorem εClosure_empty : M.εClosure ∅ = ∅ :=
 theorem εClosure_univ : M.εClosure univ = univ :=
   eq_univ_of_univ_subset <| subset_εClosure _ _
 
-theorem mem_εClosure_choice_iff (s : σ) (S : Set σ) :
+theorem mem_εClosure_choice {s : σ} {S : Set σ} :
     s ∈ M.εClosure S ↔ ∃ t ∈ S, s ∈ M.εClosure {t} := by
   constructor
   · intro h
@@ -116,17 +116,17 @@ theorem evalFrom_empty (x : List α) : M.evalFrom ∅ x = ∅ := by
   · rw [evalFrom_nil, εClosure_empty]
   · rw [evalFrom_append_singleton, ih, stepSet_empty]
 
-theorem mem_evalFrom_choice_iff (s : σ) (S : Set σ) (x : List α) :
+theorem mem_evalFrom_choice {s : σ} {S : Set σ} {x : List α} :
     s ∈ M.evalFrom S x ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} x := by
   induction' x using List.reverseRecOn with _ _ ih generalizing s
-  · exact mem_εClosure_choice_iff _ _ _
+  · apply mem_εClosure_choice
   · simp only [evalFrom_append_singleton, mem_stepSet_iff]
     constructor <;> intro h
     · obtain ⟨_, h, _⟩ := h
       rw [ih] at h
       tauto
     · obtain ⟨_, ht, _, h, _⟩ := h
-      have := (ih _).mpr ⟨_, ht, h⟩
+      have := ih.mpr ⟨_, ht, h⟩
       tauto
 
 /-- `M.eval x` computes all possible paths through `M` with input `x` starting at an element of
@@ -157,21 +157,23 @@ inductive Path : σ → σ → List (Option α) → Prop
   | cons (t s u : σ) (a : Option α) (x : List (Option α)) :
       t ∈ M.step s a → Path t u x → Path s u (a :: x)
 
-theorem Path_nil_eq (s t : σ) : M.Path s t [] → s = t := by
+theorem Path.eq_of_nil (s t : σ) : M.Path s t [] → s = t := by
   intro h
   cases h
   rfl
 
-theorem Path_singleton_iff (s t : σ) (a : Option α) : M.Path s t [a] ↔ t ∈ M.step s a:= by
+@[simp]
+theorem path_singleton {s t : σ} {a : Option α} : M.Path s t [a] ↔ t ∈ M.step s a := by
   constructor
   · intro h
     cases' h with _ _ _ _ _ _ _ h
-    apply Path_nil_eq at h
+    apply Path.eq_of_nil at h
     subst t
     assumption
   · tauto
 
-theorem Path_append_iff (s u : σ) (x y : List (Option α)) :
+@[simp]
+theorem path_append {s u : σ} {x y : List (Option α)} :
     M.Path s u (x ++ y) ↔ ∃ t, M.Path s t x ∧ M.Path t u y := by
   constructor
   · induction' x with _ _ ih generalizing s
@@ -179,12 +181,12 @@ theorem Path_append_iff (s u : σ) (x y : List (Option α)) :
       tauto
     · intro h
       cases' h with _ _ _ _ _ _ _ h
-      obtain ⟨_, _, _⟩ := ih _ h
+      obtain ⟨_, _, _⟩ := ih h
       tauto
   · intro ⟨_, hx, _⟩
     induction' x generalizing s <;> cases hx <;> tauto
 
-theorem εClosure_Path_iff (s₁ s₂ : σ) :
+theorem εClosure_path {s₁ s₂ : σ} :
     s₂ ∈ M.εClosure {s₁} ↔ ∃ n, M.Path s₁ s₂ (List.replicate n none) := by
   constructor
   · intro h
@@ -194,21 +196,21 @@ theorem εClosure_Path_iff (s₁ s₂ : σ) :
       apply Path.nil
     · obtain ⟨n, _⟩ := ih
       use n + 1
-      rw [List.replicate_add, Path_append_iff]
+      rw [List.replicate_add, path_append]
       tauto
   · intro ⟨n, h⟩
     induction' n generalizing s₂
     · rw [List.replicate_zero] at h
-      apply Path_nil_eq at h
+      apply Path.eq_of_nil at h
       solve_by_elim
-    · simp_rw [List.replicate_add, Path_append_iff, List.replicate_one, Path_singleton_iff] at h
-      obtain ⟨_, _, h⟩ := h
+    · simp_rw [List.replicate_add, path_append, List.replicate_one, path_singleton] at h
+      obtain ⟨_, _, _⟩ := h
       solve_by_elim [εClosure.step]
 
-theorem evalFrom_Path_iff (s₁ s₂ : σ) (x : List α) :
+theorem evalFrom_path {s₁ s₂ : σ} {x : List α} :
     s₂ ∈ M.evalFrom {s₁} x ↔ ∃ x', x'.reduceOption = x ∧ M.Path s₁ s₂ x' := by
   induction' x using List.reverseRecOn with _ a ih generalizing s₂
-  · rw [evalFrom_nil, εClosure_Path_iff]
+  · rw [evalFrom_nil, εClosure_path]
     constructor
     · intro ⟨n, _⟩
       use List.replicate n none
@@ -221,39 +223,39 @@ theorem evalFrom_Path_iff (s₁ s₂ : σ) (x : List α) :
   · rw [evalFrom_append_singleton, mem_stepSet_iff]
     constructor
     · intro ⟨_, ht, h⟩
-      obtain ⟨x', _, _⟩ := (ih _).mp ht
-      rw [mem_εClosure_choice_iff] at h
+      obtain ⟨x', _, _⟩ := ih.mp ht
+      rw [mem_εClosure_choice] at h
       obtain ⟨_, _, h⟩ := h
-      rw [εClosure_Path_iff] at h
+      rw [εClosure_path] at h
       obtain ⟨n, _⟩ := h
       use x' ++ some a :: List.replicate n none
       rw [List.reduceOption_append, List.reduceOption_cons_of_some,
-        List.reduceOption_replicate_none, Path_append_iff]
+        List.reduceOption_replicate_none, path_append]
       tauto
     · intro ⟨_, hx, h⟩
       rw [← List.concat_eq_append, List.reduceOption_eq_concat_iff] at hx
       obtain ⟨_, _, ⟨⟩, _, hx₂⟩ := hx
       rw [List.reduceOption_eq_nil_iff] at hx₂
       obtain ⟨_, ⟨⟩⟩ := hx₂
-      rw [Path_append_iff] at h
+      rw [path_append] at h
       obtain ⟨t, _, _ | _⟩ := h
       use t
-      rw [mem_εClosure_choice_iff, ih]
-      simp_rw [εClosure_Path_iff]
+      rw [mem_εClosure_choice, ih]
+      simp_rw [εClosure_path]
       tauto
 
-theorem accepts_Path_iff (x : List α) :
+theorem accepts_path {x : List α} :
     x ∈ M.accepts ↔
       ∃ s₁ s₂ x', s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.Path s₁ s₂ x' := by
   constructor
   · intro ⟨_, _, h⟩
-    rw [eval, mem_evalFrom_choice_iff] at h
+    rw [eval, mem_evalFrom_choice] at h
     obtain ⟨_, _, h⟩ := h
-    rw [evalFrom_Path_iff] at h
+    rw [evalFrom_path] at h
     tauto
   · intro ⟨_, _, _, hs₁, _, h⟩
-    have := (M.evalFrom_Path_iff _ _ _).mpr ⟨_, h⟩
-    have := (M.mem_evalFrom_choice_iff _ _ _).mpr ⟨_, hs₁, this⟩
+    have := M.evalFrom_path.mpr ⟨_, h⟩
+    have := M.mem_evalFrom_choice.mpr ⟨_, hs₁, this⟩
     tauto
 
 /-! ### Conversions between `εNFA` and `NFA` -/

From b1557a6234bc712c26c568d5bdc6aad1e96778ab Mon Sep 17 00:00:00 2001
From: Anthony DeRossi <aderossi@bu.edu>
Date: Sat, 18 Jan 2025 18:13:42 -0500
Subject: [PATCH 04/18] Use where syntax for iff proofs

---
 Mathlib/Computability/EpsilonNFA.lean | 42 ++++++++++++++-------------
 1 file changed, 22 insertions(+), 20 deletions(-)

diff --git a/Mathlib/Computability/EpsilonNFA.lean b/Mathlib/Computability/EpsilonNFA.lean
index 8953ae1e7140c..672be49313e71 100644
--- a/Mathlib/Computability/EpsilonNFA.lean
+++ b/Mathlib/Computability/EpsilonNFA.lean
@@ -65,15 +65,15 @@ theorem εClosure_univ : M.εClosure univ = univ :=
   eq_univ_of_univ_subset <| subset_εClosure _ _
 
 theorem mem_εClosure_choice {s : σ} {S : Set σ} :
-    s ∈ M.εClosure S ↔ ∃ t ∈ S, s ∈ M.εClosure {t} := by
-  constructor
-  · intro h
+    s ∈ M.εClosure S ↔ ∃ t ∈ S, s ∈ M.εClosure {t} where
+  mp h := by
     induction' h with s _ _ _ _ _ ih
     · tauto
     · obtain ⟨s, _, _⟩ := ih
       use s
       solve_by_elim [εClosure.step]
-  · intro ⟨_, _, h⟩
+  mpr := by
+    intro ⟨_, _, h⟩
     induction' h <;> subst_vars <;> solve_by_elim [εClosure.step]
 
 /-- `M.stepSet S a` is the union of the ε-closure of `M.step s a` for all `s ∈ S`. -/
@@ -163,33 +163,33 @@ theorem Path.eq_of_nil (s t : σ) : M.Path s t [] → s = t := by
   rfl
 
 @[simp]
-theorem path_singleton {s t : σ} {a : Option α} : M.Path s t [a] ↔ t ∈ M.step s a := by
-  constructor
-  · intro h
+theorem path_singleton {s t : σ} {a : Option α} : M.Path s t [a] ↔ t ∈ M.step s a where
+  mp := by
+    intro h
     cases' h with _ _ _ _ _ _ _ h
     apply Path.eq_of_nil at h
     subst t
     assumption
-  · tauto
+  mpr := by tauto
 
 @[simp]
 theorem path_append {s u : σ} {x y : List (Option α)} :
-    M.Path s u (x ++ y) ↔ ∃ t, M.Path s t x ∧ M.Path t u y := by
-  constructor
-  · induction' x with _ _ ih generalizing s
+    M.Path s u (x ++ y) ↔ ∃ t, M.Path s t x ∧ M.Path t u y where
+  mp := by
+    induction' x with _ _ ih generalizing s
     · rw [List.nil_append]
       tauto
     · intro h
       cases' h with _ _ _ _ _ _ _ h
       obtain ⟨_, _, _⟩ := ih h
       tauto
-  · intro ⟨_, hx, _⟩
+  mpr := by
+    intro ⟨_, hx, _⟩
     induction' x generalizing s <;> cases hx <;> tauto
 
 theorem εClosure_path {s₁ s₂ : σ} :
-    s₂ ∈ M.εClosure {s₁} ↔ ∃ n, M.Path s₁ s₂ (List.replicate n none) := by
-  constructor
-  · intro h
+    s₂ ∈ M.εClosure {s₁} ↔ ∃ n, M.Path s₁ s₂ (List.replicate n none) where
+  mp h := by
     induction' h with t _ _ _ _ _ ih
     · use 0
       subst t
@@ -198,7 +198,8 @@ theorem εClosure_path {s₁ s₂ : σ} :
       use n + 1
       rw [List.replicate_add, path_append]
       tauto
-  · intro ⟨n, h⟩
+  mpr := by
+    intro ⟨n, h⟩
     induction' n generalizing s₂
     · rw [List.replicate_zero] at h
       apply Path.eq_of_nil at h
@@ -246,14 +247,15 @@ theorem evalFrom_path {s₁ s₂ : σ} {x : List α} :
 
 theorem accepts_path {x : List α} :
     x ∈ M.accepts ↔
-      ∃ s₁ s₂ x', s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.Path s₁ s₂ x' := by
-  constructor
-  · intro ⟨_, _, h⟩
+      ∃ s₁ s₂ x', s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.Path s₁ s₂ x' where
+  mp := by
+    intro ⟨_, _, h⟩
     rw [eval, mem_evalFrom_choice] at h
     obtain ⟨_, _, h⟩ := h
     rw [evalFrom_path] at h
     tauto
-  · intro ⟨_, _, _, hs₁, _, h⟩
+  mpr := by
+    intro ⟨_, _, _, hs₁, _, h⟩
     have := M.evalFrom_path.mpr ⟨_, h⟩
     have := M.mem_evalFrom_choice.mpr ⟨_, hs₁, this⟩
     tauto

From b03924679cc8acd3ec4cfc056b5305a096fe0672 Mon Sep 17 00:00:00 2001
From: Anthony DeRossi <aderossi@bu.edu>
Date: Sat, 18 Jan 2025 18:23:44 -0500
Subject: [PATCH 05/18] Simplify proofs

---
 Mathlib/Computability/EpsilonNFA.lean | 43 ++++++++++-----------------
 1 file changed, 15 insertions(+), 28 deletions(-)

diff --git a/Mathlib/Computability/EpsilonNFA.lean b/Mathlib/Computability/EpsilonNFA.lean
index 672be49313e71..54e46691f9dee 100644
--- a/Mathlib/Computability/EpsilonNFA.lean
+++ b/Mathlib/Computability/EpsilonNFA.lean
@@ -120,14 +120,8 @@ theorem mem_evalFrom_choice {s : σ} {S : Set σ} {x : List α} :
     s ∈ M.evalFrom S x ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} x := by
   induction' x using List.reverseRecOn with _ _ ih generalizing s
   · apply mem_εClosure_choice
-  · simp only [evalFrom_append_singleton, mem_stepSet_iff]
-    constructor <;> intro h
-    · obtain ⟨_, h, _⟩ := h
-      rw [ih] at h
-      tauto
-    · obtain ⟨_, ht, _, h, _⟩ := h
-      have := ih.mpr ⟨_, ht, h⟩
-      tauto
+  · simp_rw [evalFrom_append_singleton, mem_stepSet_iff, ih]
+    tauto
 
 /-- `M.eval x` computes all possible paths through `M` with input `x` starting at an element of
 `M.start`. -/
@@ -165,8 +159,7 @@ theorem Path.eq_of_nil (s t : σ) : M.Path s t [] → s = t := by
 @[simp]
 theorem path_singleton {s t : σ} {a : Option α} : M.Path s t [a] ↔ t ∈ M.step s a where
   mp := by
-    intro h
-    cases' h with _ _ _ _ _ _ _ h
+    rintro (_ | ⟨_, _, _, _, _, _, h⟩)
     apply Path.eq_of_nil at h
     subst t
     assumption
@@ -179,13 +172,12 @@ theorem path_append {s u : σ} {x y : List (Option α)} :
     induction' x with _ _ ih generalizing s
     · rw [List.nil_append]
       tauto
-    · intro h
-      cases' h with _ _ _ _ _ _ _ h
-      obtain ⟨_, _, _⟩ := ih h
+    · rintro (_ | ⟨_, _, _, _, _, _, h⟩)
+      apply ih at h
       tauto
   mpr := by
     intro ⟨_, hx, _⟩
-    induction' x generalizing s <;> cases hx <;> tauto
+    induction x generalizing s <;> cases hx <;> tauto
 
 theorem εClosure_path {s₁ s₂ : σ} :
     s₂ ∈ M.εClosure {s₁} ↔ ∃ n, M.Path s₁ s₂ (List.replicate n none) where
@@ -200,7 +192,7 @@ theorem εClosure_path {s₁ s₂ : σ} :
       tauto
   mpr := by
     intro ⟨n, h⟩
-    induction' n generalizing s₂
+    induction n generalizing s₂
     · rw [List.replicate_zero] at h
       apply Path.eq_of_nil at h
       solve_by_elim
@@ -217,27 +209,23 @@ theorem evalFrom_path {s₁ s₂ : σ} {x : List α} :
       use List.replicate n none
       rw [List.reduceOption_replicate_none]
       trivial
-    · intro ⟨_, hx⟩
-      rw [List.reduceOption_eq_nil_iff] at hx
-      obtain ⟨⟨_, ⟨⟩⟩, _⟩ := hx
+    · simp_rw [List.reduceOption_eq_nil_iff]
+      rintro ⟨_, ⟨⟨_, ⟨⟩⟩, _⟩⟩
       tauto
   · rw [evalFrom_append_singleton, mem_stepSet_iff]
     constructor
     · intro ⟨_, ht, h⟩
       obtain ⟨x', _, _⟩ := ih.mp ht
       rw [mem_εClosure_choice] at h
-      obtain ⟨_, _, h⟩ := h
-      rw [εClosure_path] at h
-      obtain ⟨n, _⟩ := h
+      simp_rw [εClosure_path] at h
+      obtain ⟨_, _, ⟨n, _⟩⟩ := h
       use x' ++ some a :: List.replicate n none
       rw [List.reduceOption_append, List.reduceOption_cons_of_some,
         List.reduceOption_replicate_none, path_append]
       tauto
-    · intro ⟨_, hx, h⟩
-      rw [← List.concat_eq_append, List.reduceOption_eq_concat_iff] at hx
-      obtain ⟨_, _, ⟨⟩, _, hx₂⟩ := hx
-      rw [List.reduceOption_eq_nil_iff] at hx₂
-      obtain ⟨_, ⟨⟩⟩ := hx₂
+    · simp_rw [← List.concat_eq_append, List.reduceOption_eq_concat_iff,
+        List.reduceOption_eq_nil_iff]
+      rintro ⟨_, ⟨_, _, ⟨⟩, _, ⟨_, ⟨⟩⟩⟩, h⟩
       rw [path_append] at h
       obtain ⟨t, _, _ | _⟩ := h
       use t
@@ -256,8 +244,7 @@ theorem accepts_path {x : List α} :
     tauto
   mpr := by
     intro ⟨_, _, _, hs₁, _, h⟩
-    have := M.evalFrom_path.mpr ⟨_, h⟩
-    have := M.mem_evalFrom_choice.mpr ⟨_, hs₁, this⟩
+    have := M.mem_evalFrom_choice.mpr ⟨_, hs₁, M.evalFrom_path.mpr ⟨_, h⟩⟩
     tauto
 
 /-! ### Conversions between `εNFA` and `NFA` -/

From 5d2cfee28bb38c8d55205bc80d8f1dd0b4b5dd19 Mon Sep 17 00:00:00 2001
From: Anthony DeRossi <aderossi@bu.edu>
Date: Sun, 19 Jan 2025 18:55:13 -0500
Subject: [PATCH 06/18] Rename `Path` to `IsPath`

`IsPath` is more appropriate for a `Prop` definition. Related theorems
are also renamed.
---
 Mathlib/Computability/EpsilonNFA.lean | 38 ++++++++++++++-------------
 1 file changed, 20 insertions(+), 18 deletions(-)

diff --git a/Mathlib/Computability/EpsilonNFA.lean b/Mathlib/Computability/EpsilonNFA.lean
index 54e46691f9dee..50ed7fefb6ade 100644
--- a/Mathlib/Computability/EpsilonNFA.lean
+++ b/Mathlib/Computability/EpsilonNFA.lean
@@ -144,30 +144,32 @@ theorem eval_append_singleton (x : List α) (a : α) : M.eval (x ++ [a]) = M.ste
 def accepts : Language α :=
   { x | ∃ S ∈ M.accept, S ∈ M.eval x }
 
-/-- An `M.Path` represents a traversal in `M` from a start state to an end state by following a list
+/-- `M.IsPath` represents a traversal in `M` from a start state to an end state by following a list
   of transitions in order. -/
-inductive Path : σ → σ → List (Option α) → Prop
-  | nil : ∀ s, Path s s []
+inductive IsPath : σ → σ → List (Option α) → Prop
+  | nil : ∀ s, IsPath s s []
   | cons (t s u : σ) (a : Option α) (x : List (Option α)) :
-      t ∈ M.step s a → Path t u x → Path s u (a :: x)
+      t ∈ M.step s a → IsPath t u x → IsPath s u (a :: x)
 
-theorem Path.eq_of_nil (s t : σ) : M.Path s t [] → s = t := by
+theorem IsPath.eq_of_nil {s t : σ} : M.IsPath s t [] → s = t := by
   intro h
   cases h
   rfl
 
 @[simp]
-theorem path_singleton {s t : σ} {a : Option α} : M.Path s t [a] ↔ t ∈ M.step s a where
+theorem isPath_singleton {s t : σ} {a : Option α} : M.IsPath s t [a] ↔ t ∈ M.step s a where
   mp := by
     rintro (_ | ⟨_, _, _, _, _, _, h⟩)
-    apply Path.eq_of_nil at h
+    apply IsPath.eq_of_nil at h
     subst t
     assumption
   mpr := by tauto
 
+alias ⟨_, IsPath.singleton⟩ := isPath_singleton
+
 @[simp]
-theorem path_append {s u : σ} {x y : List (Option α)} :
-    M.Path s u (x ++ y) ↔ ∃ t, M.Path s t x ∧ M.Path t u y where
+theorem isPath_append {s u : σ} {x y : List (Option α)} :
+    M.IsPath s u (x ++ y) ↔ ∃ t, M.IsPath s t x ∧ M.IsPath t u y where
   mp := by
     induction' x with _ _ ih generalizing s
     · rw [List.nil_append]
@@ -180,28 +182,28 @@ theorem path_append {s u : σ} {x y : List (Option α)} :
     induction x generalizing s <;> cases hx <;> tauto
 
 theorem εClosure_path {s₁ s₂ : σ} :
-    s₂ ∈ M.εClosure {s₁} ↔ ∃ n, M.Path s₁ s₂ (List.replicate n none) where
+    s₂ ∈ M.εClosure {s₁} ↔ ∃ n, M.IsPath s₁ s₂ (List.replicate n none) where
   mp h := by
     induction' h with t _ _ _ _ _ ih
     · use 0
       subst t
-      apply Path.nil
+      apply IsPath.nil
     · obtain ⟨n, _⟩ := ih
       use n + 1
-      rw [List.replicate_add, path_append]
+      rw [List.replicate_add, isPath_append]
       tauto
   mpr := by
     intro ⟨n, h⟩
     induction n generalizing s₂
     · rw [List.replicate_zero] at h
-      apply Path.eq_of_nil at h
+      apply IsPath.eq_of_nil at h
       solve_by_elim
-    · simp_rw [List.replicate_add, path_append, List.replicate_one, path_singleton] at h
+    · simp_rw [List.replicate_add, isPath_append, List.replicate_one, isPath_singleton] at h
       obtain ⟨_, _, _⟩ := h
       solve_by_elim [εClosure.step]
 
 theorem evalFrom_path {s₁ s₂ : σ} {x : List α} :
-    s₂ ∈ M.evalFrom {s₁} x ↔ ∃ x', x'.reduceOption = x ∧ M.Path s₁ s₂ x' := by
+    s₂ ∈ M.evalFrom {s₁} x ↔ ∃ x', x'.reduceOption = x ∧ M.IsPath s₁ s₂ x' := by
   induction' x using List.reverseRecOn with _ a ih generalizing s₂
   · rw [evalFrom_nil, εClosure_path]
     constructor
@@ -221,12 +223,12 @@ theorem evalFrom_path {s₁ s₂ : σ} {x : List α} :
       obtain ⟨_, _, ⟨n, _⟩⟩ := h
       use x' ++ some a :: List.replicate n none
       rw [List.reduceOption_append, List.reduceOption_cons_of_some,
-        List.reduceOption_replicate_none, path_append]
+        List.reduceOption_replicate_none, isPath_append]
       tauto
     · simp_rw [← List.concat_eq_append, List.reduceOption_eq_concat_iff,
         List.reduceOption_eq_nil_iff]
       rintro ⟨_, ⟨_, _, ⟨⟩, _, ⟨_, ⟨⟩⟩⟩, h⟩
-      rw [path_append] at h
+      rw [isPath_append] at h
       obtain ⟨t, _, _ | _⟩ := h
       use t
       rw [mem_εClosure_choice, ih]
@@ -235,7 +237,7 @@ theorem evalFrom_path {s₁ s₂ : σ} {x : List α} :
 
 theorem accepts_path {x : List α} :
     x ∈ M.accepts ↔
-      ∃ s₁ s₂ x', s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.Path s₁ s₂ x' where
+      ∃ s₁ s₂ x', s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x' where
   mp := by
     intro ⟨_, _, h⟩
     rw [eval, mem_evalFrom_choice] at h

From cde8bf54f5ac27ab9366ea4a01ed4b663f3f0cbe Mon Sep 17 00:00:00 2001
From: Anthony DeRossi <aderossi@bu.edu>
Date: Sun, 19 Jan 2025 18:57:43 -0500
Subject: [PATCH 07/18] Remove `@[simp]` on `isPath_append`

---
 Mathlib/Computability/EpsilonNFA.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/Computability/EpsilonNFA.lean b/Mathlib/Computability/EpsilonNFA.lean
index 50ed7fefb6ade..220786dbf3cfd 100644
--- a/Mathlib/Computability/EpsilonNFA.lean
+++ b/Mathlib/Computability/EpsilonNFA.lean
@@ -167,7 +167,6 @@ theorem isPath_singleton {s t : σ} {a : Option α} : M.IsPath s t [a] ↔ t ∈
 
 alias ⟨_, IsPath.singleton⟩ := isPath_singleton
 
-@[simp]
 theorem isPath_append {s u : σ} {x y : List (Option α)} :
     M.IsPath s u (x ++ y) ↔ ∃ t, M.IsPath s t x ∧ M.IsPath t u y where
   mp := by

From 6fad8ccfe8ac587d7f045120360f20c3fadd19a6 Mon Sep 17 00:00:00 2001
From: Anthony DeRossi <aderossi@bu.edu>
Date: Sun, 19 Jan 2025 19:01:42 -0500
Subject: [PATCH 08/18] Rename `*_choice` theorems to `*_iff_exists`

---
 Mathlib/Computability/EpsilonNFA.lean | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Computability/EpsilonNFA.lean b/Mathlib/Computability/EpsilonNFA.lean
index 220786dbf3cfd..331c2da959d51 100644
--- a/Mathlib/Computability/EpsilonNFA.lean
+++ b/Mathlib/Computability/EpsilonNFA.lean
@@ -64,7 +64,7 @@ theorem εClosure_empty : M.εClosure ∅ = ∅ :=
 theorem εClosure_univ : M.εClosure univ = univ :=
   eq_univ_of_univ_subset <| subset_εClosure _ _
 
-theorem mem_εClosure_choice {s : σ} {S : Set σ} :
+theorem mem_εClosure_iff_exists {s : σ} {S : Set σ} :
     s ∈ M.εClosure S ↔ ∃ t ∈ S, s ∈ M.εClosure {t} where
   mp h := by
     induction' h with s _ _ _ _ _ ih
@@ -116,10 +116,10 @@ theorem evalFrom_empty (x : List α) : M.evalFrom ∅ x = ∅ := by
   · rw [evalFrom_nil, εClosure_empty]
   · rw [evalFrom_append_singleton, ih, stepSet_empty]
 
-theorem mem_evalFrom_choice {s : σ} {S : Set σ} {x : List α} :
+theorem mem_evalFrom_iff_exists {s : σ} {S : Set σ} {x : List α} :
     s ∈ M.evalFrom S x ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} x := by
   induction' x using List.reverseRecOn with _ _ ih generalizing s
-  · apply mem_εClosure_choice
+  · apply mem_εClosure_iff_exists
   · simp_rw [evalFrom_append_singleton, mem_stepSet_iff, ih]
     tauto
 
@@ -217,7 +217,7 @@ theorem evalFrom_path {s₁ s₂ : σ} {x : List α} :
     constructor
     · intro ⟨_, ht, h⟩
       obtain ⟨x', _, _⟩ := ih.mp ht
-      rw [mem_εClosure_choice] at h
+      rw [mem_εClosure_iff_exists] at h
       simp_rw [εClosure_path] at h
       obtain ⟨_, _, ⟨n, _⟩⟩ := h
       use x' ++ some a :: List.replicate n none
@@ -230,7 +230,7 @@ theorem evalFrom_path {s₁ s₂ : σ} {x : List α} :
       rw [isPath_append] at h
       obtain ⟨t, _, _ | _⟩ := h
       use t
-      rw [mem_εClosure_choice, ih]
+      rw [mem_εClosure_iff_exists, ih]
       simp_rw [εClosure_path]
       tauto
 
@@ -239,13 +239,13 @@ theorem accepts_path {x : List α} :
       ∃ s₁ s₂ x', s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x' where
   mp := by
     intro ⟨_, _, h⟩
-    rw [eval, mem_evalFrom_choice] at h
+    rw [eval, mem_evalFrom_iff_exists] at h
     obtain ⟨_, _, h⟩ := h
     rw [evalFrom_path] at h
     tauto
   mpr := by
     intro ⟨_, _, _, hs₁, _, h⟩
-    have := M.mem_evalFrom_choice.mpr ⟨_, hs₁, M.evalFrom_path.mpr ⟨_, h⟩⟩
+    have := M.mem_evalFrom_iff_exists.mpr ⟨_, hs₁, M.evalFrom_path.mpr ⟨_, h⟩⟩
     tauto
 
 /-! ### Conversions between `εNFA` and `NFA` -/

From 2a4753090cbd62808c9fa56f12c378c5a55a1878 Mon Sep 17 00:00:00 2001
From: Anthony DeRossi <aderossi@bu.edu>
Date: Sun, 19 Jan 2025 19:03:47 -0500
Subject: [PATCH 09/18] Rename `accepts_path` to `mem_accepts_iff_exists_path`

---
 Mathlib/Computability/EpsilonNFA.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Computability/EpsilonNFA.lean b/Mathlib/Computability/EpsilonNFA.lean
index 331c2da959d51..0243883d4673d 100644
--- a/Mathlib/Computability/EpsilonNFA.lean
+++ b/Mathlib/Computability/EpsilonNFA.lean
@@ -234,7 +234,7 @@ theorem evalFrom_path {s₁ s₂ : σ} {x : List α} :
       simp_rw [εClosure_path]
       tauto
 
-theorem accepts_path {x : List α} :
+theorem mem_accepts_iff_exists_path {x : List α} :
     x ∈ M.accepts ↔
       ∃ s₁ s₂ x', s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x' where
   mp := by

From fee8650e321f5fd1f13623b3a097ab0034d81629 Mon Sep 17 00:00:00 2001
From: Anthony DeRossi <aderossi@bu.edu>
Date: Sun, 19 Jan 2025 19:08:35 -0500
Subject: [PATCH 10/18] Simplify proofs

---
 Mathlib/Computability/EpsilonNFA.lean | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Computability/EpsilonNFA.lean b/Mathlib/Computability/EpsilonNFA.lean
index 0243883d4673d..d0be7d50dcff9 100644
--- a/Mathlib/Computability/EpsilonNFA.lean
+++ b/Mathlib/Computability/EpsilonNFA.lean
@@ -152,16 +152,13 @@ inductive IsPath : σ → σ → List (Option α) → Prop
       t ∈ M.step s a → IsPath t u x → IsPath s u (a :: x)
 
 theorem IsPath.eq_of_nil {s t : σ} : M.IsPath s t [] → s = t := by
-  intro h
-  cases h
+  rintro ⟨⟩
   rfl
 
 @[simp]
 theorem isPath_singleton {s t : σ} {a : Option α} : M.IsPath s t [a] ↔ t ∈ M.step s a where
   mp := by
-    rintro (_ | ⟨_, _, _, _, _, _, h⟩)
-    apply IsPath.eq_of_nil at h
-    subst t
+    rintro (_ | ⟨_, _, _, _, _, _, ⟨⟩⟩)
     assumption
   mpr := by tauto
 

From 76cc5a61e595b8f93fd4a5c7f331d802cf5216c5 Mon Sep 17 00:00:00 2001
From: Anthony DeRossi <aderossi@bu.edu>
Date: Tue, 21 Jan 2025 11:07:20 -0500
Subject: [PATCH 11/18] Unindent docstring

---
 Mathlib/Computability/EpsilonNFA.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Computability/EpsilonNFA.lean b/Mathlib/Computability/EpsilonNFA.lean
index d0be7d50dcff9..b2951fc838114 100644
--- a/Mathlib/Computability/EpsilonNFA.lean
+++ b/Mathlib/Computability/EpsilonNFA.lean
@@ -145,7 +145,7 @@ def accepts : Language α :=
   { x | ∃ S ∈ M.accept, S ∈ M.eval x }
 
 /-- `M.IsPath` represents a traversal in `M` from a start state to an end state by following a list
-  of transitions in order. -/
+of transitions in order. -/
 inductive IsPath : σ → σ → List (Option α) → Prop
   | nil : ∀ s, IsPath s s []
   | cons (t s u : σ) (a : Option α) (x : List (Option α)) :

From d59aaa203b6b9b831b422e79b833876effc4f7bc Mon Sep 17 00:00:00 2001
From: Anthony DeRossi <aderossi@bu.edu>
Date: Tue, 21 Jan 2025 11:21:55 -0500
Subject: [PATCH 12/18] Move common variables to the `variable` declaration

---
 Mathlib/Computability/EpsilonNFA.lean | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Computability/EpsilonNFA.lean b/Mathlib/Computability/EpsilonNFA.lean
index b2951fc838114..a3b88fb781ef5 100644
--- a/Mathlib/Computability/EpsilonNFA.lean
+++ b/Mathlib/Computability/EpsilonNFA.lean
@@ -42,7 +42,7 @@ structure εNFA (α : Type u) (σ : Type v) where
   /-- Set of acceptance states. -/
   accept : Set σ
 
-variable {α : Type u} {σ : Type v} (M : εNFA α σ) {S : Set σ} {s : σ} {a : α}
+variable {α : Type u} {σ : Type v} (M : εNFA α σ) {S : Set σ} {s t u : σ} {a : α}
 
 namespace εNFA
 
@@ -64,8 +64,7 @@ theorem εClosure_empty : M.εClosure ∅ = ∅ :=
 theorem εClosure_univ : M.εClosure univ = univ :=
   eq_univ_of_univ_subset <| subset_εClosure _ _
 
-theorem mem_εClosure_iff_exists {s : σ} {S : Set σ} :
-    s ∈ M.εClosure S ↔ ∃ t ∈ S, s ∈ M.εClosure {t} where
+theorem mem_εClosure_iff_exists : s ∈ M.εClosure S ↔ ∃ t ∈ S, s ∈ M.εClosure {t} where
   mp h := by
     induction' h with s _ _ _ _ _ ih
     · tauto
@@ -151,12 +150,12 @@ inductive IsPath : σ → σ → List (Option α) → Prop
   | cons (t s u : σ) (a : Option α) (x : List (Option α)) :
       t ∈ M.step s a → IsPath t u x → IsPath s u (a :: x)
 
-theorem IsPath.eq_of_nil {s t : σ} : M.IsPath s t [] → s = t := by
+theorem IsPath.eq_of_nil : M.IsPath s t [] → s = t := by
   rintro ⟨⟩
   rfl
 
 @[simp]
-theorem isPath_singleton {s t : σ} {a : Option α} : M.IsPath s t [a] ↔ t ∈ M.step s a where
+theorem isPath_singleton {a : Option α} : M.IsPath s t [a] ↔ t ∈ M.step s a where
   mp := by
     rintro (_ | ⟨_, _, _, _, _, _, ⟨⟩⟩)
     assumption
@@ -164,7 +163,7 @@ theorem isPath_singleton {s t : σ} {a : Option α} : M.IsPath s t [a] ↔ t ∈
 
 alias ⟨_, IsPath.singleton⟩ := isPath_singleton
 
-theorem isPath_append {s u : σ} {x y : List (Option α)} :
+theorem isPath_append {x y : List (Option α)} :
     M.IsPath s u (x ++ y) ↔ ∃ t, M.IsPath s t x ∧ M.IsPath t u y where
   mp := by
     induction' x with _ _ ih generalizing s

From d733eb1d79b16942d224657b10aefe063de4cb64 Mon Sep 17 00:00:00 2001
From: Anthony DeRossi <aderossi@bu.edu>
Date: Tue, 21 Jan 2025 11:25:56 -0500
Subject: [PATCH 13/18] Use `@[mk_iff]` on `IsPath`

---
 Mathlib/Computability/EpsilonNFA.lean | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Computability/EpsilonNFA.lean b/Mathlib/Computability/EpsilonNFA.lean
index a3b88fb781ef5..58624644683e1 100644
--- a/Mathlib/Computability/EpsilonNFA.lean
+++ b/Mathlib/Computability/EpsilonNFA.lean
@@ -145,14 +145,18 @@ def accepts : Language α :=
 
 /-- `M.IsPath` represents a traversal in `M` from a start state to an end state by following a list
 of transitions in order. -/
+@[mk_iff]
 inductive IsPath : σ → σ → List (Option α) → Prop
-  | nil : ∀ s, IsPath s s []
+  | nil (s : σ) : IsPath s s []
   | cons (t s u : σ) (a : Option α) (x : List (Option α)) :
       t ∈ M.step s a → IsPath t u x → IsPath s u (a :: x)
 
-theorem IsPath.eq_of_nil : M.IsPath s t [] → s = t := by
-  rintro ⟨⟩
-  rfl
+@[simp]
+theorem isPath_nil : M.IsPath s t [] ↔ s = t := by
+  rw [isPath_iff]
+  simp [eq_comm]
+
+alias ⟨IsPath.eq_of_nil, _⟩ := isPath_nil
 
 @[simp]
 theorem isPath_singleton {a : Option α} : M.IsPath s t [a] ↔ t ∈ M.step s a where

From 101bb158b9cff1dc51a58f67dcb6ff6b1acf2c19 Mon Sep 17 00:00:00 2001
From: Anthony DeRossi <aderossi@bu.edu>
Date: Tue, 21 Jan 2025 11:29:00 -0500
Subject: [PATCH 14/18] Rename `*_path` theorems to `*_iff_exists_path`

---
 Mathlib/Computability/EpsilonNFA.lean | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Computability/EpsilonNFA.lean b/Mathlib/Computability/EpsilonNFA.lean
index 58624644683e1..45b417046b0fa 100644
--- a/Mathlib/Computability/EpsilonNFA.lean
+++ b/Mathlib/Computability/EpsilonNFA.lean
@@ -180,7 +180,7 @@ theorem isPath_append {x y : List (Option α)} :
     intro ⟨_, hx, _⟩
     induction x generalizing s <;> cases hx <;> tauto
 
-theorem εClosure_path {s₁ s₂ : σ} :
+theorem mem_εClosure_iff_exists_path {s₁ s₂ : σ} :
     s₂ ∈ M.εClosure {s₁} ↔ ∃ n, M.IsPath s₁ s₂ (List.replicate n none) where
   mp h := by
     induction' h with t _ _ _ _ _ ih
@@ -201,10 +201,10 @@ theorem εClosure_path {s₁ s₂ : σ} :
       obtain ⟨_, _, _⟩ := h
       solve_by_elim [εClosure.step]
 
-theorem evalFrom_path {s₁ s₂ : σ} {x : List α} :
+theorem mem_evalFrom_iff_exists_path {s₁ s₂ : σ} {x : List α} :
     s₂ ∈ M.evalFrom {s₁} x ↔ ∃ x', x'.reduceOption = x ∧ M.IsPath s₁ s₂ x' := by
   induction' x using List.reverseRecOn with _ a ih generalizing s₂
-  · rw [evalFrom_nil, εClosure_path]
+  · rw [evalFrom_nil, mem_εClosure_iff_exists_path]
     constructor
     · intro ⟨n, _⟩
       use List.replicate n none
@@ -218,7 +218,7 @@ theorem evalFrom_path {s₁ s₂ : σ} {x : List α} :
     · intro ⟨_, ht, h⟩
       obtain ⟨x', _, _⟩ := ih.mp ht
       rw [mem_εClosure_iff_exists] at h
-      simp_rw [εClosure_path] at h
+      simp_rw [mem_εClosure_iff_exists_path] at h
       obtain ⟨_, _, ⟨n, _⟩⟩ := h
       use x' ++ some a :: List.replicate n none
       rw [List.reduceOption_append, List.reduceOption_cons_of_some,
@@ -231,7 +231,7 @@ theorem evalFrom_path {s₁ s₂ : σ} {x : List α} :
       obtain ⟨t, _, _ | _⟩ := h
       use t
       rw [mem_εClosure_iff_exists, ih]
-      simp_rw [εClosure_path]
+      simp_rw [mem_εClosure_iff_exists_path]
       tauto
 
 theorem mem_accepts_iff_exists_path {x : List α} :
@@ -241,11 +241,11 @@ theorem mem_accepts_iff_exists_path {x : List α} :
     intro ⟨_, _, h⟩
     rw [eval, mem_evalFrom_iff_exists] at h
     obtain ⟨_, _, h⟩ := h
-    rw [evalFrom_path] at h
+    rw [mem_evalFrom_iff_exists_path] at h
     tauto
   mpr := by
     intro ⟨_, _, _, hs₁, _, h⟩
-    have := M.mem_evalFrom_iff_exists.mpr ⟨_, hs₁, M.evalFrom_path.mpr ⟨_, h⟩⟩
+    have := M.mem_evalFrom_iff_exists.mpr ⟨_, hs₁, M.mem_evalFrom_iff_exists_path.mpr ⟨_, h⟩⟩
     tauto
 
 /-! ### Conversions between `εNFA` and `NFA` -/

From 32870b424b20c7adcfe24889f35cdcf59fa9f761 Mon Sep 17 00:00:00 2001
From: Anthony DeRossi <aderossi@bu.edu>
Date: Tue, 21 Jan 2025 11:34:20 -0500
Subject: [PATCH 15/18] Use `rfl` for substitutions on intro

---
 Mathlib/Computability/EpsilonNFA.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Computability/EpsilonNFA.lean b/Mathlib/Computability/EpsilonNFA.lean
index 45b417046b0fa..5ce504443755d 100644
--- a/Mathlib/Computability/EpsilonNFA.lean
+++ b/Mathlib/Computability/EpsilonNFA.lean
@@ -211,7 +211,7 @@ theorem mem_evalFrom_iff_exists_path {s₁ s₂ : σ} {x : List α} :
       rw [List.reduceOption_replicate_none]
       trivial
     · simp_rw [List.reduceOption_eq_nil_iff]
-      rintro ⟨_, ⟨⟨_, ⟨⟩⟩, _⟩⟩
+      rintro ⟨_, ⟨⟨_, rfl⟩, _⟩⟩
       tauto
   · rw [evalFrom_append_singleton, mem_stepSet_iff]
     constructor
@@ -226,7 +226,7 @@ theorem mem_evalFrom_iff_exists_path {s₁ s₂ : σ} {x : List α} :
       tauto
     · simp_rw [← List.concat_eq_append, List.reduceOption_eq_concat_iff,
         List.reduceOption_eq_nil_iff]
-      rintro ⟨_, ⟨_, _, ⟨⟩, _, ⟨_, ⟨⟩⟩⟩, h⟩
+      rintro ⟨_, ⟨_, _, rfl, _, _, rfl⟩, h⟩
       rw [isPath_append] at h
       obtain ⟨t, _, _ | _⟩ := h
       use t

From 4f9cfa0bc21e53d16b346c376c17b9ab568da0c9 Mon Sep 17 00:00:00 2001
From: Anthony DeRossi <aderossi@bu.edu>
Date: Tue, 21 Jan 2025 12:14:39 -0500
Subject: [PATCH 16/18] Name variables in theorems

Some `tauto` occurrences are replaced by `exact` with named variables.
---
 Mathlib/Computability/EpsilonNFA.lean | 32 +++++++++++++--------------
 1 file changed, 16 insertions(+), 16 deletions(-)

diff --git a/Mathlib/Computability/EpsilonNFA.lean b/Mathlib/Computability/EpsilonNFA.lean
index 5ce504443755d..b95a42a23c768 100644
--- a/Mathlib/Computability/EpsilonNFA.lean
+++ b/Mathlib/Computability/EpsilonNFA.lean
@@ -72,7 +72,7 @@ theorem mem_εClosure_iff_exists : s ∈ M.εClosure S ↔ ∃ t ∈ S, s ∈ M.
       use s
       solve_by_elim [εClosure.step]
   mpr := by
-    intro ⟨_, _, h⟩
+    intro ⟨t, _, h⟩
     induction' h <;> subst_vars <;> solve_by_elim [εClosure.step]
 
 /-- `M.stepSet S a` is the union of the ε-closure of `M.step s a` for all `s ∈ S`. -/
@@ -170,14 +170,14 @@ alias ⟨_, IsPath.singleton⟩ := isPath_singleton
 theorem isPath_append {x y : List (Option α)} :
     M.IsPath s u (x ++ y) ↔ ∃ t, M.IsPath s t x ∧ M.IsPath t u y where
   mp := by
-    induction' x with _ _ ih generalizing s
+    induction' x with x a ih generalizing s
     · rw [List.nil_append]
       tauto
-    · rintro (_ | ⟨_, _, _, _, _, _, h⟩)
+    · rintro (_ | ⟨t, _, _, _, _, _, h⟩)
       apply ih at h
       tauto
   mpr := by
-    intro ⟨_, hx, _⟩
+    intro ⟨t, hx, _⟩
     induction x generalizing s <;> cases hx <;> tauto
 
 theorem mem_εClosure_iff_exists_path {s₁ s₂ : σ} :
@@ -198,12 +198,12 @@ theorem mem_εClosure_iff_exists_path {s₁ s₂ : σ} :
       apply IsPath.eq_of_nil at h
       solve_by_elim
     · simp_rw [List.replicate_add, isPath_append, List.replicate_one, isPath_singleton] at h
-      obtain ⟨_, _, _⟩ := h
+      obtain ⟨t, _, _⟩ := h
       solve_by_elim [εClosure.step]
 
 theorem mem_evalFrom_iff_exists_path {s₁ s₂ : σ} {x : List α} :
     s₂ ∈ M.evalFrom {s₁} x ↔ ∃ x', x'.reduceOption = x ∧ M.IsPath s₁ s₂ x' := by
-  induction' x using List.reverseRecOn with _ a ih generalizing s₂
+  induction' x using List.reverseRecOn with x a ih generalizing s₂
   · rw [evalFrom_nil, mem_εClosure_iff_exists_path]
     constructor
     · intro ⟨n, _⟩
@@ -211,24 +211,24 @@ theorem mem_evalFrom_iff_exists_path {s₁ s₂ : σ} {x : List α} :
       rw [List.reduceOption_replicate_none]
       trivial
     · simp_rw [List.reduceOption_eq_nil_iff]
-      rintro ⟨_, ⟨⟨_, rfl⟩, _⟩⟩
-      tauto
+      intro ⟨_, ⟨⟨n, rfl⟩, h⟩⟩
+      exact ⟨n, h⟩
   · rw [evalFrom_append_singleton, mem_stepSet_iff]
     constructor
-    · intro ⟨_, ht, h⟩
+    · intro ⟨t, ht, h⟩
       obtain ⟨x', _, _⟩ := ih.mp ht
       rw [mem_εClosure_iff_exists] at h
       simp_rw [mem_εClosure_iff_exists_path] at h
-      obtain ⟨_, _, ⟨n, _⟩⟩ := h
+      obtain ⟨u, _, ⟨n, _⟩⟩ := h
       use x' ++ some a :: List.replicate n none
       rw [List.reduceOption_append, List.reduceOption_cons_of_some,
         List.reduceOption_replicate_none, isPath_append]
       tauto
     · simp_rw [← List.concat_eq_append, List.reduceOption_eq_concat_iff,
         List.reduceOption_eq_nil_iff]
-      rintro ⟨_, ⟨_, _, rfl, _, _, rfl⟩, h⟩
+      intro ⟨_, ⟨x', _, rfl, _, n, rfl⟩, h⟩
       rw [isPath_append] at h
-      obtain ⟨t, _, _ | _⟩ := h
+      obtain ⟨t, _, _ | u⟩ := h
       use t
       rw [mem_εClosure_iff_exists, ih]
       simp_rw [mem_εClosure_iff_exists_path]
@@ -238,15 +238,15 @@ theorem mem_accepts_iff_exists_path {x : List α} :
     x ∈ M.accepts ↔
       ∃ s₁ s₂ x', s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x' where
   mp := by
-    intro ⟨_, _, h⟩
+    intro ⟨s₂, _, h⟩
     rw [eval, mem_evalFrom_iff_exists] at h
-    obtain ⟨_, _, h⟩ := h
+    obtain ⟨s₁, _, h⟩ := h
     rw [mem_evalFrom_iff_exists_path] at h
     tauto
   mpr := by
-    intro ⟨_, _, _, hs₁, _, h⟩
+    intro ⟨s₁, s₂, x', hs₁, hs₂, h⟩
     have := M.mem_evalFrom_iff_exists.mpr ⟨_, hs₁, M.mem_evalFrom_iff_exists_path.mpr ⟨_, h⟩⟩
-    tauto
+    exact ⟨s₂, hs₂, this⟩
 
 /-! ### Conversions between `εNFA` and `NFA` -/
 

From 2cbaadd9f9f3ffaa8b3985720ea44d83be5ebe8a Mon Sep 17 00:00:00 2001
From: Anthony DeRossi <aderossi@bu.edu>
Date: Tue, 21 Jan 2025 18:03:12 -0500
Subject: [PATCH 17/18] Remove unnecessary brackets

---
 Mathlib/Computability/EpsilonNFA.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Computability/EpsilonNFA.lean b/Mathlib/Computability/EpsilonNFA.lean
index b95a42a23c768..9998813a86596 100644
--- a/Mathlib/Computability/EpsilonNFA.lean
+++ b/Mathlib/Computability/EpsilonNFA.lean
@@ -211,7 +211,7 @@ theorem mem_evalFrom_iff_exists_path {s₁ s₂ : σ} {x : List α} :
       rw [List.reduceOption_replicate_none]
       trivial
     · simp_rw [List.reduceOption_eq_nil_iff]
-      intro ⟨_, ⟨⟨n, rfl⟩, h⟩⟩
+      intro ⟨_, ⟨n, rfl⟩, h⟩
       exact ⟨n, h⟩
   · rw [evalFrom_append_singleton, mem_stepSet_iff]
     constructor
@@ -219,7 +219,7 @@ theorem mem_evalFrom_iff_exists_path {s₁ s₂ : σ} {x : List α} :
       obtain ⟨x', _, _⟩ := ih.mp ht
       rw [mem_εClosure_iff_exists] at h
       simp_rw [mem_εClosure_iff_exists_path] at h
-      obtain ⟨u, _, ⟨n, _⟩⟩ := h
+      obtain ⟨u, _, n, _⟩ := h
       use x' ++ some a :: List.replicate n none
       rw [List.reduceOption_append, List.reduceOption_cons_of_some,
         List.reduceOption_replicate_none, isPath_append]

From 4990674dfed79ce37cfbd4ff300a68bdc4574a25 Mon Sep 17 00:00:00 2001
From: Anthony DeRossi <aderossi@bu.edu>
Date: Wed, 22 Jan 2025 13:11:04 -0500
Subject: [PATCH 18/18] Change `List.replicate` to `.replicate`

---
 Mathlib/Computability/EpsilonNFA.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Computability/EpsilonNFA.lean b/Mathlib/Computability/EpsilonNFA.lean
index 9998813a86596..f1fca2ebd4e3c 100644
--- a/Mathlib/Computability/EpsilonNFA.lean
+++ b/Mathlib/Computability/EpsilonNFA.lean
@@ -181,7 +181,7 @@ theorem isPath_append {x y : List (Option α)} :
     induction x generalizing s <;> cases hx <;> tauto
 
 theorem mem_εClosure_iff_exists_path {s₁ s₂ : σ} :
-    s₂ ∈ M.εClosure {s₁} ↔ ∃ n, M.IsPath s₁ s₂ (List.replicate n none) where
+    s₂ ∈ M.εClosure {s₁} ↔ ∃ n, M.IsPath s₁ s₂ (.replicate n none) where
   mp h := by
     induction' h with t _ _ _ _ _ ih
     · use 0