awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.Encoding
Goal:
α : Type u
e : Encoding.{u, v} α
⊢ lift.{v, u} #α ≤ lift.{u, v} #(List e.Γ)

Tactic:
Cardinal.lift_mk_le'.2 ⟨⟨e.encode, e.encode_injective⟩⟩

Premises used: Iff.mpr, Computability.Encoding.encode, Function.Embedding.mk, Nonempty.intro, Computability.Encoding.encode_injective, Cardinal.lift_mk_le'
-- Module: Mathlib.Computability.Encoding
Goal:
α : Type u
e : Encoding.{u, v} α
inst : Countable.{v + 1} e.Γ
⊢ #α ≤ ℵ₀

Tactic:
haveI : Countable α := e.encode_injective.countable
  Cardinal.mk_le_aleph0

Premises used: Cardinal.mk_le_aleph0
-- Module: Mathlib.Computability.Encoding
Goal:
α : Type u
e : FinEncoding α
⊢ #α ≤ ℵ₀

Tactic:
e.toEncoding.card_le_aleph0

Premises used: Computability.Encoding.card_le_aleph0, Computability.FinEncoding.toEncoding
-- Module: Mathlib.Computability.Encoding
Goal:
α : Type u_1
β : Type u_2
ea : FinEncoding α
eb : FinEncoding β
x : α × β
⊢ Option.map₂ Prod.mk
      (ea.decode (List.filterMap Sum.getLeft? (List.map Sum.inl (ea.encode x.1) ++ List.map Sum.inr (eb.encode x.2))))
      (eb.decode
        (List.filterMap Sum.getRight? (List.map Sum.inl (ea.encode x.1) ++ List.map Sum.inr (eb.encode x.2)))) =
    some x

Tactic:
simp
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
⊢ S ⊆ M.εClosure S

Tactic:
εClosure.base

Premises used: εNFA.εClosure.base, Set.Mem, Set.Subset
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s : σ
hs : s ∈ M.εClosure ∅
base : ∀ (s : σ), Membership.mem (γ := Set σ) ∅ s → False
step : ∀ (s t : σ), t ∈ M.step s none → M.εClosure ∅ s → False → False
⊢ False

Tactic:
induction hs
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s s_1 : σ
h : Membership.mem (γ := Set σ) ∅ s_1
⊢ False

Tactic:
assumption
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s s_1 t : σ
h : t ∈ M.step s_1 none
h_1 : M.εClosure ∅ s_1
a_ih : False
⊢ False

Tactic:
assumption
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
⊢ M.εClosure univ = univ

Tactic:
eq_univ_of_univ_subset <| subset_εClosure _ _

Premises used: εNFA.subset_εClosure, Set.eq_univ_of_univ_subset
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s s_1 : σ
h : s_1 ∈ S
base : s_1 ∈ S ∧ s_1 ∈ M.εClosure {s_1}
base₁ : σ
base₂ : s_1 ∈ S ∧ s_1 ∈ M.εClosure {s_1}
base₃ : σ
⊢ ∃ t ∈ S, s_1 ∈ M.εClosure {t}

Tactic:
tauto
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s s_1 t : σ
h : t ∈ M.step s_1 none
h_1 : M.εClosure S s_1
ih : ∃ t ∈ S, s_1 ∈ M.εClosure {t}
step : ∀ s ∈ S, s_1 ∈ M.εClosure {s} → ∃ t_1 ∈ S, t ∈ M.εClosure {t_1}
⊢ ∃ t_1 ∈ S, t ∈ M.εClosure {t_1}

Tactic:
obtain ⟨s, _, _⟩ := ih
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s_1 s_2 t : σ
h_1 : t ∈ M.step s_2 none
h_2 : M.εClosure S s_2
s : σ
left : s ∈ S
right : s_2 ∈ M.εClosure {s}
h : s ∈ S ∧ t ∈ M.εClosure {s}
⊢ ∃ t_1 ∈ S, t ∈ M.εClosure {t_1}

Tactic:
use s
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s_1 s_2 t : σ
h : t ∈ M.step s_2 none
h_1 : M.εClosure S s_2
s : σ
left : s ∈ S
right : s_2 ∈ M.εClosure {s}
⊢ s ∈ S ∧ t ∈ M.εClosure {s}

Tactic:
solve_by_elim [εClosure.step]

Premises used: εNFA.εClosure.step
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s : σ
h : s ∈ M.εClosure S
base : ∀ s ∈ S, ∃ t ∈ S, s ∈ M.εClosure {t}
step :
  ∀ (s t : σ),
    t ∈ M.step s none → M.εClosure S s → ∀ (ih : ∃ t ∈ S, s ∈ M.εClosure {t}), ∃ t_1 ∈ S, t ∈ M.εClosure {t_1}
⊢ ∃ t ∈ S, s ∈ M.εClosure {t}

Tactic:
induction h with
    | base => tauto
    | step _ _ _ _ ih =>
      obtain ⟨s, _, _⟩ := ih
      use s
      solve_by_elim [εClosure.step]

Premises used: εNFA.εClosure.step, εNFA.step
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s t : σ
left : t ∈ S
h : s ∈ M.εClosure {t}
base : ∀ (s : σ), Membership.mem (γ := Set σ) {t} s → s ∈ M.εClosure S
step : ∀ (s t_1 : σ), t_1 ∈ M.step s none → M.εClosure {t} s → s ∈ M.εClosure S → t_1 ∈ M.εClosure S
⊢ s ∈ M.εClosure S

Tactic:
induction h
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s t : σ
left : t ∈ S
s_1 : σ
h : Membership.mem (γ := Set σ) {t} s_1
⊢ s_1 ∈ S

Tactic:
subst_vars
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s s_1 : σ
left : s_1 ∈ S
⊢ s_1 ∈ M.εClosure S

Tactic:
solve_by_elim [εClosure.step]

Premises used: εNFA.εClosure.step
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s t : σ
left : t ∈ S
s_1 t_1 : σ
h : t_1 ∈ M.step s_1 none
h_1 : M.εClosure {t} s_1
a_ih : s_1 ∈ M.εClosure S
⊢ t_1 ∈ M.εClosure S

Tactic:
solve_by_elim [εClosure.step]

Premises used: εNFA.εClosure.step
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s : σ
a : α
simp_rw :
  Membership.mem (γ := Set σ) (⋃ s ∈ S, M.εClosure (M.step s (some a))) s ↔ ∃ t ∈ S, s ∈ M.εClosure (M.step t (some a))
simp_rw₁ : (∃ (i : σ) (_ : i ∈ S), s ∈ M.εClosure (M.step i (some a))) ↔ ∃ t ∈ S, s ∈ M.εClosure (M.step t (some a))
⊢ s ∈ M.stepSet S a ↔ ∃ t ∈ S, s ∈ M.εClosure (M.step t (some a))

Tactic:
simp_rw [stepSet, mem_iUnion₂, exists_prop]

Premises used: εNFA.stepSet, exists_prop, Set.mem_iUnion₂
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
a : α
simp_rw : Eq.{v + 1} (α := Set σ) (⋃ (s : σ), ⋃ (_ : Membership.mem (γ := Set σ) ∅ s), M.εClosure (M.step s (some a))) ∅
simp_rw₁ : Eq.{v + 1} (α := Set σ) (⋃ (s : σ), ⋃ (_ : False), M.εClosure (M.step s (some a))) ∅
simp_rw₂ : Eq.{v + 1} (α := Set σ) (⋃ (s : σ), ∅) ∅
⊢ M.stepSet ∅ a = ∅

Tactic:
simp_rw [stepSet, mem_empty_iff_false, iUnion_false, iUnion_empty]

Premises used: εNFA.stepSet, Set.iUnion_false, Set.mem_empty_iff_false, Set.iUnion_empty
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
⊢ M.evalFrom S [] = M.εClosure S

Tactic:
rfl

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

Tactic:
rfl

Premises used: iSup, εNFA.stepSet, List.foldl, εNFA.evalFrom, Set.iUnion, rfl
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
x : List α
a : α
rw : List.foldl M.stepSet (M.εClosure S) (x ++ [a]) = M.stepSet (List.foldl M.stepSet (M.εClosure S) x) a
rw₁ :
  List.foldl M.stepSet (List.foldl M.stepSet (M.εClosure S) x) [a] = M.stepSet (List.foldl M.stepSet (M.εClosure S) x) a
rw₂ :
  List.foldl M.stepSet (M.stepSet (List.foldl M.stepSet (M.εClosure S) x) a) [] =
    M.stepSet (List.foldl M.stepSet (M.εClosure S) x) a
rw₃ rw₄ : M.stepSet (List.foldl M.stepSet (M.εClosure S) x) a = M.stepSet (List.foldl M.stepSet (M.εClosure S) x) a
⊢ M.evalFrom S (x ++ [a]) = M.stepSet (M.evalFrom S x) a

Tactic:
rw [evalFrom, List.foldl_append, List.foldl_cons, List.foldl_nil]

Premises used: List.foldl_nil, List.foldl_append, εNFA.evalFrom, List.foldl_cons
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
nil : M.εClosure ∅ = ∅
nil₁ nil₂ : Eq.{v + 1} (α := Set σ) ∅ ∅
⊢ M.evalFrom ∅ [] = ∅

Tactic:
rw [evalFrom_nil, εClosure_empty]

Premises used: εNFA.εClosure_empty, εNFA.evalFrom_nil
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
x : List α
a : α
ih : M.evalFrom ∅ x = ∅
append_singleton : M.stepSet (M.evalFrom ∅ x) a = ∅
append_singleton₁ : M.stepSet ∅ a = ∅
append_singleton₂ append_singleton₃ : Eq.{v + 1} (α := Set σ) ∅ ∅
⊢ M.evalFrom ∅ (x ++ [a]) = ∅

Tactic:
rw [evalFrom_append_singleton, ih, stepSet_empty]

Premises used: εNFA.evalFrom_append_singleton, εNFA.stepSet_empty
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
x : List α
nil : M.evalFrom ∅ [] = ∅
append_singleton : ∀ (x : List α) (a : α) (ih : M.evalFrom ∅ x = ∅), M.evalFrom ∅ (x ++ [a]) = ∅
⊢ M.evalFrom ∅ x = ∅

Tactic:
induction x using List.reverseRecOn with
  | nil => rw [evalFrom_nil, εClosure_empty]
  | append_singleton x a ih => rw [evalFrom_append_singleton, ih, stepSet_empty]

Premises used: εNFA.evalFrom_append_singleton, εNFA.stepSet_empty, εNFA.εClosure_empty, εNFA.evalFrom_nil
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s : σ
⊢ s ∈ M.evalFrom S [] ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} []

Tactic:
apply mem_εClosure_iff_exists

Premises used: εNFA.mem_εClosure_iff_exists
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
l : List α
a : α
ih : ∀ {s : σ}, s ∈ M.evalFrom S l ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} l
s : σ
append_singleton :
  (∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))) ↔
    ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
⊢ s ∈ M.evalFrom S (l ++ [a]) ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} (l ++ [a])

Tactic:
simp_rw [evalFrom_append_singleton, mem_stepSet_iff, ih]

Premises used: εNFA.evalFrom_append_singleton, εNFA.mem_stepSet_iff
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s : σ
S : Set σ
x : List α
nil : ∀ {s : σ}, s ∈ M.evalFrom S [] ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} []
append_singleton :
  ∀ (l : List α) (a : α) (ih : ∀ {s : σ}, s ∈ M.evalFrom S l ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} l) {s : σ},
    s ∈ M.evalFrom S (l ++ [a]) ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} (l ++ [a])
⊢ s ∈ M.evalFrom S x ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} x

Tactic:
induction x using List.reverseRecOn generalizing s with
  | nil => apply mem_εClosure_iff_exists
  | append_singleton _ _ ih =>
    simp_rw [evalFrom_append_singleton, mem_stepSet_iff, ih]
    tauto

Premises used: εNFA.evalFrom_append_singleton, εNFA.mem_εClosure_iff_exists, εNFA.mem_stepSet_iff
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
⊢ M.eval [] = M.εClosure M.start

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
evalFrom_append_singleton _ _ _ _

Premises used: εNFA.evalFrom_append_singleton, εNFA.eval
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s t : σ
rw :
  (t = s ∧ Eq.{u + 1} (α := List (Option α)) [] [] ∨
      ∃ (t_1 : σ) (a : Option α) (x : List (Option α)), t_1 ∈ M.step s a ∧ M.IsPath t_1 t x ∧ [] = a :: x) ↔
    s = t
⊢ M.IsPath s t [] ↔ s = t

Tactic:
rw [isPath_iff]

Premises used: εNFA.isPath_iff
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s t : σ
⊢ (t = s ∧ Eq.{u + 1} (α := List (Option α)) [] [] ∨
      ∃ (t_1 : σ) (a : Option α) (x : List (Option α)), t_1 ∈ M.step s a ∧ M.IsPath t_1 t x ∧ [] = a :: x) ↔
    s = t

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s t : σ
a : Option α
h : t ∈ M.step s a
⊢ t ∈ M.step s a

Tactic:
assumption
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s t : σ
a : Option α
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ : t ∈ M.step s a → M.IsPath s t [a]
⊢ t ∈ M.step s a → M.IsPath s t [a]

Tactic:
tauto
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
s : σ
nil : M.IsPath s u y → ∃ (t : σ), M.IsPath s t [] ∧ M.IsPath t u y
⊢ M.IsPath s u ([] ++ y) → ∃ (t : σ), M.IsPath s t [] ∧ M.IsPath t u y

Tactic:
rw [List.nil_append]

Premises used: List.nil_append
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
s : σ
nil nil₁ nil₂ nil₃ nil₄ nil₅ nil₆ nil₇ : M.IsPath s u y → ∃ (t : σ), M.IsPath s t [] ∧ M.IsPath t u y
⊢ M.IsPath s u y → ∃ (t : σ), M.IsPath s t [] ∧ M.IsPath t u y

Tactic:
tauto
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
x : Option α
a : List (Option α)
ih : ∀ {s : σ}, M.IsPath s u (a ++ y) → ∃ (t : σ), M.IsPath s t a ∧ M.IsPath t u y
s t : σ
h_1 : t ∈ M.step s x
h : M.IsPath t u (a.append y)
⊢ ∃ (t_1 : σ), M.IsPath t t_1 a ∧ M.IsPath t_1 u y

Tactic:
apply ih at h
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
x : Option α
a : List (Option α)
ih : ∀ {s : σ}, M.IsPath s u (a ++ y) → ∃ (t : σ), M.IsPath s t a ∧ M.IsPath t u y
s t : σ
h_1 : t ∈ M.step s x
h : ∃ (t_1 : σ), M.IsPath t t_1 a ∧ M.IsPath t_1 u y
cons cons₁ cons₂ cons₃ cons₄ cons₅ cons₆ cons₇ :
  ∀ (w : σ), M.IsPath t w a → M.IsPath w u y → ∃ (t : σ), M.IsPath s t (x :: a) ∧ M.IsPath t u y
cons₈ : ∀ (w : σ), M.IsPath t w a → M.IsPath w u y → M.IsPath s w (x :: a) ∧ M.IsPath w u y
cons₉ : (w : σ) → M.IsPath t w a → M.IsPath w u y → σ
cons₁₀ : ∀ (w : σ), M.IsPath t w a → M.IsPath w u y → M.IsPath s w (x :: a) ∧ M.IsPath w u y
cons₁₁ : (w : σ) → M.IsPath t w a → M.IsPath w u y → σ
cons₁₂ : ∀ (w : σ), M.IsPath t w a → M.IsPath w u y → M.IsPath s w (x :: a)
cons₁₃ : ∀ (w : σ), M.IsPath t w a → M.IsPath w u y → M.IsPath w u y
cons₁₄ : (w : σ) → M.IsPath t w a → M.IsPath w u y → σ
cons₁₅ : ∀ (w : σ), M.IsPath t w a → M.IsPath w u y → M.IsPath s w (x :: a)
cons₁₆ : ∀ (w : σ), M.IsPath t w a → M.IsPath w u y → M.IsPath w u y
cons₁₇ : (w : σ) → M.IsPath t w a → M.IsPath w u y → σ
cons₁₈ cons₁₉ : ∀ (w : σ), M.IsPath t w a → M.IsPath w u y → M.IsPath w u y
⊢ ∃ (t : σ), M.IsPath s t (x :: a) ∧ M.IsPath t u y

Tactic:
tauto
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s u : σ
x y : List (Option α)
nil : ∀ {s : σ}, M.IsPath s u ([] ++ y) → ∃ (t : σ), M.IsPath s t [] ∧ M.IsPath t u y
cons :
  ∀ (x : Option α) (a : List (Option α))
    (ih : ∀ {s : σ}, M.IsPath s u (a ++ y) → ∃ (t : σ), M.IsPath s t a ∧ M.IsPath t u y) {s : σ},
    M.IsPath s u (x :: a ++ y) → ∃ (t : σ), M.IsPath s t (x :: a) ∧ M.IsPath t u y
⊢ M.IsPath s u (x ++ y) → ∃ (t : σ), M.IsPath s t x ∧ M.IsPath t u y

Tactic:
induction x generalizing s with
    | nil =>
      rw [List.nil_append]
      tauto
    | cons x a ih =>
      rintro (_ | ⟨t, _, _, _, _, _, h⟩)
      apply ih at h
      tauto

Premises used: List.nil_append
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s u : σ
x y : List (Option α)
t : σ
hx : M.IsPath s t x
right : M.IsPath t u y
nil : ∀ {s : σ} (hx : M.IsPath s t []), M.IsPath s u ([] ++ y)
cons :
  ∀ (head : Option α) (tail : List (Option α)),
    (∀ {s : σ} (hx : M.IsPath s t tail), M.IsPath s u (tail ++ y)) →
      ∀ {s : σ} (hx : M.IsPath s t (head :: tail)), M.IsPath s u (head :: tail ++ y)
⊢ M.IsPath s u (x ++ y)

Tactic:
induction x generalizing s
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
t : σ
right : M.IsPath t u y
s : σ
hx : M.IsPath s t []
nil : M.IsPath t u ([] ++ y)
⊢ M.IsPath s u ([] ++ y)

Tactic:
cases hx
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
t : σ
right : M.IsPath t u y
head : Option α
tail : List (Option α)
tail_ih : ∀ {s : σ} (hx : M.IsPath s t tail), M.IsPath s u (tail ++ y)
s : σ
hx : M.IsPath s t (head :: tail)
cons : ∀ t_1 ∈ M.step s head, M.IsPath t_1 t tail → M.IsPath s u (head :: tail ++ y)
⊢ M.IsPath s u (head :: tail ++ y)

Tactic:
cases hx
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
t : σ
right : M.IsPath t u y
⊢ M.IsPath t u ([] ++ y)

Tactic:
tauto
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
u : σ
y : List (Option α)
t : σ
right : M.IsPath t u y
head : Option α
tail : List (Option α)
tail_ih : ∀ {s : σ} (hx : M.IsPath s t tail), M.IsPath s u (tail ++ y)
s t_1 : σ
h : t_1 ∈ M.step s head
h_1 : M.IsPath t_1 t tail
⊢ M.IsPath s u (head :: tail ++ y)

Tactic:
tauto
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ t : σ
h_1 : Membership.mem (γ := Set σ) {s₁} t
h : M.IsPath s₁ t (List.replicate 0 none)
⊢ ∃ (n : ℕ), M.IsPath s₁ t (List.replicate n none)

Tactic:
use 0
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ t : σ
h_1 : Membership.mem (γ := Set σ) {s₁} t
h : M.IsPath s₁ s₁ (List.replicate 0 none)
⊢ M.IsPath s₁ t (List.replicate 0 none)

Tactic:
subst t
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
⊢ M.IsPath s₁ s₁ (List.replicate 0 none)

Tactic:
apply IsPath.nil

Premises used: εNFA.IsPath.nil
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ s t : σ
h : t ∈ M.step s none
h_1 : M.εClosure {s₁} s
ih : ∃ (n : ℕ), M.IsPath s₁ s (List.replicate n none)
step : ∀ (n : ℕ), M.IsPath s₁ s (List.replicate n none) → ∃ (n : ℕ), M.IsPath s₁ t (List.replicate n none)
⊢ ∃ (n : ℕ), M.IsPath s₁ t (List.replicate n none)

Tactic:
obtain ⟨n, _⟩ := ih
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ s t : σ
h_1 : t ∈ M.step s none
h_2 : M.εClosure {s₁} s
n : ℕ
h_3 : M.IsPath s₁ s (List.replicate n none)
h : M.IsPath s₁ t (List.replicate (n + 1) none)
⊢ ∃ (n : ℕ), M.IsPath s₁ t (List.replicate n none)

Tactic:
use n + 1
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ s t : σ
h_1 : t ∈ M.step s none
h_2 : M.εClosure {s₁} s
n : ℕ
h_3 : M.IsPath s₁ s (List.replicate n none)
h : ∃ (t_1 : σ), M.IsPath s₁ t_1 (List.replicate n none) ∧ M.IsPath t_1 t (List.replicate 1 none)
⊢ M.IsPath s₁ t (List.replicate (n + 1) none)

Tactic:
rw [List.replicate_add, isPath_append]

Premises used: εNFA.isPath_append, List.replicate_add
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ s t : σ
h_1 : t ∈ M.step s none
h_2 : M.εClosure {s₁} s
n : ℕ
h_3 : M.IsPath s₁ s (List.replicate n none)
h : M.IsPath s₁ s (List.replicate n none) ∧ M.IsPath s t (List.replicate 1 none)
h₁ : σ
h₂ : M.IsPath s₁ s (List.replicate n none) ∧ M.IsPath s t (List.replicate 1 none)
h₃ : σ
h₄ : M.IsPath s₁ s (List.replicate n none)
h₅ : M.IsPath s t (List.replicate 1 none)
h₆ : σ
h₇ : M.IsPath s₁ s (List.replicate n none)
h₈ : M.IsPath s t (List.replicate 1 none)
h₉ : σ
h₁₀ h₁₁ : M.IsPath s t (List.replicate 1 none)
⊢ ∃ (t_1 : σ), M.IsPath s₁ t_1 (List.replicate n none) ∧ M.IsPath t_1 t (List.replicate 1 none)

Tactic:
tauto
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
h : s₂ ∈ M.εClosure {s₁}
base : ∀ (t : σ), Membership.mem (γ := Set σ) {s₁} t → ∃ (n : ℕ), M.IsPath s₁ t (List.replicate n none)
step :
  ∀ (s t : σ),
    t ∈ M.step s none →
      M.εClosure {s₁} s →
        ∀ (ih : ∃ (n : ℕ), M.IsPath s₁ s (List.replicate n none)), ∃ (n : ℕ), M.IsPath s₁ t (List.replicate n none)
⊢ ∃ (n : ℕ), M.IsPath s₁ s₂ (List.replicate n none)

Tactic:
induction h with
    | base t =>
      use 0
      subst t
      apply IsPath.nil
    | step _ _ _ _ ih =>
      obtain ⟨n, _⟩ := ih
      use n + 1
      rw [List.replicate_add, isPath_append]
      tauto

Premises used: εNFA.IsPath.nil, εNFA.isPath_append, εNFA.step, List.replicate_add
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
n : ℕ
h : M.IsPath s₁ s₂ (List.replicate n none)
zero : ∀ {s₂ : σ} (h : M.IsPath s₁ s₂ (List.replicate 0 none)), s₂ ∈ M.εClosure {s₁}
succ :
  ∀ (n : ℕ),
    (∀ {s₂ : σ} (h : M.IsPath s₁ s₂ (List.replicate n none)), s₂ ∈ M.εClosure {s₁}) →
      ∀ {s₂ : σ} (h : M.IsPath s₁ s₂ (List.replicate (n + 1) none)), s₂ ∈ M.εClosure {s₁}
⊢ s₂ ∈ M.εClosure {s₁}

Tactic:
induction n generalizing s₂
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
h : M.IsPath s₁ s₂ (List.replicate 0 none)
⊢ M.IsPath s₁ s₂ []

Tactic:
rw [List.replicate_zero] at h

Premises used: List.replicate_zero
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
h : M.IsPath s₁ s₂ []
⊢ s₁ = s₂

Tactic:
apply IsPath.eq_of_nil at h

Premises used: εNFA.IsPath.eq_of_nil
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
h : s₁ = s₂
⊢ s₂ ∈ M.εClosure {s₁}

Tactic:
solve_by_elim
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
n : ℕ
h_1 : ∀ {s₂ : σ} (h : M.IsPath s₁ s₂ (List.replicate n none)), s₂ ∈ M.εClosure {s₁}
s₂ : σ
h : M.IsPath s₁ s₂ (List.replicate (n + 1) none)
⊢ ∃ (t : σ), M.IsPath s₁ t (List.replicate n none) ∧ s₂ ∈ M.step t none

Tactic:
simp_rw [List.replicate_add, isPath_append, List.replicate_one, isPath_singleton] at h

Premises used: εNFA.isPath_singleton, εNFA.isPath_append, List.replicate_one, List.replicate_add
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
n : ℕ
h_1 : ∀ {s₂ : σ} (h : M.IsPath s₁ s₂ (List.replicate n none)), s₂ ∈ M.εClosure {s₁}
s₂ : σ
h : ∃ (t : σ), M.IsPath s₁ t (List.replicate n none) ∧ s₂ ∈ M.step t none
succ : ∀ (t : σ), M.IsPath s₁ t (List.replicate n none) → s₂ ∈ M.step t none → s₂ ∈ M.εClosure {s₁}
⊢ s₂ ∈ M.εClosure {s₁}

Tactic:
obtain ⟨t, _, _⟩ := h
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
n : ℕ
h : ∀ {s₂ : σ} (h : M.IsPath s₁ s₂ (List.replicate n none)), s₂ ∈ M.εClosure {s₁}
s₂ t : σ
left : M.IsPath s₁ t (List.replicate n none)
right : s₂ ∈ M.step t none
⊢ s₂ ∈ M.εClosure {s₁}

Tactic:
solve_by_elim [εClosure.step]

Premises used: εNFA.εClosure.step
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
nil :
  (∃ (n : ℕ), M.IsPath s₁ s₂ (List.replicate n none)) ↔
    ∃ (x' : List (Option α)), x'.reduceOption = [] ∧ M.IsPath s₁ s₂ x'
⊢ s₂ ∈ M.evalFrom {s₁} [] ↔ ∃ (x' : List (Option α)), x'.reduceOption = [] ∧ M.IsPath s₁ s₂ x'

Tactic:
rw [evalFrom_nil, mem_εClosure_iff_exists_path]

Premises used: εNFA.mem_εClosure_iff_exists_path, εNFA.evalFrom_nil
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
nil :
  (∃ (n : ℕ), M.IsPath s₁ s₂ (List.replicate n none)) →
    ∃ (x' : List (Option α)), x'.reduceOption = [] ∧ M.IsPath s₁ s₂ x'
nil₁ :
  (∃ (x' : List (Option α)), x'.reduceOption = [] ∧ M.IsPath s₁ s₂ x') →
    ∃ (n : ℕ), M.IsPath s₁ s₂ (List.replicate n none)
⊢ (∃ (n : ℕ), M.IsPath s₁ s₂ (List.replicate n none)) ↔
    ∃ (x' : List (Option α)), x'.reduceOption = [] ∧ M.IsPath s₁ s₂ x'

Tactic:
constructor
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
n : ℕ
h_1 : M.IsPath s₁ s₂ (List.replicate n none)
h : Eq.{u + 1} (α := List α) (List.reduceOption (List.replicate n none)) [] ∧ M.IsPath s₁ s₂ (List.replicate n none)
⊢ ∃ (x' : List (Option α)), x'.reduceOption = [] ∧ M.IsPath s₁ s₂ x'

Tactic:
use List.replicate n none

Premises used: List.replicate, Option.none
-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ : σ
n : ℕ
h_1 : M.IsPath s₁ s₂ (List.replicate n none)
h : Eq.{u + 1} (α := List α) [] [] ∧ M.IsPath s₁ s₂ (List.replicate n none)
⊢ Eq.{u + 1} (α := List α) (List.reduceOption (List.replicate n none)) [] ∧ M.IsPath s₁ s₂ (List.replicate n none)

Tactic:
rw [List.reduceOption_replicate_none]

Premises used: List.reduceOption_replicate_none