awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ (∃ (i : σ), (i ∈ S ∧ p) ∧ s ∈ M.step i a) ↔ (∃ i ∈ S, s ∈ M.step i a) ∧ p
have h₄ : ∀ (w : σ), s ∈ M.step w a → w ∈ S → p → ∃ i ∈ S, s ∈ M.step i a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ (∃ (i : σ), (i ∈ S ∧ p) ∧ s ∈ M.step i a) ↔ (∃ i ∈ S, s ∈ M.step i a) ∧ p
have h₅ : ∀ (w : σ), s ∈ M.step w a → w ∈ S → p → p
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ (∃ (i : σ), (i ∈ S ∧ p) ∧ s ∈ M.step i a) ↔ (∃ i ∈ S, s ∈ M.step i a) ∧ p
have h₆ : p → ∀ w ∈ S, s ∈ M.step w a → ∃ (i : σ), (i ∈ S ∧ p) ∧ s ∈ M.step i a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ (∃ (i : σ), (i ∈ S ∧ p) ∧ s ∈ M.step i a) ↔ (∃ i ∈ S, s ∈ M.step i a) ∧ p
have h₁₉ : p → ∀ w ∈ S, s ∈ M.step w a → (w ∈ S ∧ p) ∧ s ∈ M.step w a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ (∃ (i : σ), (i ∈ S ∧ p) ∧ s ∈ M.step i a) ↔ (∃ i ∈ S, s ∈ M.step i a) ∧ p
have h₂₀ : p → (w : σ) → w ∈ S → s ∈ M.step w a → σ
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (hypothesis)
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 σ
⊢ a :: x ∈ M.acceptsFrom {s : σ | s ∈ S ∧ p} ↔ a :: x ∈ M.acceptsFrom S ∧ p
have h : 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
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
p : Prop
x : List α
⊢ x ∈ M.acceptsFrom {s : σ | s ∈ S ∧ p} ↔ x ∈ M.acceptsFrom S ∧ p
have nil : ∀ {S : Set σ}, [] ∈ M.acceptsFrom {s : σ | s ∈ S ∧ p} ↔ [] ∈ 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]
Cleared hypotheses: S, x
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ x ∈ M.acceptsFrom {s : σ | s ∈ S ∧ p} ↔ x ∈ M.acceptsFrom S ∧ p
have 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
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]
Cleared hypotheses: S, x
-- Lean 4 proof step from Mathlib.Computability.NFA (hypothesis)
Goal:
α : Type u
σ : Type v
M : NFA α σ
s t : σ
x : List α
h : t ∈ M.evalFrom {s} []
⊢ s = t
have h₁ : t = s
Tactic: simp at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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 ∈ M.evalFrom {s} (a :: x)
have rw : ∃ t_2 ∈ M.step s a, t ∈ M.evalFrom {t_2} x
Tactic: rw [evalFrom_cons, stepSet_singleton, mem_evalFrom_iff_exists]
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
x : List α
⊢ x ∈ M.accepts ↔ ∃ s ∈ M.start, ∃ t ∈ M.accept, Nonempty (M.Path s t x)
have simp : (∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x) ↔ ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
Tactic: simp only [← mem_evalFrom_iff_nonempty_path, mem_accepts, mem_evalFrom_iff_exists (S := M.start)]
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
x : List α
⊢ (∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x) ↔ ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
have mp : (∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x) → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
x : List α
mp : (∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x) → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
⊢ (∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x) ↔ ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
have mpr : (∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x) → ∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
x : List α
mp : (∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x) → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
mpr : (∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x) → ∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x
⊢ (∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x) ↔ ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
have mp₁ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
x : List α
mp : (∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x) → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
mpr : (∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x) → ∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x
mp₁ mp₂ mp₃ :
  ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
⊢ (∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x) ↔ ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
have mpr₁ : ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → ∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
x : List α
mp : (∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x) → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
mpr : (∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x) → ∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x
mp₁ mp₂ mp₃ :
  ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
mpr₁ mpr₂ mpr₃ :
  ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → ∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x
mp₄ mp₅ mp₆ :
  ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
mpr₄ mpr₅ mpr₆ :
  ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → ∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x
mp₇ mp₈ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
⊢ (∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x) ↔ ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
have mp₉ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → w_1 ∈ M.start ∧ ∃ t ∈ M.accept, t ∈ M.evalFrom {w_1} x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
x : List α
mp : (∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x) → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
mpr : (∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x) → ∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x
mp₁ mp₂ mp₃ :
  ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
mpr₁ mpr₂ mpr₃ :
  ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → ∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x
mp₄ mp₅ mp₆ :
  ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
mpr₄ mpr₅ mpr₆ :
  ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → ∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x
mp₇ mp₈ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
mp₉ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → w_1 ∈ M.start ∧ ∃ t ∈ M.accept, t ∈ M.evalFrom {w_1} x
⊢ (∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x) ↔ ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
have mp₁₀ : (w : σ) → w ∈ M.accept → (w_1 : σ) → w_1 ∈ M.start → w ∈ M.evalFrom {w_1} x → σ
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
x : List α
mp : (∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x) → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
mpr : (∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x) → ∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x
mp₁ mp₂ mp₃ :
  ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
mpr₁ mpr₂ mpr₃ :
  ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → ∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x
mp₄ mp₅ mp₆ :
  ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
mpr₄ mpr₅ mpr₆ :
  ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → ∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x
mp₇ mp₈ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
mp₉ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → w_1 ∈ M.start ∧ ∃ t ∈ M.accept, t ∈ M.evalFrom {w_1} x
mp₁₀ : (w : σ) → w ∈ M.accept → (w_1 : σ) → w_1 ∈ M.start → w ∈ M.evalFrom {w_1} x → σ
mp₁₁ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → w_1 ∈ M.start ∧ ∃ t ∈ M.accept, t ∈ M.evalFrom {w_1} x
mp₁₂ : (w : σ) → w ∈ M.accept → (w_1 : σ) → w_1 ∈ M.start → w ∈ M.evalFrom {w_1} x → σ
⊢ (∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x) ↔ ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
have mp₁₃ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → w_1 ∈ M.start
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
x : List α
mp : (∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x) → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
mpr : (∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x) → ∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x
mp₁ mp₂ mp₃ :
  ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
mpr₁ mpr₂ mpr₃ :
  ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → ∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x
mp₄ mp₅ mp₆ :
  ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
mpr₄ mpr₅ mpr₆ :
  ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → ∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x
mp₇ mp₈ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
mp₉ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → w_1 ∈ M.start ∧ ∃ t ∈ M.accept, t ∈ M.evalFrom {w_1} x
mp₁₀ : (w : σ) → w ∈ M.accept → (w_1 : σ) → w_1 ∈ M.start → w ∈ M.evalFrom {w_1} x → σ
mp₁₁ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → w_1 ∈ M.start ∧ ∃ t ∈ M.accept, t ∈ M.evalFrom {w_1} x
mp₁₂ : (w : σ) → w ∈ M.accept → (w_1 : σ) → w_1 ∈ M.start → w ∈ M.evalFrom {w_1} x → σ
mp₁₃ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → w_1 ∈ M.start
⊢ (∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x) ↔ ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
have mp₁₄ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ t ∈ M.accept, t ∈ M.evalFrom {w_1} x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
x : List α
mp : (∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x) → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
mpr : (∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x) → ∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x
mp₁ mp₂ mp₃ :
  ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
mpr₁ mpr₂ mpr₃ :
  ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → ∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x
mp₄ mp₅ mp₆ :
  ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
mpr₄ mpr₅ mpr₆ :
  ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → ∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x
mp₇ mp₈ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
mp₉ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → w_1 ∈ M.start ∧ ∃ t ∈ M.accept, t ∈ M.evalFrom {w_1} x
mp₁₀ : (w : σ) → w ∈ M.accept → (w_1 : σ) → w_1 ∈ M.start → w ∈ M.evalFrom {w_1} x → σ
mp₁₁ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → w_1 ∈ M.start ∧ ∃ t ∈ M.accept, t ∈ M.evalFrom {w_1} x
mp₁₂ : (w : σ) → w ∈ M.accept → (w_1 : σ) → w_1 ∈ M.start → w ∈ M.evalFrom {w_1} x → σ
mp₁₃ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → w_1 ∈ M.start
mp₁₄ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ t ∈ M.accept, t ∈ M.evalFrom {w_1} x
mp₁₅ : (w : σ) → w ∈ M.accept → (w_1 : σ) → w_1 ∈ M.start → w ∈ M.evalFrom {w_1} x → σ
mp₁₆ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → w_1 ∈ M.start
mp₁₇ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ t ∈ M.accept, t ∈ M.evalFrom {w_1} x
mp₁₈ : (w : σ) → w ∈ M.accept → (w_1 : σ) → w_1 ∈ M.start → w ∈ M.evalFrom {w_1} x → σ
mp₁₉ mp₂₀ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ t ∈ M.accept, t ∈ M.evalFrom {w_1} x
mpr₇ mpr₈ :
  ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → ∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x
⊢ (∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x) ↔ ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
have mpr₉ : ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → w_1 ∈ M.accept ∧ ∃ t ∈ M.start, w_1 ∈ M.evalFrom {t} x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
x : List α
mp : (∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x) → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
mpr : (∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x) → ∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x
mp₁ mp₂ mp₃ :
  ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
mpr₁ mpr₂ mpr₃ :
  ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → ∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x
mp₄ mp₅ mp₆ :
  ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
mpr₄ mpr₅ mpr₆ :
  ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → ∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x
mp₇ mp₈ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
mp₉ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → w_1 ∈ M.start ∧ ∃ t ∈ M.accept, t ∈ M.evalFrom {w_1} x
mp₁₀ : (w : σ) → w ∈ M.accept → (w_1 : σ) → w_1 ∈ M.start → w ∈ M.evalFrom {w_1} x → σ
mp₁₁ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → w_1 ∈ M.start ∧ ∃ t ∈ M.accept, t ∈ M.evalFrom {w_1} x
mp₁₂ : (w : σ) → w ∈ M.accept → (w_1 : σ) → w_1 ∈ M.start → w ∈ M.evalFrom {w_1} x → σ
mp₁₃ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → w_1 ∈ M.start
mp₁₄ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ t ∈ M.accept, t ∈ M.evalFrom {w_1} x
mp₁₅ : (w : σ) → w ∈ M.accept → (w_1 : σ) → w_1 ∈ M.start → w ∈ M.evalFrom {w_1} x → σ
mp₁₆ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → w_1 ∈ M.start
mp₁₇ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ t ∈ M.accept, t ∈ M.evalFrom {w_1} x
mp₁₈ : (w : σ) → w ∈ M.accept → (w_1 : σ) → w_1 ∈ M.start → w ∈ M.evalFrom {w_1} x → σ
mp₁₉ mp₂₀ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ t ∈ M.accept, t ∈ M.evalFrom {w_1} x
mpr₇ mpr₈ :
  ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → ∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x
mpr₉ : ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → w_1 ∈ M.accept ∧ ∃ t ∈ M.start, w_1 ∈ M.evalFrom {t} x
⊢ (∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x) ↔ ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
have mpr₁₀ : (w : σ) → w ∈ M.start → (w_1 : σ) → w_1 ∈ M.accept → w_1 ∈ M.evalFrom {w} x → σ
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
x : List α
mp : (∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x) → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
mpr : (∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x) → ∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x
mp₁ mp₂ mp₃ :
  ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
mpr₁ mpr₂ mpr₃ :
  ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → ∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x
mp₄ mp₅ mp₆ :
  ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
mpr₄ mpr₅ mpr₆ :
  ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → ∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x
mp₇ mp₈ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
mp₉ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → w_1 ∈ M.start ∧ ∃ t ∈ M.accept, t ∈ M.evalFrom {w_1} x
mp₁₀ : (w : σ) → w ∈ M.accept → (w_1 : σ) → w_1 ∈ M.start → w ∈ M.evalFrom {w_1} x → σ
mp₁₁ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → w_1 ∈ M.start ∧ ∃ t ∈ M.accept, t ∈ M.evalFrom {w_1} x
mp₁₂ : (w : σ) → w ∈ M.accept → (w_1 : σ) → w_1 ∈ M.start → w ∈ M.evalFrom {w_1} x → σ
mp₁₃ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → w_1 ∈ M.start
mp₁₄ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ t ∈ M.accept, t ∈ M.evalFrom {w_1} x
mp₁₅ : (w : σ) → w ∈ M.accept → (w_1 : σ) → w_1 ∈ M.start → w ∈ M.evalFrom {w_1} x → σ
mp₁₆ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → w_1 ∈ M.start
mp₁₇ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ t ∈ M.accept, t ∈ M.evalFrom {w_1} x
mp₁₈ : (w : σ) → w ∈ M.accept → (w_1 : σ) → w_1 ∈ M.start → w ∈ M.evalFrom {w_1} x → σ
mp₁₉ mp₂₀ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ t ∈ M.accept, t ∈ M.evalFrom {w_1} x
mpr₇ mpr₈ :
  ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → ∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x
mpr₉ : ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → w_1 ∈ M.accept ∧ ∃ t ∈ M.start, w_1 ∈ M.evalFrom {t} x
mpr₁₀ : (w : σ) → w ∈ M.start → (w_1 : σ) → w_1 ∈ M.accept → w_1 ∈ M.evalFrom {w} x → σ
mpr₁₁ : ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → w_1 ∈ M.accept ∧ ∃ t ∈ M.start, w_1 ∈ M.evalFrom {t} x
mpr₁₂ : (w : σ) → w ∈ M.start → (w_1 : σ) → w_1 ∈ M.accept → w_1 ∈ M.evalFrom {w} x → σ
⊢ (∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x) ↔ ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
have mpr₁₃ : ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → w_1 ∈ M.accept
Tactic: tauto