awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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) []
⊢ M.evalFrom (⋃ (i : ι), s i) x = ⋃ (i : ι), M.evalFrom (s i) x
have 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)
Tactic: induction x generalizing s with
  | nil => simp
  | cons a x ih => simp [stepSet, Set.iUnion_comm (ι := σ) (ι' := ι), ih]
Cleared hypotheses: s, x
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
s : σ
S : Set σ
x : List α
⊢ s ∈ M.evalFrom S x ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} x
have rw : Membership.mem (γ := Set σ) (⋃ s ∈ S, M.evalFrom {s} x) s ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} x
Tactic: rw [evalFrom_eq_biUnion_singleton]
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
⊢ [] ∈ M.acceptsFrom S ↔ ∃ s ∈ S, s ∈ M.accept
have simp : (∃ s ∈ M.accept, s ∈ S) ↔ ∃ s ∈ S, s ∈ M.accept
Tactic: simp only [mem_acceptsFrom, evalFrom_nil]
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
⊢ (∃ s ∈ M.accept, s ∈ S) ↔ ∃ s ∈ S, s ∈ M.accept
have mp : (∃ s ∈ M.accept, s ∈ S) → ∃ s ∈ S, s ∈ M.accept
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
mp : (∃ s ∈ M.accept, s ∈ S) → ∃ s ∈ S, s ∈ M.accept
⊢ (∃ s ∈ M.accept, s ∈ S) ↔ ∃ s ∈ S, s ∈ M.accept
have mpr : (∃ s ∈ S, s ∈ M.accept) → ∃ s ∈ M.accept, s ∈ S
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ (∃ s ∈ M.accept, s ∈ S) ↔ ∃ s ∈ S, s ∈ M.accept
have mp₁ : ∀ w ∈ M.accept, w ∈ S → ∃ s ∈ S, s ∈ M.accept
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ (∃ s ∈ M.accept, s ∈ S) ↔ ∃ s ∈ S, s ∈ M.accept
have mpr₁ : ∀ w ∈ S, w ∈ M.accept → ∃ s ∈ M.accept, s ∈ S
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
a : α
⊢ (fun (x : List α) ↦ a :: x) ⁻¹' M.acceptsFrom S = M.acceptsFrom (M.stepSet S a)
have h : ∀ (x : List α),
  Membership.mem (γ := Set (List α)) ((fun (x : List α) ↦ a :: x) ⁻¹' M.acceptsFrom S) x ↔
    x ∈ M.acceptsFrom (M.stepSet S a)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
x : List α
⊢ (fun (x_1 : List α) ↦ x ++ x_1) ⁻¹' M.acceptsFrom S = M.acceptsFrom (M.evalFrom S x)
have 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)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
⊢ M.acceptsFrom (S ∪ T) = M.acceptsFrom S ∪ M.acceptsFrom T
have h : ∀ (x : List α), x ∈ M.acceptsFrom (S ∪ T) ↔ x ∈ M.acceptsFrom S ∪ M.acceptsFrom T
Tactic: ext x
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
⊢ x ∈ M.acceptsFrom (S ∪ T) ↔ x ∈ M.acceptsFrom S ∪ M.acceptsFrom T
have h : (∃ s ∈ M.accept, s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x) ↔ x ∈ M.acceptsFrom S ∪ M.acceptsFrom T
Tactic: simp only [mem_acceptsFrom, evalFrom_union, mem_union]
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
⊢ (∃ s ∈ M.accept, s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x) ↔ x ∈ M.acceptsFrom S ∪ M.acceptsFrom T
have h : (∃ s ∈ M.accept, s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x) → x ∈ M.acceptsFrom S ∪ M.acceptsFrom T
Tactic: constructor
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ (∃ s ∈ M.accept, s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x) ↔ x ∈ M.acceptsFrom S ∪ M.acceptsFrom T
have h₁ : x ∈ M.acceptsFrom S ∪ M.acceptsFrom T → ∃ s ∈ M.accept, s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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 ∪ M.acceptsFrom T
have h₁ : x ∈ M.acceptsFrom S
Tactic: left
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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 S ∪ M.acceptsFrom T
have h₁ : x ∈ M.acceptsFrom T
Tactic: right
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom S x
⊢ ∃ s ∈ M.accept, s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x
have h₁ : s ∈ M.accept ∧ (s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x)
Tactic: exists s
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
S T : Set σ
x : List α
s : σ
hs : s ∈ M.accept
h : s ∈ M.evalFrom T x
⊢ ∃ s ∈ M.accept, s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x
have h₁ : s ∈ M.accept ∧ (s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x)
Tactic: exists s
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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.accept ∧ (s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x)
have h₂ : s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ s ∈ M.accept ∧ (s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x)
have h₅ : s ∉ M.evalFrom S x → s ∈ M.evalFrom T x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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.accept ∧ (s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x)
have h₂ : s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ s ∈ M.accept ∧ (s ∈ M.evalFrom S x ∨ s ∈ M.evalFrom T x)
have h₅ : s ∉ M.evalFrom S x → s ∈ M.evalFrom T x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
ι : Sort u_1
s : ι → Set σ
⊢ M.acceptsFrom (⋃ (i : ι), s i) = ⋃ (i : ι), M.acceptsFrom (s i)
have h : ∀ (x : List α), x ∈ M.acceptsFrom (⋃ (i : ι), s i) ↔ Membership.mem (γ := Language α) (⋃ (i : ι), M.acceptsFrom (s i)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
ι : Sort u_1
s : ι → Set σ
x : List α
⊢ x ∈ M.acceptsFrom (⋃ (i : ι), s i) ↔ Membership.mem (γ := Language α) (⋃ (i : ι), M.acceptsFrom (s i)) x
have 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
Tactic: simp only [acceptsFrom, evalFrom_iUnion, mem_iUnion]
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
ι : Sort u_1
s : ι → Set σ
x : List α
⊢ 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
have 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
Tactic: simp_rw [↑mem_iUnion, ↑mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
ι : Sort u_1
s : ι → Set σ
x : List α
⊢ (∃ s_1 ∈ M.accept, ∃ (i : ι), s_1 ∈ M.evalFrom (s i) x) ↔ ∃ (i : ι), ∃ s_1 ∈ M.accept, s_1 ∈ M.evalFrom (s i) x
have 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
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ (∃ s_1 ∈ M.accept, ∃ (i : ι), s_1 ∈ M.evalFrom (s i) x) ↔ ∃ (i : ι), ∃ s_1 ∈ M.accept, s_1 ∈ M.evalFrom (s i) x
have 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
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ (∃ s_1 ∈ M.accept, ∃ (i : ι), s_1 ∈ M.evalFrom (s i) x) ↔ ∃ (i : ι), ∃ s_1 ∈ M.accept, s_1 ∈ M.evalFrom (s i) x
have 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
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ (∃ s_1 ∈ M.accept, ∃ (i : ι), s_1 ∈ M.evalFrom (s i) x) ↔ ∃ (i : ι), ∃ s_1 ∈ M.accept, s_1 ∈ M.evalFrom (s i) x
have 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
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ (∃ s_1 ∈ M.accept, ∃ (i : ι), s_1 ∈ M.evalFrom (s i) x) ↔ ∃ (i : ι), ∃ s_1 ∈ M.accept, s_1 ∈ M.evalFrom (s i) x
have 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
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ (∃ s_1 ∈ M.accept, ∃ (i : ι), s_1 ∈ M.evalFrom (s i) x) ↔ ∃ (i : ι), ∃ s_1 ∈ M.accept, s_1 ∈ M.evalFrom (s i) x
have h₁₇ : (w : σ) → w ∈ M.accept → (w_1 : ι) → w ∈ M.evalFrom (s w_1) x → ι
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ (∃ s_1 ∈ M.accept, ∃ (i : ι), s_1 ∈ M.evalFrom (s i) x) ↔ ∃ (i : ι), ∃ s_1 ∈ M.accept, s_1 ∈ M.evalFrom (s i) x
have 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
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ (∃ s_1 ∈ M.accept, ∃ (i : ι), s_1 ∈ M.evalFrom (s i) x) ↔ ∃ (i : ι), ∃ s_1 ∈ M.accept, s_1 ∈ M.evalFrom (s i) x
have h₂₃ : (w : ι) → (w_1 : σ) → w_1 ∈ M.accept → w_1 ∈ M.evalFrom (s w) x → σ
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
p : Prop
S : Set σ
⊢ [] ∈ M.acceptsFrom {s : σ | s ∈ S ∧ p} ↔ [] ∈ M.acceptsFrom S ∧ p
have nil : (∃ (s : σ), (s ∈ S ∧ p) ∧ s ∈ M.accept) ↔ (∃ s ∈ S, s ∈ M.accept) ∧ p
Tactic: simp only [nil_mem_acceptsFrom, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
p : Prop
S : Set σ
⊢ (∃ (s : σ), (s ∈ S ∧ p) ∧ s ∈ M.accept) ↔ (∃ s ∈ S, s ∈ M.accept) ∧ p
have nil : (∃ (s : σ), (s ∈ S ∧ p) ∧ s ∈ M.accept) → (∃ s ∈ S, s ∈ M.accept) ∧ p
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ (∃ (s : σ), (s ∈ S ∧ p) ∧ s ∈ M.accept) ↔ (∃ s ∈ S, s ∈ M.accept) ∧ p
have nil₁ : (∃ s ∈ S, s ∈ M.accept) ∧ p → ∃ (s : σ), (s ∈ S ∧ p) ∧ s ∈ M.accept
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ (∃ (s : σ), (s ∈ S ∧ p) ∧ s ∈ M.accept) ↔ (∃ s ∈ S, s ∈ M.accept) ∧ p
have nil₂ : ∀ w ∈ M.accept, w ∈ S → p → (∃ s ∈ S, s ∈ M.accept) ∧ p
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ (∃ (s : σ), (s ∈ S ∧ p) ∧ s ∈ M.accept) ↔ (∃ s ∈ S, s ∈ M.accept) ∧ p
have nil₄ : ∀ w ∈ M.accept, w ∈ S → p → ∃ s ∈ S, s ∈ M.accept
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ (∃ (s : σ), (s ∈ S ∧ p) ∧ s ∈ M.accept) ↔ (∃ s ∈ S, s ∈ M.accept) ∧ p
have nil₅ : ∀ w ∈ M.accept, w ∈ S → p → p
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ (∃ (s : σ), (s ∈ S ∧ p) ∧ s ∈ M.accept) ↔ (∃ s ∈ S, s ∈ M.accept) ∧ p
have nil₆ : p → ∀ w ∈ S, w ∈ M.accept → ∃ (s : σ), (s ∈ S ∧ p) ∧ s ∈ M.accept
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ (∃ (s : σ), (s ∈ S ∧ p) ∧ s ∈ M.accept) ↔ (∃ s ∈ S, s ∈ M.accept) ∧ p
have nil₁₉ : p → ∀ w ∈ S, w ∈ M.accept → (w ∈ S ∧ p) ∧ w ∈ M.accept
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ (∃ (s : σ), (s ∈ S ∧ p) ∧ s ∈ M.accept) ↔ (∃ s ∈ S, s ∈ M.accept) ∧ p
have nil₂₀ : p → (w : σ) → w ∈ S → w ∈ M.accept → σ
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 σ
⊢ M.stepSet {s : σ | s ∈ S ∧ p} a = {s : σ | s ∈ M.stepSet S a ∧ p}
have h : ∀ (s : σ), s ∈ M.stepSet {s : σ | s ∈ S ∧ p} a ↔ Membership.mem (γ := Set σ) {s : σ | s ∈ M.stepSet S a ∧ p} s
Tactic: ext s
-- 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 : σ
⊢ s ∈ M.stepSet {s : σ | s ∈ S ∧ p} a ↔ Membership.mem (γ := Set σ) {s : σ | s ∈ M.stepSet S a ∧ p} s
have h : (∃ (i : σ), (i ∈ S ∧ p) ∧ s ∈ M.step i a) ↔ (∃ i ∈ S, s ∈ M.step i a) ∧ p
Tactic: simp only [stepSet, mem_setOf_eq, mem_iUnion, exists_prop]
-- 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 : σ
⊢ (∃ (i : σ), (i ∈ S ∧ p) ∧ s ∈ M.step i a) ↔ (∃ i ∈ S, s ∈ M.step i a) ∧ p
have h : (∃ (i : σ), (i ∈ S ∧ p) ∧ s ∈ M.step i a) → (∃ i ∈ S, s ∈ M.step i a) ∧ 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
⊢ (∃ (i : σ), (i ∈ S ∧ p) ∧ s ∈ M.step i a) ↔ (∃ i ∈ S, s ∈ M.step i a) ∧ p
have h₁ : (∃ i ∈ S, s ∈ M.step i a) ∧ p → ∃ (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
⊢ (∃ (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) ∧ p
Tactic: tauto