awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
M : Λ → Stmt Γ Λ σ
S : Finset Λ
q₁ q₂ : Stmt Γ Λ σ
h₁ : q₁ ∈ stmts₁ q₂
simp : ∀ x ∈ S, q₂ ∈ stmts₁ (M x) → ∃ a ∈ S, q₁ ∈ stmts₁ (M a)
⊢ some q₂ ∈ stmts M S → some q₁ ∈ stmts M S

Tactic:
simp only [stmts, Finset.mem_insertNone, Finset.mem_biUnion, Option.mem_def, Option.some.injEq,
    forall_eq', exists_imp, and_imp]

Premises used: and_imp, Option.some.injEq, forall_eq', Turing.TM1.stmts, exists_imp, Finset.mem_biUnion, Option.mem_def, Finset.mem_insertNone
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
M : Λ → Stmt Γ Λ σ
S : Finset Λ
q₁ q₂ : Stmt Γ Λ σ
h₁ : q₁ ∈ stmts₁ q₂
⊢ ∀ x ∈ S, q₂ ∈ stmts₁ (M x) → ∃ a ∈ S, q₁ ∈ stmts₁ (M a)

Tactic:
fun l ls h₂ ↦ ⟨_, ls, stmts₁_trans h₂ h₁⟩

Premises used: Turing.TM1.stmts₁_trans, And.intro, Exists.intro
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
M : Λ → Stmt Γ Λ σ
S : Finset Λ
q₁ q₂ : Stmt Γ Λ σ
h₁ : q₁ ∈ stmts₁ q₂
⊢ ∀ x ∈ S, q₂ ∈ stmts₁ (M x) → ∃ a ∈ S, q₁ ∈ stmts₁ (M a)

Tactic:
exact fun l ls h₂ ↦ ⟨_, ls, stmts₁_trans h₂ h₁⟩
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst : Inhabited Λ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
q : Stmt Γ Λ σ
ss : Supports M S
simp : ∀ x ∈ S, q ∈ stmts₁ (M x) → SupportsStmt S q
⊢ some q ∈ stmts M S → SupportsStmt S q

Tactic:
simp only [stmts, Finset.mem_insertNone, Finset.mem_biUnion, Option.mem_def, Option.some.injEq,
    forall_eq', exists_imp, and_imp]

Premises used: and_imp, Option.some.injEq, forall_eq', Turing.TM1.stmts, exists_imp, Finset.mem_biUnion, Option.mem_def, Finset.mem_insertNone
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst : Inhabited Λ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
q : Stmt Γ Λ σ
ss : Supports M S
⊢ ∀ x ∈ S, q ∈ stmts₁ (M x) → SupportsStmt S q

Tactic:
fun l ls h ↦ stmts₁_supportsStmt_mono h (ss.2 _ ls)

Premises used: Turing.TM1.stmts₁_supportsStmt_mono, And.right
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst : Inhabited Λ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
q : Stmt Γ Λ σ
ss : Supports M S
⊢ ∀ x ∈ S, q ∈ stmts₁ (M x) → SupportsStmt S q

Tactic:
exact fun l ls h ↦ stmts₁_supportsStmt_mono h (ss.2 _ ls)

Premises used: Turing.TM1.stmts₁_supportsStmt_mono, And.right
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst : Inhabited Λ
inst_1 : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
v : σ
T : Tape Γ
c' : Cfg Γ Λ σ
h₁ : c' ∈ step M { l := some l₁, var := v, Tape := T : Cfg Γ Λ σ }
h₂ :
  Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    { l := some l₁, var := v, Tape := T : Cfg Γ Λ σ }.l
⊢ SupportsStmt S (M l₁)

Tactic:
replace h₂ := ss.2 _ (Finset.some_mem_insertNone.1 h₂)
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst : Inhabited Λ
inst_1 : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
v : σ
T : Tape Γ
c' : Cfg Γ Λ σ
h₁ : c' ∈ step M { l := some l₁, var := v, Tape := T : Cfg Γ Λ σ }
h₂ : SupportsStmt S (M l₁)
⊢ stepAux (M l₁) v T = c'

Tactic:
simp only [step, Option.mem_def, Option.some.injEq] at h₁

Premises used: Turing.TM1.step, Option.some.injEq, Option.mem_def
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst : Inhabited Λ
inst_1 : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
v : σ
T : Tape Γ
c' : Cfg Γ Λ σ
h₂ : SupportsStmt S (M l₁)
h₁ : stepAux (M l₁) v T = c'
subst :
  Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux (M l₁) v T).l
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) c'.l

Tactic:
subst c'
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst : Inhabited Λ
inst_1 : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
v : σ
T : Tape Γ
h₂ : SupportsStmt S (M l₁)
revert :
  ∀ (h₂ : SupportsStmt S (M l₁)),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux (M l₁) v T).l
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux (M l₁) v T).l

Tactic:
revert h₂
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst : Inhabited Λ
inst_1 : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
p : Γ → σ → Bool
q₁' q₂' : Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : Tape Γ) (h₂ : SupportsStmt S q₁'),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux q₁' v T).l
IH₂ :
  ∀ (v : σ) (T : Tape Γ) (h₂ : SupportsStmt S q₂'),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux q₂' v T).l
v : σ
T : Tape Γ
hs : SupportsStmt S (Stmt.branch p q₁' q₂')
branch :
  Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    (bif false then stepAux q₁' v T else stepAux q₂' v T).l
branch₁ :
  Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    (bif true then stepAux q₁' v T else stepAux q₂' v T).l
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    (bif p T.head v then stepAux q₁' v T else stepAux q₂' v T).l

Tactic:
cases p T.1 v

Premises used: Turing.Tape.head
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst : Inhabited Λ
inst_1 : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
p : Γ → σ → Bool
q₁' q₂' : Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : Tape Γ) (h₂ : SupportsStmt S q₁'),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux q₁' v T).l
IH₂ :
  ∀ (v : σ) (T : Tape Γ) (h₂ : SupportsStmt S q₂'),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux q₂' v T).l
v : σ
T : Tape Γ
hs : SupportsStmt S (branch p q₁' q₂')
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    (bif false then stepAux q₁' v T else stepAux q₂' v T).l

Tactic:
IH₂ _ _ hs.2

Premises used: cond, Set.Mem, setOf, And.right
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst : Inhabited Λ
inst_1 : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
p : Γ → σ → Bool
q₁' q₂' : Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : Tape Γ) (h₂ : SupportsStmt S q₁'),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux q₁' v T).l
IH₂ :
  ∀ (v : σ) (T : Tape Γ) (h₂ : SupportsStmt S q₂'),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux q₂' v T).l
v : σ
T : Tape Γ
hs : SupportsStmt S (branch p q₁' q₂')
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    (bif false then stepAux q₁' v T else stepAux q₂' v T).l

Tactic:
exact IH₂ _ _ hs.2

Premises used: And.right
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst : Inhabited Λ
inst_1 : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
p : Γ → σ → Bool
q₁' q₂' : Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : Tape Γ) (h₂ : SupportsStmt S q₁'),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux q₁' v T).l
IH₂ :
  ∀ (v : σ) (T : Tape Γ) (h₂ : SupportsStmt S q₂'),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux q₂' v T).l
v : σ
T : Tape Γ
hs : SupportsStmt S (branch p q₁' q₂')
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    (bif true then stepAux q₁' v T else stepAux q₂' v T).l

Tactic:
IH₁ _ _ hs.1

Premises used: cond, Set.Mem, setOf, And.left
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst : Inhabited Λ
inst_1 : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
p : Γ → σ → Bool
q₁' q₂' : Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (T : Tape Γ) (h₂ : SupportsStmt S q₁'),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux q₁' v T).l
IH₂ :
  ∀ (v : σ) (T : Tape Γ) (h₂ : SupportsStmt S q₂'),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux q₂' v T).l
v : σ
T : Tape Γ
hs : SupportsStmt S (branch p q₁' q₂')
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ))
    (bif true then stepAux q₁' v T else stepAux q₂' v T).l

Tactic:
exact IH₁ _ _ hs.1

Premises used: And.left
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst : Inhabited Λ
inst_1 : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
a : Γ → σ → Λ
v : σ
T : Tape Γ
hs : SupportsStmt S (goto a)
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux (goto a) v T).l

Tactic:
Finset.some_mem_insertNone.2 (hs _ _)

Premises used: Iff.mpr, Set.Mem, setOf, Finset.some_mem_insertNone
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst : Inhabited Λ
inst_1 : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
a : Γ → σ → Λ
v : σ
T : Tape Γ
hs : SupportsStmt S (goto a)
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux (goto a) v T).l

Tactic:
exact Finset.some_mem_insertNone.2 (hs _ _)

Premises used: Iff.mpr, Finset.some_mem_insertNone
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst : Inhabited Λ
inst_1 : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
v : σ
T : Tape Γ
hs : SupportsStmt.{u_1, u_2, u_3} (Γ := Γ) (σ := σ) S halt
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (Cfg.l (stepAux halt v T))

Tactic:
apply Multiset.mem_cons_self

Premises used: Multiset.mem_cons_self
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst : Inhabited Λ
inst_1 : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
a : Dir
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (T : Tape Γ) (h₂ : SupportsStmt S q),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux q v T).l
v : σ
T : Tape Γ
hs : SupportsStmt S (move a q)
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux (move a q) v T).l

Tactic:
IH _ _ hs

Premises used: Set.Mem, setOf
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst : Inhabited Λ
inst_1 : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
a : Dir
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (T : Tape Γ) (h₂ : SupportsStmt S q),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux q v T).l
v : σ
T : Tape Γ
hs : SupportsStmt S (move a q)
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux (move a q) v T).l

Tactic:
exact IH _ _ hs
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst : Inhabited Λ
inst_1 : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
a : Γ → σ → Γ
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (T : Tape Γ) (h₂ : SupportsStmt S q),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux q v T).l
v : σ
T : Tape Γ
hs : SupportsStmt S (write a q)
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux (write a q) v T).l

Tactic:
IH _ _ hs

Premises used: Set.Mem, setOf
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst : Inhabited Λ
inst_1 : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
a : Γ → σ → Γ
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (T : Tape Γ) (h₂ : SupportsStmt S q),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux q v T).l
v : σ
T : Tape Γ
hs : SupportsStmt S (write a q)
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux (write a q) v T).l

Tactic:
exact IH _ _ hs
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst : Inhabited Λ
inst_1 : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
a : Γ → σ → σ
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (T : Tape Γ) (h₂ : SupportsStmt S q),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux q v T).l
v : σ
T : Tape Γ
hs : SupportsStmt S (load a q)
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux (load a q) v T).l

Tactic:
IH _ _ hs

Premises used: Set.Mem, setOf
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst : Inhabited Λ
inst_1 : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
a : Γ → σ → σ
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (T : Tape Γ) (h₂ : SupportsStmt S q),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux q v T).l
v : σ
T : Tape Γ
hs : SupportsStmt S (load a q)
⊢ Membership.mem (γ := Finset (Option Λ))
    ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux (load a q) v T).l

Tactic:
exact IH _ _ hs
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst : Inhabited Λ
inst_1 : Inhabited Γ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
ss : Supports M S
l₁ : Λ
v : σ
T : Tape Γ
induction :
  ∀ (x : Stmt Γ Λ σ) (h₂ : SupportsStmt S x),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux x v T).l
⊢ ∀ (h₂ : SupportsStmt S (M l₁)),
    Membership.mem (γ := Finset (Option Λ))
      ((Finset.insertNone : (a : Finset Λ) → Finset (Option Λ)) S : Finset (Option Λ)) (stepAux (M l₁) v T).l

Tactic:
induction M l₁ generalizing v T with intro hs
    | branch p q₁' q₂' IH₁ IH₂ =>
      unfold stepAux; cases p T.1 v
      · exact IH₂ _ _ hs.2
      · exact IH₁ _ _ hs.1
    | goto => exact Finset.some_mem_insertNone.2 (hs _ _)
    | halt => apply Multiset.mem_cons_self
    | _ _ q IH => exact IH _ _ hs

Premises used: Turing.TM1.stepAux, Turing.TM1.Stmt.halt, Turing.TM1.Stmt.goto, Multiset.mem_cons_self, Turing.TM1.Stmt.branch
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
inst : Inhabited Λ
σ : Type u_3
inst_1 : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst_2 : Inhabited Γ
x : TM1.Cfg Γ Λ σ
l₁ : Option Λ
v : σ
T : Tape Γ
none :
  FRespects (TM0.step (tr M)) (trCfg M) (trCfg M { l := Option.none, var := v, Tape := T : TM1.Cfg Γ Λ σ })
    (TM1.step M { l := Option.none, var := v, Tape := T : TM1.Cfg Γ Λ σ })
some :
  ∀ (l₁ : Λ),
    FRespects (TM0.step (tr M)) (trCfg M) (trCfg M { l := Option.some l₁, var := v, Tape := T : TM1.Cfg Γ Λ σ })
      (TM1.step M { l := Option.some l₁, var := v, Tape := T : TM1.Cfg Γ Λ σ })
⊢ FRespects (TM0.step (tr M)) (trCfg M) (trCfg M { l := l₁, var := v, Tape := T : TM1.Cfg Γ Λ σ })
    (TM1.step M { l := l₁, var := v, Tape := T : TM1.Cfg Γ Λ σ })

Tactic:
rcases l₁ with - | l₁
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
inst : Inhabited Λ
σ : Type u_3
inst_1 : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst_2 : Inhabited Γ
x : TM1.Cfg Γ Λ σ
v : σ
T : Tape Γ
⊢ FRespects (TM0.step (tr M)) (trCfg M) (trCfg M { l := none, var := v, Tape := T : TM1.Cfg Γ Λ σ })
    (TM1.step M { l := none, var := v, Tape := T : TM1.Cfg Γ Λ σ })

Tactic:
rfl

Premises used: Turing.TM0.step, StateTransition.FRespects, rfl
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
inst : Inhabited Λ
σ : Type u_3
inst_1 : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst_2 : Inhabited Γ
x : TM1.Cfg Γ Λ σ
v : σ
T : Tape Γ
⊢ FRespects (TM0.step (tr M)) (trCfg M) (trCfg M { l := none, var := v, Tape := T : TM1.Cfg Γ Λ σ })
    (TM1.step M { l := none, var := v, Tape := T : TM1.Cfg Γ Λ σ })

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
inst : Inhabited Λ
σ : Type u_3
inst_1 : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst_2 : Inhabited Γ
x : TM1.Cfg Γ Λ σ
v : σ
T : Tape Γ
l₁ : Λ
some :
  Reaches₁ (TM0.step (tr M)) { q := (Option.some (M l₁), v), Tape := T : TM0.Cfg Γ (Λ' M) }
    {
      q :=
        (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ)) (TM1.stepAux (M l₁) v T).l with
          | Option.some x => Option.some (M x)
          | none => none,
          (TM1.stepAux (M l₁) v T).var),
      Tape := (TM1.stepAux (M l₁) v T).Tape }
⊢ FRespects (TM0.step (tr M)) (trCfg M) (trCfg M { l := Option.some l₁, var := v, Tape := T : TM1.Cfg Γ Λ σ })
    (TM1.step M { l := Option.some l₁, var := v, Tape := T : TM1.Cfg Γ Λ σ })

Tactic:
simp only [trCfg, TM1.step, FRespects, Option.map]

Premises used: Turing.TM1.step, Turing.TM1to0.trCfg, Option.map, StateTransition.FRespects
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
inst : Inhabited Λ
σ : Type u_3
inst_1 : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst_2 : Inhabited Γ
x : TM1.Cfg Γ Λ σ
l₁ : Λ
a : Dir
a_1 : TM1.Stmt Γ Λ σ
IH :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a_1, v), Tape := T : TM0.Cfg Γ (Λ' M) }
      {
        q :=
          (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ)) (TM1.stepAux a_1 v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a_1 v T).var),
        Tape := (TM1.stepAux a_1 v T).Tape }
v : σ
T : Tape Γ
⊢ Reaches₁ (TM0.step (tr M)) { q := (some (TM1.Stmt.move a a_1), v), Tape := T : TM0.Cfg Γ (Λ' M) }
    {
      q :=
        (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ)) (TM1.stepAux (TM1.Stmt.move a a_1) v T).l with
          | some x => some (M x)
          | none => none,
          (TM1.stepAux (TM1.Stmt.move a a_1) v T).var),
      Tape := (TM1.stepAux (TM1.Stmt.move a a_1) v T).Tape }

Tactic:
TransGen.head rfl (IH _ _)

Premises used: Relation.TransGen.head, StateTransition.Reaches₁, rfl
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
inst : Inhabited Λ
σ : Type u_3
inst_1 : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst_2 : Inhabited Γ
x : TM1.Cfg Γ Λ σ
l₁ : Λ
a : Dir
a_1 : TM1.Stmt Γ Λ σ
IH :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a_1, v), Tape := T : TM0.Cfg Γ (Λ' M) }
      {
        q :=
          (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ)) (TM1.stepAux a_1 v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a_1 v T).var),
        Tape := (TM1.stepAux a_1 v T).Tape }
v : σ
T : Tape Γ
⊢ Reaches₁ (TM0.step (tr M)) { q := (some (TM1.Stmt.move a a_1), v), Tape := T : TM0.Cfg Γ (Λ' M) }
    {
      q :=
        (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ)) (TM1.stepAux (TM1.Stmt.move a a_1) v T).l with
          | some x => some (M x)
          | none => none,
          (TM1.stepAux (TM1.Stmt.move a a_1) v T).var),
      Tape := (TM1.stepAux (TM1.Stmt.move a a_1) v T).Tape }

Tactic:
exact TransGen.head rfl (IH _ _)
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
inst : Inhabited Λ
σ : Type u_3
inst_1 : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst_2 : Inhabited Γ
x : TM1.Cfg Γ Λ σ
l₁ : Λ
a : Γ → σ → Γ
a_1 : TM1.Stmt Γ Λ σ
IH :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a_1, v), Tape := T : TM0.Cfg Γ (Λ' M) }
      {
        q :=
          (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ)) (TM1.stepAux a_1 v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a_1 v T).var),
        Tape := (TM1.stepAux a_1 v T).Tape }
v : σ
T : Tape Γ
⊢ Reaches₁ (TM0.step (tr M)) { q := (some (TM1.Stmt.write a a_1), v), Tape := T : TM0.Cfg Γ (Λ' M) }
    {
      q :=
        (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ)) (TM1.stepAux (TM1.Stmt.write a a_1) v T).l with
          | some x => some (M x)
          | none => none,
          (TM1.stepAux (TM1.Stmt.write a a_1) v T).var),
      Tape := (TM1.stepAux (TM1.Stmt.write a a_1) v T).Tape }

Tactic:
TransGen.head rfl (IH _ _)

Premises used: Relation.TransGen.head, StateTransition.Reaches₁, rfl
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
inst : Inhabited Λ
σ : Type u_3
inst_1 : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst_2 : Inhabited Γ
x : TM1.Cfg Γ Λ σ
l₁ : Λ
a : Γ → σ → Γ
a_1 : TM1.Stmt Γ Λ σ
IH :
  ∀ (v : σ) (T : Tape Γ),
    Reaches₁ (TM0.step (tr M)) { q := (some a_1, v), Tape := T : TM0.Cfg Γ (Λ' M) }
      {
        q :=
          (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ)) (TM1.stepAux a_1 v T).l with
            | some x => some (M x)
            | none => none,
            (TM1.stepAux a_1 v T).var),
        Tape := (TM1.stepAux a_1 v T).Tape }
v : σ
T : Tape Γ
⊢ Reaches₁ (TM0.step (tr M)) { q := (some (TM1.Stmt.write a a_1), v), Tape := T : TM0.Cfg Γ (Λ' M) }
    {
      q :=
        (match (motive := Option Λ → Option (TM1.Stmt Γ Λ σ)) (TM1.stepAux (TM1.Stmt.write a a_1) v T).l with
          | some x => some (M x)
          | none => none,
          (TM1.stepAux (TM1.Stmt.write a a_1) v T).var),
      Tape := (TM1.stepAux (TM1.Stmt.write a a_1) v T).Tape }

Tactic:
exact TransGen.head rfl (IH _ _)