awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
x : List α
simp : (∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x) ↔ ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
⊢ x ∈ M.accepts ↔ ∃ s ∈ M.start, ∃ t ∈ M.accept, Nonempty (M.Path s t x)

Tactic:
simp only [← mem_evalFrom_iff_nonempty_path, mem_accepts, mem_evalFrom_iff_exists (S := M.start)]

Premises used: NFA.mem_evalFrom_iff_exists, NFA.mem_accepts, NFA.mem_evalFrom_iff_nonempty_path
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
h : ∀ (x : List α), x ∈ M.toDFA.accepts ↔ x ∈ M.accepts
⊢ M.toDFA.accepts = M.accepts

Tactic:
ext x
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
x : List α
h : M.toDFA.eval x ∈ M.toDFA.accept → ∃ S ∈ M.accept, S ∈ M.evalFrom M.start x
h₁ : (∃ S ∈ M.accept, S ∈ M.evalFrom M.start x) → M.toDFA.eval x ∈ M.toDFA.accept
⊢ M.toDFA.eval x ∈ M.toDFA.accept ↔ ∃ S ∈ M.accept, S ∈ M.evalFrom M.start x

Tactic:
constructor
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
x : List α
⊢ M.toDFA.eval x ∈ M.toDFA.accept → ∃ S ∈ M.accept, S ∈ M.evalFrom M.start x

Tactic:
fun ⟨w, h2, h3⟩ => ⟨w, h3, h2⟩

Premises used: NFA.evalFrom, Membership.mem, Exists, NFA.start, NFA.accept, And, And.intro, Exists.intro, _private.0.NFA.toDFA_correct.match_1
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
x : List α
⊢ M.toDFA.eval x ∈ M.toDFA.accept → ∃ S ∈ M.accept, S ∈ M.evalFrom M.start x

Tactic:
exact fun ⟨w, h2, h3⟩ => ⟨w, h3, h2⟩
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
x : List α
⊢ (∃ S ∈ M.accept, S ∈ M.evalFrom M.start x) → M.toDFA.eval x ∈ M.toDFA.accept

Tactic:
fun ⟨w, h2, h3⟩ => ⟨w, h3, h2⟩

Premises used: Membership.mem, NFA.toDFA, DFA.accept, And.intro, Exists.intro, _private.0.NFA.toDFA_correct.match_2, DFA.eval
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
x : List α
⊢ (∃ S ∈ M.accept, S ∈ M.evalFrom M.start x) → M.toDFA.eval x ∈ M.toDFA.accept

Tactic:
exact fun ⟨w, h2, h3⟩ => ⟨w, h3, h2⟩
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
inst : Fintype σ
x : List α
hx : x ∈ M.accepts
hlen : Fintype.card.{v} (Set σ) ≤ x.length
rw :
  ∀ (hx : x ∈ M.toDFA.accepts) (hlen : Fintype.card.{v} (Set σ) ≤ x.length),
    ∃ (a : List α) (b : List α) (c : List α),
      x = a ++ b ++ c ∧
        a.length + b.length ≤ Fintype.card.{v} (Set σ) ∧
          b ≠ [] ∧ HMul.hMul (α := Language α) {a} {b}∗ * {c} ≤ M.toDFA.accepts
⊢ ∃ (a : List α) (b : List α) (c : List α),
    x = a ++ b ++ c ∧
      a.length + b.length ≤ Fintype.card.{v} (Set σ) ∧ b ≠ [] ∧ HMul.hMul (α := Language α) {a} {b}∗ * {c} ≤ M.accepts

Tactic:
rw [← toDFA_correct] at hx ⊢

Premises used: NFA.toDFA_correct
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
inst : Fintype σ
x : List α
hx : x ∈ M.toDFA.accepts
hlen : Fintype.card.{v} (Set σ) ≤ x.length
⊢ ∃ (a : List α) (b : List α) (c : List α),
    x = a ++ b ++ c ∧
      a.length + b.length ≤ Fintype.card.{v} (Set σ) ∧
        b ≠ [] ∧ HMul.hMul (α := Language α) {a} {b}∗ * {c} ≤ M.toDFA.accepts

Tactic:
M.toDFA.pumping_lemma hx hlen

Premises used: NFA.toDFA, DFA.pumping_lemma
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
inst : Fintype σ
x : List α
hx : x ∈ M.toDFA.accepts
hlen : Fintype.card.{v} (Set σ) ≤ x.length
⊢ ∃ (a : List α) (b : List α) (c : List α),
    x = a ++ b ++ c ∧
      a.length + b.length ≤ Fintype.card.{v} (Set σ) ∧
        b ≠ [] ∧ HMul.hMul (α := Language α) {a} {b}∗ * {c} ≤ M.toDFA.accepts

Tactic:
exact M.toDFA.pumping_lemma hx hlen

Premises used: NFA.toDFA, DFA.pumping_lemma
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
start : σ
⊢ List.foldl M.toNFA.stepSet {start} [] = {List.foldl M.step start []}

Tactic:
tauto
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
a : α
s : List α
ih : ∀ (start : σ), List.foldl M.toNFA.stepSet {start} s = {List.foldl M.step start s}
start : σ
⊢ M.toNFA.stepSet {start} a = {M.step start a}

Tactic:
simp [NFA.stepSet]

Premises used: NFA.stepSet
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
a : α
s : List α
ih : ∀ (start : σ), List.foldl M.toNFA.stepSet {start} s = {List.foldl M.step start s}
start : σ
cons : List.foldl M.toNFA.stepSet {M.step start a} s = {List.foldl M.step (M.step start a) s}
⊢ List.foldl M.toNFA.stepSet {start} (a :: s) = {List.foldl M.step start (a :: s)}

Tactic:
rw [List.foldl, List.foldl,
      show M.toNFA.stepSet {start} a = {M.step start a} by simp [NFA.stepSet]]

Premises used: List.foldl
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
a : α
s : List α
ih : ∀ (start : σ), List.foldl M.toNFA.stepSet {start} s = {List.foldl M.step start s}
start : σ
⊢ List.foldl M.toNFA.stepSet {M.step start a} s = {List.foldl M.step (M.step start a) s}

Tactic:
tauto
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
start : σ
s : List α
nil : ∀ (start : σ), List.foldl M.toNFA.stepSet {start} [] = {List.foldl M.step start []}
cons :
  ∀ (a : α) (s : List α) (ih : ∀ (start : σ), List.foldl M.toNFA.stepSet {start} s = {List.foldl M.step start s})
    (start : σ), List.foldl M.toNFA.stepSet {start} (a :: s) = {List.foldl M.step start (a :: s)}
⊢ List.foldl M.toNFA.stepSet {start} s = {List.foldl M.step start s}

Tactic:
induction s generalizing start with
  | nil => tauto
  | cons a s ih =>
    rw [List.foldl, List.foldl,
      show M.toNFA.stepSet {start} a = {M.step start a} by simp [NFA.stepSet]]
    tauto

Premises used: List.foldl
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
h : ∀ (x : List α), x ∈ M.toNFA.accepts ↔ x ∈ M.accepts
⊢ M.toNFA.accepts = M.accepts

Tactic:
ext x
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
x : List α
h : (∃ S ∈ M.toNFA.accept, Membership.mem (γ := Set σ) {M.evalFrom M.start x} S) ↔ x ∈ M.accepts
⊢ x ∈ M.toNFA.accepts ↔ x ∈ M.accepts

Tactic:
rw [NFA.mem_accepts, toNFA_start, toNFA_evalFrom_match]

Premises used: DFA.toNFA_start, DFA.toNFA_evalFrom_match, NFA.mem_accepts
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
x : List α
h : (∃ S ∈ M.toNFA.accept, Membership.mem (γ := Set σ) {M.evalFrom M.start x} S) → x ∈ M.accepts
h₁ : x ∈ M.accepts → ∃ S ∈ M.toNFA.accept, Membership.mem (γ := Set σ) {M.evalFrom M.start x} S
⊢ (∃ S ∈ M.toNFA.accept, Membership.mem (γ := Set σ) {M.evalFrom M.start x} S) ↔ x ∈ M.accepts

Tactic:
constructor
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
x : List α
S : σ
hS₁ : S ∈ M.toNFA.accept
hS₂ : Membership.mem (γ := Set σ) {M.evalFrom M.start x} S
h h₁ h₂ h₃ :
  ∀ (hS₁ : M.evalFrom M.start x ∈ M.toNFA.accept) (hS₂ : Membership.mem (γ := Set σ) {M.evalFrom M.start x} S),
    x ∈ M.accepts
⊢ x ∈ M.accepts

Tactic:
rwa [Set.mem_singleton_iff.mp hS₂] at hS₁

Premises used: Set.mem_singleton_iff, Iff.mp
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
x : List α
⊢ x ∈ M.accepts → ∃ S ∈ M.toNFA.accept, Membership.mem (γ := Set σ) {M.evalFrom M.start x} S

Tactic:
fun h => ⟨M.eval x, h, rfl⟩

Premises used: And.intro, Exists.intro, DFA.eval, rfl
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : DFA α σ
x : List α
⊢ x ∈ M.accepts → ∃ S ∈ M.toNFA.accept, Membership.mem (γ := Set σ) {M.evalFrom M.start x} S

Tactic:
exact fun h => ⟨M.eval x, h, rfl⟩
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
⊢ M.reverse.reverse = M

Tactic:
simp [reverse]

Premises used: NFA.reverse
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
a : α
S S' : Set σ
rw : ¬Disjoint S (M.reverse.stepSet S' a) ↔ ¬Disjoint S' (M.stepSet S a)
⊢ Disjoint S (M.reverse.stepSet S' a) ↔ Disjoint S' (M.stepSet S a)

Tactic:
rw [← not_iff_not]

Premises used: not_iff_not
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
a : α
S S' : Set σ
simp : (∃ x ∈ S, ∃ t ∈ S', t ∈ M.step x a) ↔ ∃ x ∈ S', ∃ t ∈ S, x ∈ M.step t a
⊢ ¬Disjoint S (M.reverse.stepSet S' a) ↔ ¬Disjoint S' (M.stepSet S a)

Tactic:
simp only [Set.not_disjoint_iff, mem_stepSet, reverse_step, Set.mem_setOf_eq]

Premises used: NFA.reverse_step, Set.mem_setOf_eq, Set.not_disjoint_iff, NFA.mem_stepSet
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
a : α
S S' : Set σ
mp : (∃ x ∈ S, ∃ t ∈ S', t ∈ M.step x a) → ∃ x ∈ S', ∃ t ∈ S, x ∈ M.step t a
mpr : (∃ x ∈ S', ∃ t ∈ S, x ∈ M.step t a) → ∃ x ∈ S, ∃ t ∈ S', t ∈ M.step x a
mp₁ mp₂ mp₃ : ∀ w ∈ S, ∀ w_1 ∈ S', w_1 ∈ M.step w a → ∃ x ∈ S', ∃ t ∈ S, x ∈ M.step t a
mpr₁ mpr₂ mpr₃ : ∀ w ∈ S', ∀ w_1 ∈ S, w ∈ M.step w_1 a → ∃ x ∈ S, ∃ t ∈ S', t ∈ M.step x a
mp₄ mp₅ mp₆ : ∀ w ∈ S, ∀ w_1 ∈ S', w_1 ∈ M.step w a → ∃ x ∈ S', ∃ t ∈ S, x ∈ M.step t a
mpr₄ mpr₅ mpr₆ : ∀ w ∈ S', ∀ w_1 ∈ S, w ∈ M.step w_1 a → ∃ x ∈ S, ∃ t ∈ S', t ∈ M.step x a
mp₇ mp₈ : ∀ w ∈ S, ∀ w_1 ∈ S', w_1 ∈ M.step w a → ∃ x ∈ S', ∃ t ∈ S, x ∈ M.step t a
mp₉ : ∀ w ∈ S, ∀ w_1 ∈ S', w_1 ∈ M.step w a → w_1 ∈ S' ∧ ∃ t ∈ S, w_1 ∈ M.step t a
mp₁₀ : (w : σ) → w ∈ S → (w_1 : σ) → w_1 ∈ S' → w_1 ∈ M.step w a → σ
mp₁₁ : ∀ w ∈ S, ∀ w_1 ∈ S', w_1 ∈ M.step w a → w_1 ∈ S' ∧ ∃ t ∈ S, w_1 ∈ M.step t a
mp₁₂ : (w : σ) → w ∈ S → (w_1 : σ) → w_1 ∈ S' → w_1 ∈ M.step w a → σ
mp₁₃ : ∀ w ∈ S, ∀ w_1 ∈ S', w_1 ∈ M.step w a → w_1 ∈ S'
mp₁₄ : ∀ w ∈ S, ∀ w_1 ∈ S', w_1 ∈ M.step w a → ∃ t ∈ S, w_1 ∈ M.step t a
mp₁₅ : (w : σ) → w ∈ S → (w_1 : σ) → w_1 ∈ S' → w_1 ∈ M.step w a → σ
mp₁₆ : ∀ w ∈ S, ∀ w_1 ∈ S', w_1 ∈ M.step w a → w_1 ∈ S'
mp₁₇ : ∀ w ∈ S, ∀ w_1 ∈ S', w_1 ∈ M.step w a → ∃ t ∈ S, w_1 ∈ M.step t a
mp₁₈ : (w : σ) → w ∈ S → (w_1 : σ) → w_1 ∈ S' → w_1 ∈ M.step w a → σ
mp₁₉ mp₂₀ : ∀ w ∈ S, ∀ w_1 ∈ S', w_1 ∈ M.step w a → ∃ t ∈ S, w_1 ∈ M.step t a
mpr₇ mpr₈ : ∀ w ∈ S', ∀ w_1 ∈ S, w ∈ M.step w_1 a → ∃ x ∈ S, ∃ t ∈ S', t ∈ M.step x a
mpr₉ : ∀ w ∈ S', ∀ w_1 ∈ S, w ∈ M.step w_1 a → w_1 ∈ S ∧ ∃ t ∈ S', t ∈ M.step w_1 a
mpr₁₀ : (w : σ) → w ∈ S' → (w_1 : σ) → w_1 ∈ S → w ∈ M.step w_1 a → σ
mpr₁₁ : ∀ w ∈ S', ∀ w_1 ∈ S, w ∈ M.step w_1 a → w_1 ∈ S ∧ ∃ t ∈ S', t ∈ M.step w_1 a
mpr₁₂ : (w : σ) → w ∈ S' → (w_1 : σ) → w_1 ∈ S → w ∈ M.step w_1 a → σ
mpr₁₃ : ∀ w ∈ S', ∀ w_1 ∈ S, w ∈ M.step w_1 a → w_1 ∈ S
mpr₁₄ : ∀ w ∈ S', ∀ w_1 ∈ S, w ∈ M.step w_1 a → ∃ t ∈ S', t ∈ M.step w_1 a
mpr₁₅ : (w : σ) → w ∈ S' → (w_1 : σ) → w_1 ∈ S → w ∈ M.step w_1 a → σ
mpr₁₆ : ∀ w ∈ S', ∀ w_1 ∈ S, w ∈ M.step w_1 a → w_1 ∈ S
mpr₁₇ : ∀ w ∈ S', ∀ w_1 ∈ S, w ∈ M.step w_1 a → ∃ t ∈ S', t ∈ M.step w_1 a
mpr₁₈ : (w : σ) → w ∈ S' → (w_1 : σ) → w_1 ∈ S → w ∈ M.step w_1 a → σ
mpr₁₉ mpr₂₀ : ∀ w ∈ S', ∀ w_1 ∈ S, w ∈ M.step w_1 a → ∃ t ∈ S', t ∈ M.step w_1 a
⊢ (∃ x ∈ S, ∃ t ∈ S', t ∈ M.step x a) ↔ ∃ x ∈ S', ∃ t ∈ S, x ∈ M.step t a

Tactic:
tauto
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
x : List α
S S' : Set σ
h : Disjoint S (M.reverse.evalFrom S' x)
simp : Disjoint S' (List.foldr (fun (x : α) (y : Set σ) ↦ M.stepSet y x) S x)
⊢ Disjoint S' (M.evalFrom S x.reverse)

Tactic:
simp only [evalFrom, List.foldl_reverse] at h ⊢

Premises used: NFA.evalFrom, List.foldl_reverse
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S S' : Set σ
h : Disjoint S (List.foldl M.reverse.stepSet S' [])
nil : Disjoint (List.foldr (fun (x : α) (y : Set σ) ↦ M.stepSet y x) S []) S'
⊢ Disjoint S' (List.foldr (fun (x : α) (y : Set σ) ↦ M.stepSet y x) S [])

Tactic:
rw [disjoint_comm]

Premises used: disjoint_comm
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S S' : Set σ
h : Disjoint S (List.foldl M.reverse.stepSet S' [])
⊢ Disjoint (List.foldr (fun (x : α) (y : Set σ) ↦ M.stepSet y x) S []) S'

Tactic:
h

Premises used: List.foldl, List.foldr
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
S S' : Set σ
h : Disjoint S (List.foldl M.reverse.stepSet S' [])
⊢ Disjoint (List.foldr (fun (x : α) (y : Set σ) ↦ M.stepSet y x) S []) S'

Tactic:
exact h
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
x : α
xs : List α
ih :
  ∀ {S S' : Set σ} (h : Disjoint S (List.foldl M.reverse.stepSet S' xs)),
    Disjoint S' (List.foldr (fun (x : α) (y : Set σ) ↦ M.stepSet y x) S xs)
S S' : Set σ
h : Disjoint S (List.foldl M.reverse.stepSet S' (x :: xs))
⊢ Disjoint S (List.foldl M.reverse.stepSet (M.reverse.stepSet S' x) xs)

Tactic:
rw [List.foldl_cons] at h

Premises used: List.foldl_cons
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
x : α
xs : List α
ih :
  ∀ {S S' : Set σ} (h : Disjoint S (List.foldl M.reverse.stepSet S' xs)),
    Disjoint S' (List.foldr (fun (x : α) (y : Set σ) ↦ M.stepSet y x) S xs)
S S' : Set σ
h : Disjoint S (List.foldl M.reverse.stepSet (M.reverse.stepSet S' x) xs)
cons : Disjoint (M.reverse.stepSet S' x) (List.foldr (fun (x : α) (y : Set σ) ↦ M.stepSet y x) S xs)
⊢ Disjoint S' (List.foldr (fun (x : α) (y : Set σ) ↦ M.stepSet y x) S (x :: xs))

Tactic:
rw [List.foldr_cons, ← NFA.disjoint_stepSet_reverse, disjoint_comm]

Premises used: List.foldr_cons, disjoint_comm, NFA.disjoint_stepSet_reverse
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
x : α
xs : List α
ih :
  ∀ {S S' : Set σ} (h : Disjoint S (List.foldl M.reverse.stepSet S' xs)),
    Disjoint S' (List.foldr (fun (x : α) (y : Set σ) ↦ M.stepSet y x) S xs)
S S' : Set σ
h : Disjoint S (List.foldl M.reverse.stepSet (M.reverse.stepSet S' x) xs)
⊢ Disjoint (M.reverse.stepSet S' x) (List.foldr (fun (x : α) (y : Set σ) ↦ M.stepSet y x) S xs)

Tactic:
ih h
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
x : α
xs : List α
ih :
  ∀ {S S' : Set σ} (h : Disjoint S (List.foldl M.reverse.stepSet S' xs)),
    Disjoint S' (List.foldr (fun (x : α) (y : Set σ) ↦ M.stepSet y x) S xs)
S S' : Set σ
h : Disjoint S (List.foldl M.reverse.stepSet (M.reverse.stepSet S' x) xs)
⊢ Disjoint (M.reverse.stepSet S' x) (List.foldr (fun (x : α) (y : Set σ) ↦ M.stepSet y x) S xs)

Tactic:
exact ih h
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
x : List α
S S' : Set σ
h : Disjoint S (List.foldl M.reverse.stepSet S' x)
nil :
  ∀ {S S' : Set σ} (h : Disjoint S (List.foldl M.reverse.stepSet S' [])),
    Disjoint S' (List.foldr (fun (x : α) (y : Set σ) ↦ M.stepSet y x) S [])
cons :
  ∀ (x : α) (xs : List α)
    (ih :
      ∀ {S S' : Set σ} (h : Disjoint S (List.foldl M.reverse.stepSet S' xs)),
        Disjoint S' (List.foldr (fun (x : α) (y : Set σ) ↦ M.stepSet y x) S xs))
    {S S' : Set σ} (h : Disjoint S (List.foldl M.reverse.stepSet S' (x :: xs))),
    Disjoint S' (List.foldr (fun (x : α) (y : Set σ) ↦ M.stepSet y x) S (x :: xs))
⊢ Disjoint S' (List.foldr (fun (x : α) (y : Set σ) ↦ M.stepSet y x) S x)

Tactic:
induction x generalizing S S' with
  | nil =>
    rw [disjoint_comm]
    exact h
  | cons x xs ih =>
    rw [List.foldl_cons] at h
    rw [List.foldr_cons, ← NFA.disjoint_stepSet_reverse, disjoint_comm]
    exact ih h

Premises used: List.foldr_cons, disjoint_comm, NFA.disjoint_stepSet_reverse, List.foldl_cons
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
x : List α
S S' : Set σ
⊢ Disjoint S (M.reverse.evalFrom S' x) ↔ Disjoint S' (M.evalFrom S x.reverse)

Tactic:
⟨disjoint_evalFrom_reverse, fun h ↦ List.reverse_reverse x ▸ disjoint_evalFrom_reverse h⟩

Premises used: Eq.rec, List.reverse_reverse, Iff.intro, NFA.disjoint_evalFrom_reverse
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
x : List α
⊢ x ∈ M.reverse.accepts ↔ x.reverse ∈ M.accepts

Tactic:
simp [mem_accepts, ← Set.not_disjoint_iff, disjoint_evalFrom_reverse_iff]

Premises used: NFA.disjoint_evalFrom_reverse_iff, Set.not_disjoint_iff, NFA.mem_accepts
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
L : Language α
h : L.IsRegular
σ : Type
w : Fintype σ
M : DFA α σ
hM : M.accepts = L
h₁ : ∀ (x : List α), x ∈ M.toNFA.reverse.toDFA.accepts ↔ x ∈ L.reverse
⊢ M.toNFA.reverse.toDFA.accepts = L.reverse

Tactic:
ext
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
L : Language α
h : L.IsRegular
σ : Type
w : Fintype σ
M : DFA α σ
hM : M.accepts = L
x : List α
⊢ x ∈ M.toNFA.reverse.toDFA.accepts ↔ x ∈ L.reverse

Tactic:
simp [hM]
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
L : Language α
h : L.reverse.IsRegular
⊢ L.IsRegular

Tactic:
L.reverse_reverse ▸ h.reverse

Premises used: Eq.rec, Language.IsRegular.reverse, Language.reverse_reverse
-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
L : Language α
⊢ L.reverse.IsRegular ↔ L.IsRegular

Tactic:
⟨.of_reverse, .reverse⟩

Premises used: Language.IsRegular.reverse, Language.IsRegular.of_reverse, Iff.intro
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
let : ∀ (n : ℕ) (pn : true ∈ p n ∧ ∀ k < n, (p k).Dom) (a : ℕ), Acc (lbp p) a
⊢ ∀ (a : ℕ), Acc (lbp p) a

Tactic:
let ⟨n, pn⟩ := H
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
this : ∀ (m k : ℕ), n ≤ k + m → Acc (lbp p) k
⊢ ∀ (a : ℕ), Acc (lbp p) a

Tactic:
fun a => this _ _ (Nat.le_add_left _ _)

Premises used: Nat.le_add_left
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
this : ∀ (m k : ℕ), n ≤ k + m → Acc (lbp p) k
⊢ ∀ (a : ℕ), Acc (lbp p) a

Tactic:
exact fun a => this _ _ (Nat.le_add_left _ _)

Premises used: Nat.le_add_left
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
suffices : ∀ (m k : ℕ), n ≤ k + m → Acc (lbp p) k
⊢ ∀ (a : ℕ), Acc (lbp p) a

Tactic:
suffices ∀ m k, n ≤ k + m → Acc (lbp p) k by exact fun a => this _ _ (Nat.le_add_left _ _)
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
k : ℕ
kn : n ≤ k + 0
⊢ Acc (lbp p) k

Tactic:
⟨_, fun y r => ?_⟩

Premises used: Acc.intro
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
k : ℕ
kn : n ≤ k + 0
zero : ∀ (y : ℕ) (r : lbp p y k), Acc (lbp p) y
⊢ Acc (lbp p) k

Tactic:
refine ⟨_, fun y r => ?_⟩
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
k : ℕ
kn : n ≤ k + 0
y : ℕ
r : lbp p y k
zero : ∀ (a : ∀ k_1 ≤ k, false ∈ p k_1), Acc (lbp p) (k + 1)
⊢ Acc (lbp p) y

Tactic:
rcases r with ⟨rfl, a⟩

Premises used: rfl
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
k : ℕ
kn : n ≤ k + 0
a : ∀ k_1 ≤ k, false ∈ p k_1
⊢ Acc (lbp p) (k + 1)

Tactic:
injection mem_unique pn.1 (a _ kn)

Premises used: And.left, Part.mem_unique
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : ∀ (k : ℕ) (kn : n ≤ k + m), Acc (lbp p) k
k : ℕ
kn : n ≤ k + (m + 1)
⊢ Acc (lbp p) k

Tactic:
⟨_, fun y r => ?_⟩

Premises used: Acc.intro
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : ∀ (k : ℕ) (kn : n ≤ k + m), Acc (lbp p) k
k : ℕ
kn : n ≤ k + (m + 1)
succ : ∀ (y : ℕ) (r : lbp p y k), Acc (lbp p) y
⊢ Acc (lbp p) k

Tactic:
refine ⟨_, fun y r => ?_⟩
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : ∀ (k : ℕ) (kn : n ≤ k + m), Acc (lbp p) k
k : ℕ
kn : n ≤ k + (m + 1)
y : ℕ
r : lbp p y k
succ : ∀ (a : ∀ k_1 ≤ k, false ∈ p k_1), Acc (lbp p) (k + 1)
⊢ Acc (lbp p) y

Tactic:
rcases r with ⟨rfl, a⟩

Premises used: rfl
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : ∀ (k : ℕ) (kn : n ≤ k + m), Acc (lbp p) k
k : ℕ
kn : n ≤ k + (m + 1)
a : ∀ k_1 ≤ k, false ∈ p k_1
rw : n ≤ k + m + 1
⊢ n ≤ k + 1 + m

Tactic:
rw [Nat.add_right_comm]

Premises used: Nat.add_right_comm
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : ∀ (k : ℕ) (kn : n ≤ k + m), Acc (lbp p) k
k : ℕ
kn : n ≤ k + (m + 1)
a : ∀ k_1 ≤ k, false ∈ p k_1
⊢ n ≤ k + m + 1

Tactic:
kn
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : ∀ (k : ℕ) (kn : n ≤ k + m), Acc (lbp p) k
k : ℕ
kn : n ≤ k + (m + 1)
a : ∀ k_1 ≤ k, false ∈ p k_1
⊢ n ≤ k + m + 1

Tactic:
exact kn
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : ∀ (k : ℕ) (kn : n ≤ k + m), Acc (lbp p) k
k : ℕ
kn : n ≤ k + (m + 1)
a : ∀ k_1 ≤ k, false ∈ p k_1
⊢ Acc (lbp p) (k + 1)

Tactic:
exact IH _ (by rw [Nat.add_right_comm]; exact kn)
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
m k : ℕ
kn : n ≤ k + m
zero : ∀ (k : ℕ) (kn : n ≤ k + 0), Acc (lbp p) k
zero₁ : ∀ (k : ℕ) (kn : n ≤ k + 0) (a : ∀ k_1 ≤ k, false ∈ p k_1), Acc (lbp p) (k + 1)
succ : ∀ (m : ℕ) (IH : ∀ (k : ℕ) (kn : n ≤ k + m), Acc (lbp p) k) (k : ℕ) (kn : n ≤ k + (m + 1)), Acc (lbp p) k
succ₁ :
  ∀ (m : ℕ) (IH : ∀ (k : ℕ) (kn : n ≤ k + m), Acc (lbp p) k) (k : ℕ) (kn : n ≤ k + (m + 1))
    (a : ∀ k_1 ≤ k, false ∈ p k_1), Acc (lbp p) (k + 1)
⊢ Acc (lbp p) k

Tactic:
induction m generalizing k with (refine ⟨_, fun y r => ?_⟩; rcases r with ⟨rfl, a⟩)
    | zero => injection mem_unique pn.1 (a _ kn)
    | succ m IH => exact IH _ (by rw [Nat.add_right_comm]; exact kn)

Premises used: Nat.zero, Nat.succ, rfl
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
H : ∃ (n : ℕ), true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, false ∈ p n) → { n : ℕ // true ∈ p n ∧ ∀ m < n, false ∈ p m }
al : ∀ n < m, false ∈ p n
rcases : ∀ (n : ℕ) (h₁ : true ∈ p n) (h₂ : ∀ k < n, (p k).Dom), (p m).Dom
⊢ (p m).Dom

Tactic:
rcases H with ⟨n, h₁, h₂⟩
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, false ∈ p n) → { n : ℕ // true ∈ p n ∧ ∀ m < n, false ∈ p m }
al : ∀ n < m, false ∈ p n
n : ℕ
h₁ : true ∈ p n
h₂ : ∀ k < n, (p k).Dom
inl : ∀ (h₃ : m < n), (p m).Dom
inr : ∀ (h₃ : m = n), (p m).Dom
inr₁ : ∀ (h₃ : n < m), (p m).Dom
⊢ (p m).Dom

Tactic:
rcases lt_trichotomy m n with (h₃ | h₃ | h₃)

Premises used: lt_trichotomy
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, false ∈ p n) → { n : ℕ // true ∈ p n ∧ ∀ m < n, false ∈ p m }
al : ∀ n < m, false ∈ p n
n : ℕ
h₁ : true ∈ p n
h₂ : ∀ k < n, (p k).Dom
h₃ : m < n
⊢ (p m).Dom

Tactic:
h₂ _ h₃
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, false ∈ p n) → { n : ℕ // true ∈ p n ∧ ∀ m < n, false ∈ p m }
al : ∀ n < m, false ∈ p n
n : ℕ
h₁ : true ∈ p n
h₂ : ∀ k < n, (p k).Dom
h₃ : m < n
⊢ (p m).Dom

Tactic:
exact h₂ _ h₃
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, false ∈ p n) → { n : ℕ // true ∈ p n ∧ ∀ m < n, false ∈ p m }
al : ∀ n < m, false ∈ p n
n : ℕ
h₁ : true ∈ p n
h₂ : ∀ k < n, (p k).Dom
h₃ : m = n
inr : (p n).Dom
⊢ (p m).Dom

Tactic:
rw [h₃]
-- Module: Mathlib.Computability.Partrec
Goal:
p : ℕ →. Bool
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, false ∈ p n) → { n : ℕ // true ∈ p n ∧ ∀ m < n, false ∈ p m }
al : ∀ n < m, false ∈ p n
n : ℕ
h₁ : true ∈ p n
h₂ : ∀ k < n, (p k).Dom
h₃ : m = n
⊢ (p n).Dom

Tactic:
h₁.fst

Premises used: Exists.fst