awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.Encoding (goal)
Goal:
m : PosNum
hm : decodePosNum (encodePosNum m) = m
⊢ (if encodePosNum m = [] then PosNum.one else (decodePosNum (encodePosNum m)).bit1) = m.bit1
have bit1 : (if encodePosNum m = [] then PosNum.one else m.bit1) = m.bit1
Tactic: rw [hm]
-- Lean 4 proof step from Mathlib.Computability.Encoding (goal)
Goal:
n : PosNum
⊢ decodePosNum (encodePosNum n) = n
have one : decodePosNum (encodePosNum PosNum.one) = PosNum.one
Tactic: induction n with unfold encodePosNum decodePosNum
  | one => rfl
  | bit1 m hm =>
    rw [hm]
    exact if_neg (encodePosNum_nonempty m)
  | bit0 m hm => exact congr_arg PosNum.bit0 hm
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Encoding (goal)
Goal:
n : PosNum
one : decodePosNum (encodePosNum PosNum.one) = PosNum.one
⊢ decodePosNum (encodePosNum n) = n
have one₁ : (if Eq (α := List Bool) [] [] then PosNum.one else (decodePosNum []).bit1) = PosNum.one
Tactic: induction n with unfold encodePosNum decodePosNum
  | one => rfl
  | bit1 m hm =>
    rw [hm]
    exact if_neg (encodePosNum_nonempty m)
  | bit0 m hm => exact congr_arg PosNum.bit0 hm
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Encoding (goal)
Goal:
n : PosNum
one : decodePosNum (encodePosNum PosNum.one) = PosNum.one
one₁ : (if Eq (α := List Bool) [] [] then PosNum.one else (decodePosNum []).bit1) = PosNum.one
⊢ decodePosNum (encodePosNum n) = n
have bit1 : ∀ (m : PosNum) (hm : decodePosNum (encodePosNum m) = m), decodePosNum (encodePosNum m.bit1) = m.bit1
Tactic: induction n with unfold encodePosNum decodePosNum
  | one => rfl
  | bit1 m hm =>
    rw [hm]
    exact if_neg (encodePosNum_nonempty m)
  | bit0 m hm => exact congr_arg PosNum.bit0 hm
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Encoding (goal)
Goal:
n : PosNum
one : decodePosNum (encodePosNum PosNum.one) = PosNum.one
one₁ : (if Eq (α := List Bool) [] [] then PosNum.one else (decodePosNum []).bit1) = PosNum.one
bit1 : ∀ (m : PosNum) (hm : decodePosNum (encodePosNum m) = m), decodePosNum (encodePosNum m.bit1) = m.bit1
⊢ decodePosNum (encodePosNum n) = n
have bit1₁ : ∀ (m : PosNum) (hm : decodePosNum (encodePosNum m) = m),
  (if encodePosNum m = [] then PosNum.one else (decodePosNum (encodePosNum m)).bit1) = m.bit1
Tactic: induction n with unfold encodePosNum decodePosNum
  | one => rfl
  | bit1 m hm =>
    rw [hm]
    exact if_neg (encodePosNum_nonempty m)
  | bit0 m hm => exact congr_arg PosNum.bit0 hm
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Encoding (goal)
Goal:
n : PosNum
one : decodePosNum (encodePosNum PosNum.one) = PosNum.one
one₁ : (if Eq (α := List Bool) [] [] then PosNum.one else (decodePosNum []).bit1) = PosNum.one
bit1 : ∀ (m : PosNum) (hm : decodePosNum (encodePosNum m) = m), decodePosNum (encodePosNum m.bit1) = m.bit1
bit1₁ :
  ∀ (m : PosNum) (hm : decodePosNum (encodePosNum m) = m),
    (if encodePosNum m = [] then PosNum.one else (decodePosNum (encodePosNum m)).bit1) = m.bit1
⊢ decodePosNum (encodePosNum n) = n
have bit0 : ∀ (m : PosNum) (hm : decodePosNum (encodePosNum m) = m), decodePosNum (encodePosNum m.bit0) = m.bit0
Tactic: induction n with unfold encodePosNum decodePosNum
  | one => rfl
  | bit1 m hm =>
    rw [hm]
    exact if_neg (encodePosNum_nonempty m)
  | bit0 m hm => exact congr_arg PosNum.bit0 hm
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Encoding (goal)
Goal:
n : PosNum
one : decodePosNum (encodePosNum PosNum.one) = PosNum.one
one₁ : (if Eq (α := List Bool) [] [] then PosNum.one else (decodePosNum []).bit1) = PosNum.one
bit1 : ∀ (m : PosNum) (hm : decodePosNum (encodePosNum m) = m), decodePosNum (encodePosNum m.bit1) = m.bit1
bit1₁ :
  ∀ (m : PosNum) (hm : decodePosNum (encodePosNum m) = m),
    (if encodePosNum m = [] then PosNum.one else (decodePosNum (encodePosNum m)).bit1) = m.bit1
bit0 : ∀ (m : PosNum) (hm : decodePosNum (encodePosNum m) = m), decodePosNum (encodePosNum m.bit0) = m.bit0
⊢ decodePosNum (encodePosNum n) = n
have bit0₁ : ∀ (m : PosNum) (hm : decodePosNum (encodePosNum m) = m), (decodePosNum (encodePosNum m)).bit0 = m.bit0
Tactic: induction n with unfold encodePosNum decodePosNum
  | one => rfl
  | bit1 m hm =>
    rw [hm]
    exact if_neg (encodePosNum_nonempty m)
  | bit0 m hm => exact congr_arg PosNum.bit0 hm
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Encoding (goal)
Goal:
n : Num
⊢ decodeNum (encodeNum n) = n
have zero : decodeNum (encodeNum Num.zero) = Num.zero
Tactic: obtain - | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Encoding (goal)
Goal:
n : Num
zero : decodeNum (encodeNum Num.zero) = Num.zero
⊢ decodeNum (encodeNum n) = n
have pos : ∀ (n : PosNum), decodeNum (encodeNum (Num.pos n)) = Num.pos n
Tactic: obtain - | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Encoding (goal)
Goal:
n : PosNum
⊢ (if
        Eq (α := List Bool)
          (match (motive := Num → List Bool) Num.pos n with
            | Num.zero => []
            | Num.pos n => encodePosNum n :
            List Bool)
          ([] : List Bool) then
      Num.zero
    else
      (↑(decodePosNum
            (match (motive := Num → List Bool) Num.pos n with
            | Num.zero => []
            | Num.pos n => encodePosNum n)) :
        Num)) =
    Num.pos n
have pos : (if
      Eq (α := List Bool)
        (match (motive := Num → List Bool) Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n :
          List Bool)
        ([] : List Bool) then
    Num.zero
  else (↑n : Num)) =
  Num.pos n
Tactic: rw [decode_encodePosNum n]
-- Lean 4 proof step from Mathlib.Computability.Encoding (goal)
Goal:
n : PosNum
⊢ (if
        Eq (α := List Bool)
          (match (motive := Num → List Bool) Num.pos n with
            | Num.zero => []
            | Num.pos n => encodePosNum n :
            List Bool)
          ([] : List Bool) then
      Num.zero
    else (↑n : Num)) =
    Num.pos n
have pos : (if
      Eq (α := List Bool)
        (match (motive := Num → List Bool) Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n :
          List Bool)
        ([] : List Bool) then
    Num.zero
  else Num.pos n) =
  Num.pos n
Tactic: rw [PosNum.cast_to_num]
-- Lean 4 proof step from Mathlib.Computability.Encoding (goal)
Goal:
n : ℕ
| n
have rw : (↑(↑n : Num) : ℕ)
Tactic: rw [← Num.to_of_nat n]
-- Lean 4 proof step from Mathlib.Computability.Encoding (goal)
Goal:
n : ℕ
⊢ decodeNat (encodeNat n) = n
have conv_rhs : decodeNat (encodeNat n) = (↑(↑n : Num) : ℕ)
Tactic: conv_rhs => rw [← Num.to_of_nat n]
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s : σ
hs : s ∈ M.εClosure ∅
⊢ False
have base : ∀ (s : σ), Membership.mem (γ := Set σ) ∅ s → False
Tactic: induction hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
s : σ
hs : s ∈ M.εClosure ∅
base : ∀ (s : σ), Membership.mem (γ := Set σ) ∅ s → False
⊢ False
have step : ∀ (s t : σ), t ∈ M.step s none → M.εClosure ∅ s → False → False
Tactic: induction hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s s_1 : σ
h : s_1 ∈ S
⊢ ∃ t ∈ S, s_1 ∈ M.εClosure {t}
have base : s_1 ∈ S ∧ s_1 ∈ M.εClosure {s_1}
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s s_1 t : σ
h : t ∈ M.step s_1 none
h_1 : M.εClosure S s_1
ih : ∃ t ∈ S, s_1 ∈ M.εClosure {t}
⊢ ∃ t_1 ∈ S, t ∈ M.εClosure {t_1}
have step : ∀ s ∈ S, s_1 ∈ M.εClosure {s} → ∃ t_1 ∈ S, t ∈ M.εClosure {t_1}
Tactic: obtain ⟨s, _, _⟩ := ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s_1 s_2 t : σ
h : t ∈ M.step s_2 none
h_1 : M.εClosure S s_2
s : σ
left : s ∈ S
right : s_2 ∈ M.εClosure {s}
⊢ ∃ t_1 ∈ S, t ∈ M.εClosure {t_1}
have h : s ∈ S ∧ t ∈ M.εClosure {s}
Tactic: use s
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s : σ
h : s ∈ M.εClosure S
⊢ ∃ t ∈ S, s ∈ M.εClosure {t}
have base : ∀ s ∈ S, ∃ t ∈ S, s ∈ M.εClosure {t}
Tactic: induction h with
    | base => tauto
    | step _ _ _ _ ih =>
      obtain ⟨s, _, _⟩ := ih
      use s
      solve_by_elim [εClosure.step]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s : σ
h : s ∈ M.εClosure S
base : ∀ s ∈ S, ∃ t ∈ S, s ∈ M.εClosure {t}
⊢ ∃ t ∈ S, s ∈ M.εClosure {t}
have step : ∀ (s t : σ), t ∈ M.step s none → M.εClosure S s → ∀ (ih : ∃ t ∈ S, s ∈ M.εClosure {t}), ∃ t_1 ∈ S, t ∈ M.εClosure {t_1}
Tactic: induction h with
    | base => tauto
    | step _ _ _ _ ih =>
      obtain ⟨s, _, _⟩ := ih
      use s
      solve_by_elim [εClosure.step]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s t : σ
left : t ∈ S
h : s ∈ M.εClosure {t}
⊢ s ∈ M.εClosure S
have base : ∀ (s : σ), Membership.mem (γ := Set σ) {t} s → s ∈ M.εClosure S
Tactic: induction h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s t : σ
left : t ∈ S
h : s ∈ M.εClosure {t}
base : ∀ (s : σ), Membership.mem (γ := Set σ) {t} s → s ∈ M.εClosure S
⊢ s ∈ M.εClosure S
have step : ∀ (s t_1 : σ), t_1 ∈ M.step s none → M.εClosure {t} s → s ∈ M.εClosure S → t_1 ∈ M.εClosure S
Tactic: induction h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (hypothesis)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s t : σ
left : t ∈ S
s_1 : σ
h : Membership.mem (γ := Set σ) {t} s_1
⊢ s_1 ∈ M.εClosure S
have left : s_1 ∈ S
Tactic: subst_vars
Cleared hypotheses: t, left, h
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s : σ
a : α
⊢ s ∈ M.stepSet S a ↔ ∃ t ∈ S, s ∈ M.εClosure (M.step t (some a))
have simp_rw : Membership.mem (γ := Set σ) (⋃ s ∈ S, M.εClosure (M.step s (some a))) s ↔ ∃ t ∈ S, s ∈ M.εClosure (M.step t (some a))
Tactic: simp_rw [stepSet, mem_iUnion₂, exists_prop]
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
s : σ
a : α
simp_rw :
  Membership.mem (γ := Set σ) (⋃ s ∈ S, M.εClosure (M.step s (some a))) s ↔ ∃ t ∈ S, s ∈ M.εClosure (M.step t (some a))
⊢ s ∈ M.stepSet S a ↔ ∃ t ∈ S, s ∈ M.εClosure (M.step t (some a))
have simp_rw₁ : (∃ (i : σ) (_ : i ∈ S), s ∈ M.εClosure (M.step i (some a))) ↔ ∃ t ∈ S, s ∈ M.εClosure (M.step t (some a))
Tactic: simp_rw [stepSet, mem_iUnion₂, exists_prop]
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
a : α
⊢ M.stepSet ∅ a = ∅
have simp_rw : Eq.{v + 1} (α := Set σ) (⋃ (s : σ), ⋃ (_ : Membership.mem (γ := Set σ) ∅ s), M.εClosure (M.step s (some a))) ∅
Tactic: simp_rw [stepSet, mem_empty_iff_false, iUnion_false, iUnion_empty]
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
a : α
simp_rw : Eq.{v + 1} (α := Set σ) (⋃ (s : σ), ⋃ (_ : Membership.mem (γ := Set σ) ∅ s), M.εClosure (M.step s (some a))) ∅
⊢ M.stepSet ∅ a = ∅
have simp_rw₁ : Eq.{v + 1} (α := Set σ) (⋃ (s : σ), ⋃ (_ : False), M.εClosure (M.step s (some a))) ∅
Tactic: simp_rw [stepSet, mem_empty_iff_false, iUnion_false, iUnion_empty]
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
a : α
simp_rw : Eq.{v + 1} (α := Set σ) (⋃ (s : σ), ⋃ (_ : Membership.mem (γ := Set σ) ∅ s), M.εClosure (M.step s (some a))) ∅
simp_rw₁ : Eq.{v + 1} (α := Set σ) (⋃ (s : σ), ⋃ (_ : False), M.εClosure (M.step s (some a))) ∅
⊢ M.stepSet ∅ a = ∅
have simp_rw₂ : Eq.{v + 1} (α := Set σ) (⋃ (s : σ), ∅) ∅
Tactic: simp_rw [stepSet, mem_empty_iff_false, iUnion_false, iUnion_empty]
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
x : List α
a : α
⊢ M.evalFrom S (x ++ [a]) = M.stepSet (M.evalFrom S x) a
have rw : List.foldl M.stepSet (M.εClosure S) (x ++ [a]) = M.stepSet (List.foldl M.stepSet (M.εClosure S) x) a
Tactic: rw [evalFrom, List.foldl_append, List.foldl_cons, List.foldl_nil]
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
x : List α
a : α
rw : List.foldl M.stepSet (M.εClosure S) (x ++ [a]) = M.stepSet (List.foldl M.stepSet (M.εClosure S) x) a
⊢ M.evalFrom S (x ++ [a]) = M.stepSet (M.evalFrom S x) a
have rw₁ : List.foldl M.stepSet (List.foldl M.stepSet (M.εClosure S) x) [a] = M.stepSet (List.foldl M.stepSet (M.εClosure S) x) a
Tactic: rw [evalFrom, List.foldl_append, List.foldl_cons, List.foldl_nil]
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
x : List α
a : α
rw : List.foldl M.stepSet (M.εClosure S) (x ++ [a]) = M.stepSet (List.foldl M.stepSet (M.εClosure S) x) a
rw₁ :
  List.foldl M.stepSet (List.foldl M.stepSet (M.εClosure S) x) [a] = M.stepSet (List.foldl M.stepSet (M.εClosure S) x) a
⊢ M.evalFrom S (x ++ [a]) = M.stepSet (M.evalFrom S x) a
have rw₂ : List.foldl M.stepSet (M.stepSet (List.foldl M.stepSet (M.εClosure S) x) a) [] =
  M.stepSet (List.foldl M.stepSet (M.εClosure S) x) a
Tactic: rw [evalFrom, List.foldl_append, List.foldl_cons, List.foldl_nil]
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
x : List α
a : α
rw : List.foldl M.stepSet (M.εClosure S) (x ++ [a]) = M.stepSet (List.foldl M.stepSet (M.εClosure S) x) a
rw₁ :
  List.foldl M.stepSet (List.foldl M.stepSet (M.εClosure S) x) [a] = M.stepSet (List.foldl M.stepSet (M.εClosure S) x) a
rw₂ :
  List.foldl M.stepSet (M.stepSet (List.foldl M.stepSet (M.εClosure S) x) a) [] =
    M.stepSet (List.foldl M.stepSet (M.εClosure S) x) a
⊢ M.evalFrom S (x ++ [a]) = M.stepSet (M.evalFrom S x) a
have rw₃ : M.stepSet (List.foldl M.stepSet (M.εClosure S) x) a = M.stepSet (List.foldl M.stepSet (M.εClosure S) x) a
Tactic: rw [evalFrom, List.foldl_append, List.foldl_cons, List.foldl_nil]
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
⊢ M.evalFrom ∅ [] = ∅
have nil : M.εClosure ∅ = ∅
Tactic: rw [evalFrom_nil, εClosure_empty]
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
nil : M.εClosure ∅ = ∅
⊢ M.evalFrom ∅ [] = ∅
have nil₁ : Eq.{v + 1} (α := Set σ) ∅ ∅
Tactic: rw [evalFrom_nil, εClosure_empty]
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
x : List α
a : α
ih : M.evalFrom ∅ x = ∅
⊢ M.evalFrom ∅ (x ++ [a]) = ∅
have append_singleton : M.stepSet (M.evalFrom ∅ x) a = ∅
Tactic: rw [evalFrom_append_singleton, ih, stepSet_empty]
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
x : List α
a : α
ih : M.evalFrom ∅ x = ∅
append_singleton : M.stepSet (M.evalFrom ∅ x) a = ∅
⊢ M.evalFrom ∅ (x ++ [a]) = ∅
have append_singleton₁ : M.stepSet ∅ a = ∅
Tactic: rw [evalFrom_append_singleton, ih, stepSet_empty]
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
x : List α
a : α
ih : M.evalFrom ∅ x = ∅
append_singleton : M.stepSet (M.evalFrom ∅ x) a = ∅
append_singleton₁ : M.stepSet ∅ a = ∅
⊢ M.evalFrom ∅ (x ++ [a]) = ∅
have append_singleton₂ : Eq.{v + 1} (α := Set σ) ∅ ∅
Tactic: rw [evalFrom_append_singleton, ih, stepSet_empty]
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
x : List α
⊢ M.evalFrom ∅ x = ∅
have nil : M.evalFrom ∅ [] = ∅
Tactic: induction x using List.reverseRecOn with
  | nil => rw [evalFrom_nil, εClosure_empty]
  | append_singleton x a ih => rw [evalFrom_append_singleton, ih, stepSet_empty]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
x : List α
nil : M.evalFrom ∅ [] = ∅
⊢ M.evalFrom ∅ x = ∅
have append_singleton : ∀ (x : List α) (a : α) (ih : M.evalFrom ∅ x = ∅), M.evalFrom ∅ (x ++ [a]) = ∅
Tactic: induction x using List.reverseRecOn with
  | nil => rw [evalFrom_nil, εClosure_empty]
  | append_singleton x a ih => rw [evalFrom_append_singleton, ih, stepSet_empty]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
l : List α
a : α
ih : ∀ {s : σ}, s ∈ M.evalFrom S l ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} l
s : σ
⊢ s ∈ M.evalFrom S (l ++ [a]) ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} (l ++ [a])
have append_singleton : (∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))) ↔
  ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
Tactic: simp_rw [evalFrom_append_singleton, mem_stepSet_iff, ih]
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
l : List α
a : α
ih : ∀ {s : σ}, s ∈ M.evalFrom S l ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} l
s : σ
⊢ (∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))) ↔
    ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
have append_singleton : (∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))) →
  ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
l : List α
a : α
ih : ∀ {s : σ}, s ∈ M.evalFrom S l ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} l
s : σ
append_singleton :
  (∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))) →
    ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
⊢ (∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))) ↔
    ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
have append_singleton₁ : (∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))) →
  ∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
l : List α
a : α
ih : ∀ {s : σ}, s ∈ M.evalFrom S l ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} l
s : σ
append_singleton :
  (∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))) →
    ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
append_singleton₁ :
  (∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))) →
    ∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))
⊢ (∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))) ↔
    ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
have append_singleton₂ : ∀ (w : σ),
  s ∈ M.εClosure (M.step w (some a)) →
    ∀ w_1 ∈ S, w ∈ M.evalFrom {w_1} l → ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
l : List α
a : α
ih : ∀ {s : σ}, s ∈ M.evalFrom S l ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} l
s : σ
append_singleton :
  (∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))) →
    ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
append_singleton₁ :
  (∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))) →
    ∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))
append_singleton₂ append_singleton₃ append_singleton₄ :
  ∀ (w : σ),
    s ∈ M.εClosure (M.step w (some a)) →
      ∀ w_1 ∈ S, w ∈ M.evalFrom {w_1} l → ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
⊢ (∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))) ↔
    ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
have append_singleton₅ : ∀ w ∈ S,
  ∀ w_1 ∈ M.evalFrom {w} l,
    s ∈ M.εClosure (M.step w_1 (some a)) →
      ∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
l : List α
a : α
ih : ∀ {s : σ}, s ∈ M.evalFrom S l ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} l
s : σ
append_singleton :
  (∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))) →
    ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
append_singleton₁ :
  (∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))) →
    ∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))
append_singleton₂ append_singleton₃ append_singleton₄ :
  ∀ (w : σ),
    s ∈ M.εClosure (M.step w (some a)) →
      ∀ w_1 ∈ S, w ∈ M.evalFrom {w_1} l → ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
append_singleton₅ append_singleton₆ append_singleton₇ :
  ∀ w ∈ S,
    ∀ w_1 ∈ M.evalFrom {w} l,
      s ∈ M.εClosure (M.step w_1 (some a)) →
        ∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))
append_singleton₈ append_singleton₉ append_singleton₁₀ :
  ∀ (w : σ),
    s ∈ M.εClosure (M.step w (some a)) →
      ∀ w_1 ∈ S, w ∈ M.evalFrom {w_1} l → ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
append_singleton₁₁ append_singleton₁₂ append_singleton₁₃ :
  ∀ w ∈ S,
    ∀ w_1 ∈ M.evalFrom {w} l,
      s ∈ M.εClosure (M.step w_1 (some a)) →
        ∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))
append_singleton₁₄ append_singleton₁₅ :
  ∀ (w : σ),
    s ∈ M.εClosure (M.step w (some a)) →
      ∀ w_1 ∈ S, w ∈ M.evalFrom {w_1} l → ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
⊢ (∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))) ↔
    ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
have append_singleton₁₆ : ∀ (w : σ),
  s ∈ M.εClosure (M.step w (some a)) →
    ∀ w_1 ∈ S, w ∈ M.evalFrom {w_1} l → w_1 ∈ S ∧ ∃ t ∈ M.evalFrom {w_1} l, s ∈ M.εClosure (M.step t (some a))
Tactic: tauto