awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 → σ
mpr₁₃ : ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → w_1 ∈ M.accept
⊢ (∃ 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 → ∃ 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 α σ
⊢ M.toDFA.accepts = M.accepts
have h : ∀ (x : List α), x ∈ M.toDFA.accepts ↔ x ∈ M.accepts
Tactic: ext x
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
have h : M.toDFA.eval x ∈ M.toDFA.accept → ∃ S ∈ M.accept, S ∈ M.evalFrom M.start x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ M.toDFA.eval x ∈ M.toDFA.accept ↔ ∃ S ∈ M.accept, S ∈ M.evalFrom M.start x
have h₁ : (∃ S ∈ M.accept, S ∈ M.evalFrom M.start x) → M.toDFA.eval x ∈ M.toDFA.accept
Tactic: constructor
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
inst : Fintype σ
x : List α
hx : x ∈ M.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.accepts
have 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
Tactic: rw [← toDFA_correct] at hx ⊢
Cleared hypotheses: hx, hlen
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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 {start} (a :: s) = {List.foldl M.step start (a :: s)}
have cons : List.foldl M.toNFA.stepSet {M.step start a} s = {List.foldl M.step (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]]
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
start : σ
s : List α
⊢ List.foldl M.toNFA.stepSet {start} s = {List.foldl M.step start s}
have nil : ∀ (start : σ), List.foldl M.toNFA.stepSet {start} [] = {List.foldl M.step start []}
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
Cleared hypotheses: start, s
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
start : σ
s : List α
nil : ∀ (start : σ), List.foldl M.toNFA.stepSet {start} [] = {List.foldl M.step start []}
⊢ List.foldl M.toNFA.stepSet {start} s = {List.foldl M.step start s}
have 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)}
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
Cleared hypotheses: start, s
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
⊢ M.toNFA.accepts = M.accepts
have h : ∀ (x : List α), x ∈ M.toNFA.accepts ↔ x ∈ M.accepts
Tactic: ext x
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
x : List α
⊢ x ∈ M.toNFA.accepts ↔ x ∈ M.accepts
have h : (∃ S ∈ M.toNFA.accept, Membership.mem (γ := Set σ) {M.evalFrom M.start x} S) ↔ x ∈ M.accepts
Tactic: rw [NFA.mem_accepts, toNFA_start, toNFA_evalFrom_match]
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
x : List α
⊢ (∃ S ∈ M.toNFA.accept, Membership.mem (γ := Set σ) {M.evalFrom M.start x} S) ↔ x ∈ M.accepts
have h : (∃ S ∈ M.toNFA.accept, Membership.mem (γ := Set σ) {M.evalFrom M.start x} S) → x ∈ M.accepts
Tactic: constructor
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ (∃ S ∈ M.toNFA.accept, Membership.mem (γ := Set σ) {M.evalFrom M.start x} S) ↔ x ∈ M.accepts
have h₁ : x ∈ M.accepts → ∃ S ∈ M.toNFA.accept, Membership.mem (γ := Set σ) {M.evalFrom M.start x} S
Tactic: constructor
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ x ∈ M.accepts
have h : ∀ (hS₁ : M.evalFrom M.start x ∈ M.toNFA.accept) (hS₂ : Membership.mem (γ := Set σ) {M.evalFrom M.start x} S),
  x ∈ M.accepts
Tactic: rwa [Set.mem_singleton_iff.mp hS₂] at hS₁
Cleared hypotheses: hS₁, hS₂
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
a : α
S S' : Set σ
⊢ Disjoint S (M.reverse.stepSet S' a) ↔ Disjoint S' (M.stepSet S a)
have rw : ¬Disjoint S (M.reverse.stepSet S' a) ↔ ¬Disjoint S' (M.stepSet S a)
Tactic: rw [← not_iff_not]
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
a : α
S S' : Set σ
⊢ ¬Disjoint S (M.reverse.stepSet S' a) ↔ ¬Disjoint S' (M.stepSet S a)
have simp : (∃ x ∈ S, ∃ t ∈ S', t ∈ M.step x a) ↔ ∃ x ∈ S', ∃ t ∈ S, x ∈ M.step t a
Tactic: simp only [Set.not_disjoint_iff, mem_stepSet, reverse_step, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
a : α
S S' : Set σ
⊢ (∃ x ∈ S, ∃ t ∈ S', t ∈ M.step x a) ↔ ∃ x ∈ S', ∃ t ∈ S, x ∈ M.step t a
have mp : (∃ x ∈ S, ∃ t ∈ S', t ∈ M.step x a) → ∃ x ∈ S', ∃ t ∈ S, x ∈ M.step t a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ (∃ x ∈ S, ∃ t ∈ S', t ∈ M.step x a) ↔ ∃ x ∈ S', ∃ t ∈ S, x ∈ M.step t a
have mpr : (∃ x ∈ S', ∃ t ∈ S, x ∈ M.step t a) → ∃ x ∈ S, ∃ t ∈ S', t ∈ M.step x a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ (∃ x ∈ S, ∃ t ∈ S', t ∈ M.step x a) ↔ ∃ x ∈ S', ∃ t ∈ S, x ∈ M.step t a
have mp₁ : ∀ w ∈ S, ∀ w_1 ∈ S', w_1 ∈ M.step w a → ∃ x ∈ S', ∃ t ∈ S, x ∈ M.step t a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ (∃ x ∈ S, ∃ t ∈ S', t ∈ M.step x a) ↔ ∃ x ∈ S', ∃ t ∈ S, x ∈ M.step t a
have mpr₁ : ∀ w ∈ S', ∀ w_1 ∈ S, w ∈ M.step w_1 a → ∃ x ∈ S, ∃ t ∈ S', t ∈ M.step x a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ (∃ x ∈ S, ∃ t ∈ S', t ∈ M.step x a) ↔ ∃ x ∈ S', ∃ t ∈ S, x ∈ M.step t a
have mp₉ : ∀ w ∈ S, ∀ w_1 ∈ S', w_1 ∈ M.step w a → w_1 ∈ S' ∧ ∃ t ∈ S, w_1 ∈ M.step t a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ (∃ x ∈ S, ∃ t ∈ S', t ∈ M.step x a) ↔ ∃ x ∈ S', ∃ t ∈ S, x ∈ M.step t a
have mp₁₀ : (w : σ) → w ∈ S → (w_1 : σ) → w_1 ∈ S' → w_1 ∈ M.step w a → σ
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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 → σ
⊢ (∃ x ∈ S, ∃ t ∈ S', t ∈ M.step x a) ↔ ∃ x ∈ S', ∃ t ∈ S, x ∈ M.step t a
have mp₁₃ : ∀ w ∈ S, ∀ w_1 ∈ S', w_1 ∈ M.step w a → w_1 ∈ S'
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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'
⊢ (∃ x ∈ S, ∃ t ∈ S', t ∈ M.step x a) ↔ ∃ x ∈ S', ∃ t ∈ S, x ∈ M.step t a
have mp₁₄ : ∀ w ∈ S, ∀ w_1 ∈ S', w_1 ∈ M.step w a → ∃ t ∈ S, w_1 ∈ M.step t a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ (∃ x ∈ S, ∃ t ∈ S', t ∈ M.step x a) ↔ ∃ x ∈ S', ∃ t ∈ S, x ∈ M.step t a
have mpr₉ : ∀ w ∈ S', ∀ w_1 ∈ S, w ∈ M.step w_1 a → w_1 ∈ S ∧ ∃ t ∈ S', t ∈ M.step w_1 a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ (∃ x ∈ S, ∃ t ∈ S', t ∈ M.step x a) ↔ ∃ x ∈ S', ∃ t ∈ S, x ∈ M.step t a
have mpr₁₀ : (w : σ) → w ∈ S' → (w_1 : σ) → w_1 ∈ S → w ∈ M.step w_1 a → σ
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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 → σ
⊢ (∃ x ∈ S, ∃ t ∈ S', t ∈ M.step x a) ↔ ∃ x ∈ S', ∃ t ∈ S, x ∈ M.step t a
have mpr₁₃ : ∀ w ∈ S', ∀ w_1 ∈ S, w ∈ M.step w_1 a → w_1 ∈ S
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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
⊢ (∃ x ∈ S, ∃ t ∈ S', t ∈ M.step x a) ↔ ∃ x ∈ S', ∃ t ∈ S, x ∈ M.step t a
have mpr₁₄ : ∀ w ∈ S', ∀ w_1 ∈ S, w ∈ M.step w_1 a → ∃ t ∈ S', t ∈ M.step w_1 a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
x : List α
S S' : Set σ
h : Disjoint S (M.reverse.evalFrom S' x)
⊢ Disjoint S' (M.evalFrom S x.reverse)
have simp : Disjoint S' (List.foldr (fun (x : α) (y : Set σ) ↦ M.stepSet y x) S x)
Tactic: simp only [evalFrom, List.foldl_reverse] at h ⊢
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
Goal:
α : Type u
σ : Type v
M : NFA α σ
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 [])
have nil : Disjoint (List.foldr (fun (x : α) (y : Set σ) ↦ M.stepSet y x) S []) S'
Tactic: rw [disjoint_comm]
-- Lean 4 proof step from Mathlib.Computability.NFA (hypothesis)
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.foldr (fun (x : α) (y : Set σ) ↦ M.stepSet y x) S (x :: xs))
have h₁ : Disjoint S (List.foldl M.reverse.stepSet (M.reverse.stepSet S' x) xs)
Tactic: rw [List.foldl_cons] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.NFA (goal)
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 S' (List.foldr (fun (x : α) (y : Set σ) ↦ M.stepSet y x) S (x :: xs))
have cons : Disjoint (M.reverse.stepSet S' x) (List.foldr (fun (x : α) (y : Set σ) ↦ M.stepSet y x) S xs)
Tactic: rw [List.foldr_cons, ← NFA.disjoint_stepSet_reverse, disjoint_comm]