awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
s : σ
S : Set σ
a : α
⊢ s ∈ M.stepSet S a ↔ ∃ t ∈ S, s ∈ M.step t a

Tactic:
simp [stepSet]

Premises used: NFA.stepSet
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
a : α
⊢ M.stepSet ∅ a = ∅

Tactic:
simp [stepSet]

Premises used: NFA.stepSet
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
s : σ
a : α
⊢ M.stepSet {s} a = M.step s a

Tactic:
simp [stepSet]

Premises used: NFA.stepSet
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
a : α
h : ∀ (s : σ), s ∈ M.stepSet (S ∪ T) a ↔ s ∈ M.stepSet S a ∪ M.stepSet T a
⊢ M.stepSet (S ∪ T) a = M.stepSet S a ∪ M.stepSet T a

Tactic:
ext s
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
a : α
s : σ
⊢ s ∈ M.stepSet (S ∪ T) a ↔ s ∈ M.stepSet S a ∪ M.stepSet T a

Tactic:
simp [mem_stepSet, or_and_right, exists_or]

Premises used: exists_or, or_and_right, NFA.mem_stepSet
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
⊢ M.evalFrom S [] = S

Tactic:
rfl

Premises used: NFA.evalFrom, List.foldl, rfl
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
a : α
⊢ M.evalFrom S [a] = M.stepSet S a

Tactic:
rfl

Premises used: iSup, NFA.evalFrom, List.foldl, NFA.stepSet, Set.iUnion, rfl
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
a : α
x : List α
⊢ M.evalFrom S (a :: x) = M.evalFrom (M.stepSet S a) x

Tactic:
rfl

Premises used: iSup, NFA.evalFrom, setOf, List.foldl, NFA.stepSet, Set.iUnion, rfl
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
x y : List α
⊢ M.evalFrom S (x ++ y) = M.evalFrom (M.evalFrom S x) y

Tactic:
simp only [evalFrom, List.foldl_append]

Premises used: NFA.evalFrom, List.foldl_append
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
x : List α
a : α
⊢ M.evalFrom S (x ++ [a]) = M.stepSet (M.evalFrom S x) a

Tactic:
simp only [evalFrom_append, evalFrom_cons, evalFrom_nil]

Premises used: NFA.evalFrom_append, NFA.evalFrom_cons, NFA.evalFrom_nil
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
⊢ M.evalFrom (S ∪ T) [] = M.evalFrom S [] ∪ M.evalFrom T []

Tactic:
simp
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
a : α
x : List α
ih : ∀ (S T : Set σ), M.evalFrom (S ∪ T) x = M.evalFrom S x ∪ M.evalFrom T x
S T : Set σ
⊢ M.evalFrom (S ∪ T) (a :: x) = M.evalFrom S (a :: x) ∪ M.evalFrom T (a :: x)

Tactic:
simp [ih]
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
nil : ∀ (S T : Set σ), M.evalFrom (S ∪ T) [] = M.evalFrom S [] ∪ M.evalFrom T []
cons :
  ∀ (a : α) (x : List α) (ih : ∀ (S T : Set σ), M.evalFrom (S ∪ T) x = M.evalFrom S x ∪ M.evalFrom T x) (S T : Set σ),
    M.evalFrom (S ∪ T) (a :: x) = M.evalFrom S (a :: x) ∪ M.evalFrom T (a :: x)
⊢ M.evalFrom (S ∪ T) x = M.evalFrom S x ∪ M.evalFrom T x

Tactic:
induction x generalizing S T with
  | nil => simp
  | cons a x ih => simp [ih]
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
ι : Sort u_1
s : ι → Set σ
⊢ M.evalFrom (⋃ (i : ι), s i) [] = ⋃ (i : ι), M.evalFrom (s i) []

Tactic:
simp
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
ι : Sort u_1
a : α
x : List α
ih : ∀ (s : ι → Set σ), M.evalFrom (⋃ (i : ι), s i) x = ⋃ (i : ι), M.evalFrom (s i) x
s : ι → Set σ
⊢ M.evalFrom (⋃ (i : ι), s i) (a :: x) = ⋃ (i : ι), M.evalFrom (s i) (a :: x)

Tactic:
simp [stepSet, Set.iUnion_comm (ι := σ) (ι' := ι), ih]

Premises used: Set.iUnion_comm, NFA.stepSet
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
ι : Sort u_1
s : ι → Set σ
x : List α
nil : ∀ (s : ι → Set σ), M.evalFrom (⋃ (i : ι), s i) [] = ⋃ (i : ι), M.evalFrom (s i) []
cons :
  ∀ (a : α) (x : List α) (ih : ∀ (s : ι → Set σ), M.evalFrom (⋃ (i : ι), s i) x = ⋃ (i : ι), M.evalFrom (s i) x)
    (s : ι → Set σ), M.evalFrom (⋃ (i : ι), s i) (a :: x) = ⋃ (i : ι), M.evalFrom (s i) (a :: x)
⊢ M.evalFrom (⋃ (i : ι), s i) x = ⋃ (i : ι), M.evalFrom (s i) x

Tactic:
induction x generalizing s with
  | nil => simp
  | cons a x ih => simp [stepSet, Set.iUnion_comm (ι := σ) (ι' := ι), ih]

Premises used: Set.iUnion_comm, NFA.stepSet
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
ι : Sort u_1
κ : ι → Sort u_2
f : (i : ι) → κ i → Set σ
x : List α
⊢ M.evalFrom (⋃ (i : ι), ⋃ (j : κ i), f i j) x = ⋃ (i : ι), ⋃ (j : κ i), M.evalFrom (f i j) x

Tactic:
simp
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
ι : Type u_1
t : Set ι
f : ι → Set σ
⊢ M.evalFrom (⋃ i ∈ t, f i) [] = ⋃ i ∈ t, M.evalFrom (f i) []

Tactic:
simp
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
ι : Type u_1
t : Set ι
f : ι → Set σ
a : α
x : List α
⊢ M.evalFrom (⋃ i ∈ t, f i) (a :: x) = ⋃ i ∈ t, M.evalFrom (f i) (a :: x)

Tactic:
simp [stepSet, evalFrom_biUnion _ _ x]

Premises used: NFA.stepSet
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
x : List α
⊢ M.evalFrom S x = ⋃ s ∈ S, M.evalFrom {s} x

Tactic:
simp [← evalFrom_iUnion₂]

Premises used: NFA.evalFrom_iUnion₂
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
s : σ
S : Set σ
x : List α
rw : Membership.mem (γ := Set σ) (⋃ s ∈ S, M.evalFrom {s} x) s ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} x
⊢ s ∈ M.evalFrom S x ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} x

Tactic:
rw [evalFrom_eq_biUnion_singleton]

Premises used: NFA.evalFrom_eq_biUnion_singleton
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
s : σ
S : Set σ
x : List α
⊢ Membership.mem (γ := Set σ) (⋃ s ∈ S, M.evalFrom {s} x) s ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} x

Tactic:
simp
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
x : List α
⊢ x ∈ M.acceptsFrom S ↔ ∃ s ∈ M.accept, s ∈ M.evalFrom S x

Tactic:
rfl
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
simp : (∃ s ∈ M.accept, s ∈ S) ↔ ∃ s ∈ S, s ∈ M.accept
⊢ [] ∈ M.acceptsFrom S ↔ ∃ s ∈ S, s ∈ M.accept

Tactic:
simp only [mem_acceptsFrom, evalFrom_nil]

Premises used: NFA.mem_acceptsFrom, NFA.evalFrom_nil
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
mp : (∃ s ∈ M.accept, s ∈ S) → ∃ s ∈ S, s ∈ M.accept
mpr : (∃ s ∈ S, s ∈ M.accept) → ∃ s ∈ M.accept, s ∈ S
mp₁ mp₂ mp₃ : ∀ w ∈ M.accept, w ∈ S → ∃ s ∈ S, s ∈ M.accept
mpr₁ mpr₂ mpr₃ : ∀ w ∈ S, w ∈ M.accept → ∃ s ∈ M.accept, s ∈ S
mp₄ mp₅ mp₆ : ∀ w ∈ M.accept, w ∈ S → ∃ s ∈ S, s ∈ M.accept
mpr₄ mpr₅ mpr₆ : ∀ w ∈ S, w ∈ M.accept → ∃ s ∈ M.accept, s ∈ S
mp₇ mp₈ : ∀ w ∈ M.accept, w ∈ S → ∃ s ∈ S, s ∈ M.accept
mpr₇ mpr₈ : ∀ w ∈ S, w ∈ M.accept → ∃ s ∈ M.accept, s ∈ S
⊢ (∃ s ∈ M.accept, s ∈ S) ↔ ∃ s ∈ S, s ∈ M.accept

Tactic:
tauto
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
a : α
x : List α
⊢ a :: x ∈ M.acceptsFrom S ↔ x ∈ M.acceptsFrom (M.stepSet S a)

Tactic:
simp [mem_acceptsFrom]

Premises used: NFA.mem_acceptsFrom
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
a : α
h :
  ∀ (x : List α),
    Membership.mem (γ := Set (List α)) ((fun (x : List α) ↦ a :: x) ⁻¹' M.acceptsFrom S) x ↔
      x ∈ M.acceptsFrom (M.stepSet S a)
⊢ (fun (x : List α) ↦ a :: x) ⁻¹' M.acceptsFrom S = M.acceptsFrom (M.stepSet S a)

Tactic:
ext x
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
a : α
x : List α
⊢ Membership.mem (γ := Set (List α)) ((fun (x : List α) ↦ a :: x) ⁻¹' M.acceptsFrom S) x ↔
    x ∈ M.acceptsFrom (M.stepSet S a)

Tactic:
simp [cons_mem_acceptsFrom M]

Premises used: NFA.cons_mem_acceptsFrom
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
x y : List α
⊢ x ++ y ∈ M.acceptsFrom S ↔ y ∈ M.acceptsFrom (M.evalFrom S x)

Tactic:
simp [mem_acceptsFrom]

Premises used: NFA.mem_acceptsFrom
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
x : List α
h :
  ∀ (y : List α),
    Membership.mem (γ := Set (List α)) ((fun (x_1 : List α) ↦ x ++ x_1) ⁻¹' M.acceptsFrom S) y ↔
      y ∈ M.acceptsFrom (M.evalFrom S x)
⊢ (fun (x_1 : List α) ↦ x ++ x_1) ⁻¹' M.acceptsFrom S = M.acceptsFrom (M.evalFrom S x)

Tactic:
ext y
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
x y : List α
⊢ Membership.mem (γ := Set (List α)) ((fun (x_1 : List α) ↦ x ++ x_1) ⁻¹' M.acceptsFrom S) y ↔
    y ∈ M.acceptsFrom (M.evalFrom S x)

Tactic:
simp [append_mem_acceptsFrom M]

Premises used: NFA.append_mem_acceptsFrom
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
h : ∀ (x : List α), x ∈ M.acceptsFrom (S ∪ T) ↔ x ∈ M.acceptsFrom S ∪ M.acceptsFrom T
⊢ M.acceptsFrom (S ∪ T) = M.acceptsFrom S ∪ M.acceptsFrom T

Tactic:
ext x
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
h : (∃ s ∈ M.accept, s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x) ↔ x ∈ M.acceptsFrom S ∪ M.acceptsFrom T
⊢ x ∈ M.acceptsFrom (S ∪ T) ↔ x ∈ M.acceptsFrom S ∪ M.acceptsFrom T

Tactic:
simp only [mem_acceptsFrom, evalFrom_union, mem_union]

Premises used: Set.mem_union, NFA.mem_acceptsFrom, NFA.evalFrom_union
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
h : (∃ s ∈ M.accept, s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x) → x ∈ M.acceptsFrom S ∪ M.acceptsFrom T
h₁ : x ∈ M.acceptsFrom S ∪ M.acceptsFrom T → ∃ s ∈ M.accept, s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x
⊢ (∃ s ∈ M.accept, s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x) ↔ x ∈ M.acceptsFrom S ∪ M.acceptsFrom T

Tactic:
constructor
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom S x
h₁ : x ∈ M.acceptsFrom S
⊢ x ∈ M.acceptsFrom S ∪ M.acceptsFrom T

Tactic:
left
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom S x
⊢ x ∈ M.acceptsFrom S

Tactic:
tauto
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom T x
h₁ : x ∈ M.acceptsFrom T
⊢ x ∈ M.acceptsFrom S ∪ M.acceptsFrom T

Tactic:
right
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom T x
⊢ x ∈ M.acceptsFrom T

Tactic:
tauto
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom S x
h₁ : s ∈ M.accept ∧ (s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x)
⊢ ∃ s ∈ M.accept, s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x

Tactic:
exists s
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom T x
h₁ : s ∈ M.accept ∧ (s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x)
⊢ ∃ s ∈ M.accept, s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x

Tactic:
exists s
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom S x
h₁ : s ∈ M.accept
h₂ h₃ h₄ : s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x
h₅ h₆ : s ∉ M.evalFrom S x → s ∈ M.evalFrom T x
⊢ s ∈ M.accept ∧ (s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x)

Tactic:
tauto
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom T x
h₁ : s ∈ M.accept
h₂ h₃ h₄ : s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x
h₅ : s ∉ M.evalFrom S x → s ∈ M.evalFrom T x
⊢ s ∈ M.accept ∧ (s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x)

Tactic:
tauto
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
ι : Sort u_1
s : ι → Set σ
h :
  ∀ (x : List α),
    x ∈ M.acceptsFrom (⋃ (i : ι), s i) ↔ Membership.mem (γ := Language α) (⋃ (i : ι), M.acceptsFrom (s i)) x
⊢ M.acceptsFrom (⋃ (i : ι), s i) = ⋃ (i : ι), M.acceptsFrom (s i)

Tactic:
ext x
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
ι : Sort u_1
s : ι → Set σ
x : List α
h :
  Membership.mem (γ := Language α) {x : List α | ∃ s_1 ∈ M.accept, ∃ (i : ι), s_1 ∈ M.evalFrom (s i) x} x ↔
    Membership.mem (γ := Language α) (⋃ (i : ι), {x : List α | ∃ s_1 ∈ M.accept, s_1 ∈ M.evalFrom (s i) x}) x
⊢ x ∈ M.acceptsFrom (⋃ (i : ι), s i) ↔ Membership.mem (γ := Language α) (⋃ (i : ι), M.acceptsFrom (s i)) x

Tactic:
simp only [acceptsFrom, evalFrom_iUnion, mem_iUnion]

Premises used: Set.mem_iUnion, NFA.evalFrom_iUnion, NFA.acceptsFrom
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
ι : Sort u_1
s : ι → Set σ
x : List α
h : (∃ s_1 ∈ M.accept, ∃ (i : ι), s_1 ∈ M.evalFrom (s i) x) ↔ ∃ (i : ι), ∃ s_1 ∈ M.accept, s_1 ∈ M.evalFrom (s i) x
⊢ Membership.mem (γ := Language α) {x : List α | ∃ s_1 ∈ M.accept, ∃ (i : ι), s_1 ∈ M.evalFrom (s i) x} x ↔
    Membership.mem (γ := Language α) (⋃ (i : ι), {x : List α | ∃ s_1 ∈ M.accept, s_1 ∈ M.evalFrom (s i) x}) x

Tactic:
simp_rw [↑mem_iUnion, ↑mem_setOf_eq]

Premises used: Set.mem_iUnion, Set.mem_setOf_eq
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
ι : Sort u_1
s : ι → Set σ
x : List α
h : (∃ s_1 ∈ M.accept, ∃ (i : ι), s_1 ∈ M.evalFrom (s i) x) → ∃ (i : ι), ∃ s_1 ∈ M.accept, s_1 ∈ M.evalFrom (s i) x
h₁ : (∃ (i : ι), ∃ s_1 ∈ M.accept, s_1 ∈ M.evalFrom (s i) x) → ∃ s_1 ∈ M.accept, ∃ (i : ι), s_1 ∈ M.evalFrom (s i) x
h₂ h₃ h₄ : ∀ w ∈ M.accept, ∀ (w_1 : ι), w ∈ M.evalFrom (s w_1) x → ∃ (i : ι), ∃ s_1 ∈ M.accept, s_1 ∈ M.evalFrom (s i) x
h₅ h₆ h₇ : ∀ (w : ι), ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom (s w) x → ∃ s_1 ∈ M.accept, ∃ (i : ι), s_1 ∈ M.evalFrom (s i) x
h₈ h₉ h₁₀ :
  ∀ w ∈ M.accept, ∀ (w_1 : ι), w ∈ M.evalFrom (s w_1) x → ∃ (i : ι), ∃ s_1 ∈ M.accept, s_1 ∈ M.evalFrom (s i) x
h₁₁ h₁₂ h₁₃ :
  ∀ (w : ι), ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom (s w) x → ∃ s_1 ∈ M.accept, ∃ (i : ι), s_1 ∈ M.evalFrom (s i) x
h₁₄ h₁₅ : ∀ w ∈ M.accept, ∀ (w_1 : ι), w ∈ M.evalFrom (s w_1) x → ∃ (i : ι), ∃ s_1 ∈ M.accept, s_1 ∈ M.evalFrom (s i) x
h₁₆ : ∀ w ∈ M.accept, ∀ (w_1 : ι), w ∈ M.evalFrom (s w_1) x → ∃ s_1 ∈ M.accept, s_1 ∈ M.evalFrom (s w_1) x
h₁₇ : (w : σ) → w ∈ M.accept → (w_1 : ι) → w ∈ M.evalFrom (s w_1) x → ι
h₁₈ : ∀ w ∈ M.accept, ∀ (w_1 : ι), w ∈ M.evalFrom (s w_1) x → ∃ s_1 ∈ M.accept, s_1 ∈ M.evalFrom (s w_1) x
h₁₉ : (w : σ) → w ∈ M.accept → (w_1 : ι) → w ∈ M.evalFrom (s w_1) x → ι
h₂₀ h₂₁ : ∀ (w : ι), ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom (s w) x → ∃ s_1 ∈ M.accept, ∃ (i : ι), s_1 ∈ M.evalFrom (s i) x
h₂₂ : ∀ (w : ι), ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom (s w) x → w_1 ∈ M.accept ∧ ∃ (i : ι), w_1 ∈ M.evalFrom (s i) x
h₂₃ : (w : ι) → (w_1 : σ) → w_1 ∈ M.accept → w_1 ∈ M.evalFrom (s w) x → σ
h₂₄ : ∀ (w : ι), ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom (s w) x → w_1 ∈ M.accept ∧ ∃ (i : ι), w_1 ∈ M.evalFrom (s i) x
h₂₅ : (w : ι) → (w_1 : σ) → w_1 ∈ M.accept → w_1 ∈ M.evalFrom (s w) x → σ
⊢ (∃ s_1 ∈ M.accept, ∃ (i : ι), s_1 ∈ M.evalFrom (s i) x) ↔ ∃ (i : ι), ∃ s_1 ∈ M.accept, s_1 ∈ M.evalFrom (s i) x

Tactic:
tauto
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
ι : Sort u_1
κ : ι → Sort u_2
f : (i : ι) → κ i → Set σ
⊢ M.acceptsFrom (⋃ (i : ι), ⋃ (j : κ i), f i j) = ⋃ (i : ι), ⋃ (j : κ i), M.acceptsFrom (f i j)

Tactic:
simp
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
p : Prop
S : Set σ
nil : (∃ (s : σ), (s ∈ S ∧ p) ∧ s ∈ M.accept) ↔ (∃ s ∈ S, s ∈ M.accept) ∧ p
⊢ [] ∈ M.acceptsFrom {s : σ | s ∈ S ∧ p} ↔ [] ∈ M.acceptsFrom S ∧ p

Tactic:
simp only [nil_mem_acceptsFrom, mem_setOf_eq]

Premises used: Set.mem_setOf_eq, NFA.nil_mem_acceptsFrom
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
p : Prop
S : Set σ
nil : (∃ (s : σ), (s ∈ S ∧ p) ∧ s ∈ M.accept) → (∃ s ∈ S, s ∈ M.accept) ∧ p
nil₁ : (∃ s ∈ S, s ∈ M.accept) ∧ p → ∃ (s : σ), (s ∈ S ∧ p) ∧ s ∈ M.accept
nil₂ nil₃ : ∀ w ∈ M.accept, w ∈ S → p → (∃ s ∈ S, s ∈ M.accept) ∧ p
nil₄ : ∀ w ∈ M.accept, w ∈ S → p → ∃ s ∈ S, s ∈ M.accept
nil₅ : ∀ w ∈ M.accept, w ∈ S → p → p
nil₆ nil₇ nil₈ : p → ∀ w ∈ S, w ∈ M.accept → ∃ (s : σ), (s ∈ S ∧ p) ∧ s ∈ M.accept
nil₉ nil₁₀ nil₁₁ : ∀ w ∈ M.accept, w ∈ S → p → ∃ s ∈ S, s ∈ M.accept
nil₁₂ nil₁₃ nil₁₄ : p → ∀ w ∈ S, w ∈ M.accept → ∃ (s : σ), (s ∈ S ∧ p) ∧ s ∈ M.accept
nil₁₅ nil₁₆ : ∀ w ∈ M.accept, w ∈ S → p → ∃ s ∈ S, s ∈ M.accept
nil₁₇ nil₁₈ : p → ∀ w ∈ S, w ∈ M.accept → ∃ (s : σ), (s ∈ S ∧ p) ∧ s ∈ M.accept
nil₁₉ : p → ∀ w ∈ S, w ∈ M.accept → (w ∈ S ∧ p) ∧ w ∈ M.accept
nil₂₀ : p → (w : σ) → w ∈ S → w ∈ M.accept → σ
nil₂₁ : p → ∀ w ∈ S, w ∈ M.accept → (w ∈ S ∧ p) ∧ w ∈ M.accept
nil₂₂ : p → (w : σ) → w ∈ S → w ∈ M.accept → σ
⊢ (∃ (s : σ), (s ∈ S ∧ p) ∧ s ∈ M.accept) ↔ (∃ s ∈ S, s ∈ M.accept) ∧ p

Tactic:
tauto
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
p : Prop
a : α
x : List α
ih : ∀ {S : Set σ}, x ∈ M.acceptsFrom {s : σ | s ∈ S ∧ p} ↔ x ∈ M.acceptsFrom S ∧ p
S : Set σ
h : ∀ (s : σ), s ∈ M.stepSet {s : σ | s ∈ S ∧ p} a ↔ Membership.mem (γ := Set σ) {s : σ | s ∈ M.stepSet S a ∧ p} s
⊢ M.stepSet {s : σ | s ∈ S ∧ p} a = {s : σ | s ∈ M.stepSet S a ∧ p}

Tactic:
ext s
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
p : Prop
a : α
x : List α
ih : ∀ {S : Set σ}, x ∈ M.acceptsFrom {s : σ | s ∈ S ∧ p} ↔ x ∈ M.acceptsFrom S ∧ p
S : Set σ
s : σ
h : (∃ (i : σ), (i ∈ S ∧ p) ∧ s ∈ M.step i a) ↔ (∃ i ∈ S, s ∈ M.step i a) ∧ p
⊢ s ∈ M.stepSet {s : σ | s ∈ S ∧ p} a ↔ Membership.mem (γ := Set σ) {s : σ | s ∈ M.stepSet S a ∧ p} s

Tactic:
simp only [stepSet, mem_setOf_eq, mem_iUnion, exists_prop]

Premises used: Set.mem_iUnion, Set.mem_setOf_eq, exists_prop, NFA.stepSet
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
p : Prop
a : α
x : List α
ih : ∀ {S : Set σ}, x ∈ M.acceptsFrom {s : σ | s ∈ S ∧ p} ↔ x ∈ M.acceptsFrom S ∧ p
S : Set σ
s : σ
h : (∃ (i : σ), (i ∈ S ∧ p) ∧ s ∈ M.step i a) → (∃ i ∈ S, s ∈ M.step i a) ∧ p
h₁ : (∃ i ∈ S, s ∈ M.step i a) ∧ p → ∃ (i : σ), (i ∈ S ∧ p) ∧ s ∈ M.step i a
h₂ h₃ : ∀ (w : σ), s ∈ M.step w a → w ∈ S → p → (∃ i ∈ S, s ∈ M.step i a) ∧ p
h₄ : ∀ (w : σ), s ∈ M.step w a → w ∈ S → p → ∃ i ∈ S, s ∈ M.step i a
h₅ : ∀ (w : σ), s ∈ M.step w a → w ∈ S → p → p
h₆ h₇ h₈ : p → ∀ w ∈ S, s ∈ M.step w a → ∃ (i : σ), (i ∈ S ∧ p) ∧ s ∈ M.step i a
h₉ h₁₀ h₁₁ : ∀ (w : σ), s ∈ M.step w a → w ∈ S → p → ∃ i ∈ S, s ∈ M.step i a
h₁₂ h₁₃ h₁₄ : p → ∀ w ∈ S, s ∈ M.step w a → ∃ (i : σ), (i ∈ S ∧ p) ∧ s ∈ M.step i a
h₁₅ h₁₆ : ∀ (w : σ), s ∈ M.step w a → w ∈ S → p → ∃ i ∈ S, s ∈ M.step i a
h₁₇ h₁₈ : p → ∀ w ∈ S, s ∈ M.step w a → ∃ (i : σ), (i ∈ S ∧ p) ∧ s ∈ M.step i a
h₁₉ : p → ∀ w ∈ S, s ∈ M.step w a → (w ∈ S ∧ p) ∧ s ∈ M.step w a
h₂₀ : p → (w : σ) → w ∈ S → s ∈ M.step w a → σ
h₂₁ : p → ∀ w ∈ S, s ∈ M.step w a → (w ∈ S ∧ p) ∧ s ∈ M.step w a
h₂₂ : p → (w : σ) → w ∈ S → s ∈ M.step w a → σ
⊢ (∃ (i : σ), (i ∈ S ∧ p) ∧ s ∈ M.step i a) ↔ (∃ i ∈ S, s ∈ M.step i a) ∧ p

Tactic:
tauto
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
p : Prop
a : α
x : List α
ih : ∀ {S : Set σ}, x ∈ M.acceptsFrom {s : σ | s ∈ S ∧ p} ↔ x ∈ M.acceptsFrom S ∧ p
S : Set σ
⊢ M.stepSet {s : σ | s ∈ S ∧ p} a = {s : σ | s ∈ M.stepSet S a ∧ p}

Tactic:
have h : M.stepSet {s ∈ S | p} a = {s ∈ M.stepSet S a | p} := by
      ext s; simp only [stepSet, mem_setOf_eq, mem_iUnion, exists_prop]; tauto
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
p : Prop
a : α
x : List α
ih : ∀ {S : Set σ}, x ∈ M.acceptsFrom {s : σ | s ∈ S ∧ p} ↔ x ∈ M.acceptsFrom S ∧ p
S : Set σ
h : M.stepSet {s : σ | s ∈ S ∧ p} a = {s : σ | s ∈ M.stepSet S a ∧ p}
⊢ a :: x ∈ M.acceptsFrom {s : σ | s ∈ S ∧ p} ↔ a :: x ∈ M.acceptsFrom S ∧ p

Tactic:
simp [h, ih]
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
p : Prop
x : List α
nil : ∀ {S : Set σ}, [] ∈ M.acceptsFrom {s : σ | s ∈ S ∧ p} ↔ [] ∈ M.acceptsFrom S ∧ p
cons :
  ∀ (a : α) (x : List α) (ih : ∀ {S : Set σ}, x ∈ M.acceptsFrom {s : σ | s ∈ S ∧ p} ↔ x ∈ M.acceptsFrom S ∧ p)
    {S : Set σ}, a :: x ∈ M.acceptsFrom {s : σ | s ∈ S ∧ p} ↔ a :: x ∈ M.acceptsFrom S ∧ p
⊢ x ∈ M.acceptsFrom {s : σ | s ∈ S ∧ p} ↔ x ∈ M.acceptsFrom S ∧ p

Tactic:
induction x generalizing S with
  | nil => simp only [nil_mem_acceptsFrom, mem_setOf_eq]; tauto
  | cons a x ih =>
    have h : M.stepSet {s ∈ S | p} a = {s ∈ M.stepSet S a | p} := by
      ext s; simp only [stepSet, mem_setOf_eq, mem_iUnion, exists_prop]; tauto
    simp [h, ih]

Premises used: Set.mem_setOf_eq, NFA.nil_mem_acceptsFrom
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
⊢ M.eval [] = M.start

Tactic:
rfl

Premises used: NFA.evalFrom, List.foldl, rfl, NFA.eval
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
a : α
⊢ M.eval [a] = M.stepSet M.start a

Tactic:
rfl

Premises used: iSup, NFA.evalFrom, List.foldl, NFA.stepSet, Set.iUnion, rfl, NFA.eval
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
x : List α
a : α
⊢ M.eval (x ++ [a]) = M.stepSet (M.eval x) a

Tactic:
simp [eval]

Premises used: NFA.eval
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
x : List α
⊢ x ∈ M.accepts ↔ ∃ S ∈ M.accept, S ∈ M.evalFrom M.start x

Tactic:
rfl
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
⊢ M.accepts = M.acceptsFrom M.start

Tactic:
rfl

Premises used: Set.Mem, setOf, NFA.accepts, NFA.acceptsFrom, rfl, NFA.eval
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
s t : σ
x : List α
h : t ∈ M.evalFrom {s} []
⊢ t = s

Tactic:
simp at h
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
s t : σ
x : List α
h : t = s
⊢ s = t

Tactic:
tauto
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
s t : σ
x_1 : List α
a : α
x : List α
h : t ∈ M.evalFrom {s} (a :: x)
⊢ ∃ t_1 ∈ M.step s a, t ∈ M.evalFrom {t_1} x

Tactic:
rw [evalFrom_cons, mem_evalFrom_iff_exists, stepSet_singleton] at h

Premises used: NFA.evalFrom_cons, NFA.mem_evalFrom_iff_exists, NFA.stepSet_singleton
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
s t : σ
x_1 : List α
a : α
x : List α
h : ∃ t_1 ∈ M.step s a, t ∈ M.evalFrom {t_1} x
⊢ ∃ s' ∈ M.step s a, t ∈ M.evalFrom {s'} x

Tactic:
h
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
s t : σ
x_1 : List α
a : α
x : List α
h : ∃ t_1 ∈ M.step s a, t ∈ M.evalFrom {t_1} x
⊢ ∃ s' ∈ M.step s a, t ∈ M.evalFrom {s'} x

Tactic:
exact h
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
s_1 t : σ
x : List α
p : Nonempty (M.Path s_1 t x)
s : σ
⊢ s ∈ M.evalFrom {s} []

Tactic:
simp
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
s_1 t_1 : σ
x_1 : List α
p : Nonempty (M.Path s_1 t_1 x_1)
t s s' : σ
a : α
x : List α
h₁ : s' ∈ M.step s a
h₂ : M.Path s' t x
rw : ∃ t_2 ∈ M.step s a, t ∈ M.evalFrom {t_2} x
⊢ t ∈ M.evalFrom {s} (a :: x)

Tactic:
rw [evalFrom_cons, stepSet_singleton, mem_evalFrom_iff_exists]

Premises used: NFA.evalFrom_cons, NFA.mem_evalFrom_iff_exists, NFA.stepSet_singleton
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
s_1 t_1 : σ
x_1 : List α
p : Nonempty (M.Path s_1 t_1 x_1)
t s s' : σ
a : α
x : List α
h₁ : s' ∈ M.step s a
h₂ : M.Path s' t x
⊢ ∃ t_2 ∈ M.step s a, t ∈ M.evalFrom {t_2} x

Tactic:
⟨s', h₁, mem_evalFrom_iff_nonempty_path.2 ⟨h₂⟩⟩

Premises used: Iff.mpr, Nonempty.intro, And.intro, Exists.intro
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
s_1 t_1 : σ
x_1 : List α
p : Nonempty (M.Path s_1 t_1 x_1)
t s s' : σ
a : α
x : List α
h₁ : s' ∈ M.step s a
h₂ : M.Path s' t x
⊢ ∃ t_2 ∈ M.step s a, t ∈ M.evalFrom {t_2} x

Tactic:
exact ⟨s', h₁, mem_evalFrom_iff_nonempty_path.2 ⟨h₂⟩⟩