awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Fintype Γ
inst_1 : Inhabited Λ
S : Finset Λ
ss : Supports M S
q_1 : Λ' Γ Λ σ
h : q_1 ∈ trSupp M S
a : Γ → σ → σ
q : Stmt Γ Λ σ
hs : SupportsStmt S (Stmt.load a q)
hw : ∀ q' ∈ writes q, q' ∈ trSupp M S
IH : SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.load a q)) ∧
    ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
exact ⟨supportsStmt_read _ fun _ ↦ IH.1, IH.2⟩
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Fintype Γ
inst_1 : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ :
  ∀ (hs : SupportsStmt S q₁) (hw : ∀ q' ∈ writes q₁, q' ∈ trSupp M S),
    SupportsStmt (trSupp M S) (trNormal dec q₁) ∧ ∀ q' ∈ writes q₁, SupportsStmt (trSupp M S) (tr enc dec M q')
IH₂ :
  ∀ (hs : SupportsStmt S q₂) (hw : ∀ q' ∈ writes q₂, q' ∈ trSupp M S),
    SupportsStmt (trSupp M S) (trNormal dec q₂) ∧ ∀ q' ∈ writes q₂, SupportsStmt (trSupp M S) (tr enc dec M q')
hs : SupportsStmt S (Stmt.branch p q₁ q₂)
hw : ∀ q' ∈ writes (Stmt.branch p q₁ q₂), q' ∈ trSupp M S
⊢ ∀ q' ∈ writes q₁ ∪ writes q₂, q' ∈ trSupp M S

Tactic:
unfold writes at hw ⊢

Premises used: Turing.TM1to1.writes
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Fintype Γ
inst_1 : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ :
  ∀ (hs : SupportsStmt S q₁) (hw : ∀ q' ∈ writes q₁, q' ∈ trSupp M S),
    SupportsStmt (trSupp M S) (trNormal dec q₁) ∧ ∀ q' ∈ writes q₁, SupportsStmt (trSupp M S) (tr enc dec M q')
IH₂ :
  ∀ (hs : SupportsStmt S q₂) (hw : ∀ q' ∈ writes q₂, q' ∈ trSupp M S),
    SupportsStmt (trSupp M S) (trNormal dec q₂) ∧ ∀ q' ∈ writes q₂, SupportsStmt (trSupp M S) (tr enc dec M q')
hs : SupportsStmt S (Stmt.branch p q₁ q₂)
hw : ∀ q' ∈ writes q₁ ∪ writes q₂, q' ∈ trSupp M S
branch :
  ∀ (hw : ∀ (q' : Λ' Γ Λ σ), q' ∈ writes q₁ ∨ q' ∈ writes q₂ → q' ∈ trSupp M S),
    SupportsStmt (trSupp M S) (trNormal dec (Stmt.branch p q₁ q₂)) ∧
      ∀ (q' : Λ' Γ Λ σ), q' ∈ writes q₁ ∨ q' ∈ writes q₂ → SupportsStmt (trSupp M S) (tr enc dec M q')
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.branch p q₁ q₂)) ∧
    ∀ q' ∈ writes q₁ ∪ writes q₂, SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
simp only [Finset.mem_union] at hw ⊢

Premises used: Finset.mem_union
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Fintype Γ
inst_1 : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ :
  ∀ (hs : SupportsStmt S q₁) (hw : ∀ q' ∈ writes q₁, q' ∈ trSupp M S),
    SupportsStmt (trSupp M S) (trNormal dec q₁) ∧ ∀ q' ∈ writes q₁, SupportsStmt (trSupp M S) (tr enc dec M q')
IH₂ :
  ∀ (hs : SupportsStmt S q₂) (hw : ∀ q' ∈ writes q₂, q' ∈ trSupp M S),
    SupportsStmt (trSupp M S) (trNormal dec q₂) ∧ ∀ q' ∈ writes q₂, SupportsStmt (trSupp M S) (tr enc dec M q')
hs : SupportsStmt S (Stmt.branch p q₁ q₂)
hw : ∀ (q' : Λ' Γ Λ σ), q' ∈ writes q₁ ∨ q' ∈ writes q₂ → q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec q₁) ∧ ∀ q' ∈ writes q₁, SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
replace IH₁ := IH₁ hs.1 fun q hq ↦ hw q (Or.inl hq)
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Fintype Γ
inst_1 : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₂ :
  ∀ (hs : SupportsStmt S q₂) (hw : ∀ q' ∈ writes q₂, q' ∈ trSupp M S),
    SupportsStmt (trSupp M S) (trNormal dec q₂) ∧ ∀ q' ∈ writes q₂, SupportsStmt (trSupp M S) (tr enc dec M q')
hs : SupportsStmt S (Stmt.branch p q₁ q₂)
hw : ∀ (q' : Λ' Γ Λ σ), q' ∈ writes q₁ ∨ q' ∈ writes q₂ → q' ∈ trSupp M S
IH₁ : SupportsStmt (trSupp M S) (trNormal dec q₁) ∧ ∀ q' ∈ writes q₁, SupportsStmt (trSupp M S) (tr enc dec M q')
⊢ SupportsStmt (trSupp M S) (trNormal dec q₂) ∧ ∀ q' ∈ writes q₂, SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
replace IH₂ := IH₂ hs.2 fun q hq ↦ hw q (Or.inr hq)
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Fintype Γ
inst_1 : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
hs : SupportsStmt S (Stmt.branch p q₁ q₂)
hw : ∀ (q' : Λ' Γ Λ σ), q' ∈ writes q₁ ∨ q' ∈ writes q₂ → q' ∈ trSupp M S
IH₁ : SupportsStmt (trSupp M S) (trNormal dec q₁) ∧ ∀ q' ∈ writes q₁, SupportsStmt (trSupp M S) (tr enc dec M q')
IH₂ : SupportsStmt (trSupp M S) (trNormal dec q₂) ∧ ∀ q' ∈ writes q₂, SupportsStmt (trSupp M S) (tr enc dec M q')
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.branch p q₁ q₂)) ∧
    ∀ (q' : Λ' Γ Λ σ), q' ∈ writes q₁ ∨ q' ∈ writes q₂ → SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
⟨supportsStmt_read _ fun _ ↦ ⟨IH₁.1, IH₂.1⟩, fun q ↦ Or.rec (IH₁.2 _) (IH₂.2 _)⟩

Premises used: Or.rec, Turing.TM1to1.supportsStmt_read, And.left, And.intro
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Fintype Γ
inst_1 : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
hs : SupportsStmt S (Stmt.branch p q₁ q₂)
hw : ∀ (q' : Λ' Γ Λ σ), q' ∈ writes q₁ ∨ q' ∈ writes q₂ → q' ∈ trSupp M S
IH₁ : SupportsStmt (trSupp M S) (trNormal dec q₁) ∧ ∀ q' ∈ writes q₁, SupportsStmt (trSupp M S) (tr enc dec M q')
IH₂ : SupportsStmt (trSupp M S) (trNormal dec q₂) ∧ ∀ q' ∈ writes q₂, SupportsStmt (trSupp M S) (tr enc dec M q')
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.branch p q₁ q₂)) ∧
    ∀ (q' : Λ' Γ Λ σ), q' ∈ writes q₁ ∨ q' ∈ writes q₂ → SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
exact ⟨supportsStmt_read _ fun _ ↦ ⟨IH₁.1, IH₂.1⟩, fun q ↦ Or.rec (IH₁.2 _) (IH₂.2 _)⟩
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Fintype Γ
inst_1 : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
l : Γ → σ → Λ
hs : SupportsStmt S (Stmt.goto l)
hw : ∀ q' ∈ writes (Stmt.goto l), q' ∈ trSupp M S
goto :
  SupportsStmt (trSupp M S) (trNormal dec (Stmt.goto l)) ∧
    ∀ (q' : Λ' Γ Λ σ), False → SupportsStmt (trSupp M S) (tr enc dec M q')
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.goto l)) ∧
    ∀ q' ∈ writes (Stmt.goto l), SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
simp only [writes, Finset.notMem_empty]

Premises used: Turing.TM1to1.writes, Finset.notMem_empty
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Fintype Γ
inst_1 : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
l : Γ → σ → Λ
hs : SupportsStmt S (Stmt.goto l)
hw : ∀ q' ∈ writes (Stmt.goto l), q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.goto l)) ∧
    ∀ (q' : Λ' Γ Λ σ), False → SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
⟨?_, fun _ ↦ False.elim⟩

Premises used: False.elim, And.intro
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Fintype Γ
inst_1 : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
l : Γ → σ → Λ
hs : SupportsStmt S (Stmt.goto l)
hw : ∀ q' ∈ writes (Stmt.goto l), q' ∈ trSupp M S
goto : SupportsStmt (trSupp M S) (trNormal dec (Stmt.goto l))
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.goto l)) ∧
    ∀ (q' : Λ' Γ Λ σ), False → SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
refine ⟨?_, fun _ ↦ False.elim⟩
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Fintype Γ
inst_1 : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
l : Γ → σ → Λ
hs : SupportsStmt S (Stmt.goto l)
hw : ∀ q' ∈ writes (Stmt.goto l), q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.goto l))

Tactic:
supportsStmt_read _ fun a _ s ↦ ?_

Premises used: Turing.TM1to1.supportsStmt_read, Turing.TM1to1.trNormal
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Fintype Γ
inst_1 : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
l : Γ → σ → Λ
hs : SupportsStmt S (Stmt.goto l)
hw : ∀ q' ∈ writes (Stmt.goto l), q' ∈ trSupp M S
goto : ∀ (a : Γ) (x : Bool) (s : σ), (fun (x : Bool) (s : σ) ↦ (Λ'.normal (l a s) : Λ' Γ Λ σ)) x s ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.goto l))

Tactic:
refine supportsStmt_read _ fun a _ s ↦ ?_
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Fintype Γ
inst_1 : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
l : Γ → σ → Λ
hs : SupportsStmt S (Stmt.goto l)
hw : ∀ q' ∈ writes (Stmt.goto l), q' ∈ trSupp M S
a : Γ
x : Bool
s : σ
⊢ (fun (x : Bool) (s : σ) ↦ (Λ'.normal (l a s) : Λ' Γ Λ σ)) x s ∈ trSupp M S

Tactic:
Finset.mem_biUnion.2 ⟨_, hs _ _, Finset.mem_insert_self _ _⟩

Premises used: Iff.mpr, Finset.mem_insert_self, Set.Mem, setOf, And.intro, Exists.intro, Finset.mem_biUnion
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Fintype Γ
inst_1 : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
l : Γ → σ → Λ
hs : SupportsStmt S (Stmt.goto l)
hw : ∀ q' ∈ writes (Stmt.goto l), q' ∈ trSupp M S
a : Γ
x : Bool
s : σ
⊢ (fun (x : Bool) (s : σ) ↦ (Λ'.normal (l a s) : Λ' Γ Λ σ)) x s ∈ trSupp M S

Tactic:
exact Finset.mem_biUnion.2 ⟨_, hs _ _, Finset.mem_insert_self _ _⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Finset.mem_biUnion
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Fintype Γ
inst_1 : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
hs : SupportsStmt.{u_1, u_2, u_3} (Γ := Γ) (σ := σ) S Stmt.halt
hw : ∀ (q' : Λ' Γ Λ σ), Membership.mem (γ := Finset (Λ' Γ Λ σ)) (writes Stmt.halt) q' → q' ∈ trSupp M S
halt :
  SupportsStmt (trSupp M S) (trNormal dec Stmt.halt) ∧
    ∀ (q' : Λ' Γ Λ σ), False → SupportsStmt (trSupp M S) (tr enc dec M q')
⊢ SupportsStmt (trSupp M S) (trNormal dec Stmt.halt) ∧
    ∀ (q' : Λ' Γ Λ σ),
      Membership.mem (γ := Finset (Λ' Γ Λ σ)) (writes Stmt.halt) q' → SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
simp only [writes, Finset.notMem_empty]

Premises used: Turing.TM1to1.writes, Finset.notMem_empty
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Fintype Γ
inst_1 : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
hs : SupportsStmt.{u_1, u_2, u_3} (Γ := Γ) (σ := σ) S Stmt.halt
hw : ∀ (q' : Λ' Γ Λ σ), Membership.mem (γ := Finset (Λ' Γ Λ σ)) (writes Stmt.halt) q' → q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec Stmt.halt) ∧
    ∀ (q' : Λ' Γ Λ σ), False → SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
⟨?_, fun _ ↦ False.elim⟩

Premises used: False.elim, And.intro
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Fintype Γ
inst_1 : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
hs : SupportsStmt.{u_1, u_2, u_3} (Γ := Γ) (σ := σ) S Stmt.halt
hw : ∀ (q' : Λ' Γ Λ σ), Membership.mem (γ := Finset (Λ' Γ Λ σ)) (writes Stmt.halt) q' → q' ∈ trSupp M S
halt : SupportsStmt (trSupp M S) (trNormal dec Stmt.halt)
⊢ SupportsStmt (trSupp M S) (trNormal dec Stmt.halt) ∧
    ∀ (q' : Λ' Γ Λ σ), False → SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
refine ⟨?_, fun _ ↦ False.elim⟩
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst : Fintype Γ
inst_1 : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
hs : SupportsStmt.{u_1, u_2, u_3} (Γ := Γ) (σ := σ) S Stmt.halt
hw : ∀ (q' : Λ' Γ Λ σ), Membership.mem (γ := Finset (Λ' Γ Λ σ)) (writes Stmt.halt) q' → q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec Stmt.halt)

Tactic:
simp only [SupportsStmt, trNormal]

Premises used: Turing.TM1to1.trNormal, Turing.TM1.SupportsStmt
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
inst : Inhabited Γ
Λ : Type u_2
inst_1 : Inhabited Λ
M : TM0.Machine Γ Λ
x : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
none :
  ∀ (e : M q T.head = Option.none),
    FRespects (TM1.step (tr M)) (trCfg M) (trCfg M { q := q, Tape := T : TM0.Cfg Γ Λ })
      (TM0.step M { q := q, Tape := T : TM0.Cfg Γ Λ })
some :
  ∀ (val : Prod.{u_2, u_1} Λ (TM0.Stmt Γ)) (e : M q T.head = Option.some val),
    FRespects (TM1.step (tr M)) (trCfg M) (trCfg M { q := q, Tape := T : TM0.Cfg Γ Λ })
      (TM0.step M { q := q, Tape := T : TM0.Cfg Γ Λ })
⊢ FRespects (TM1.step (tr M)) (trCfg M) (trCfg M { q := q, Tape := T : TM0.Cfg Γ Λ })
    (TM0.step M { q := q, Tape := T : TM0.Cfg Γ Λ })

Tactic:
rcases e : M q T.1 with - | val

Premises used: Turing.Tape.head
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
inst : Inhabited Γ
Λ : Type u_2
inst_1 : Inhabited Λ
M : TM0.Machine Γ Λ
x : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
e : M q T.head = Option.none
none :
  FRespects (TM1.step (tr M)) (trCfg M)
    { l := bif Option.isSome (α := Prod.{u_2, u_1} Λ (TM0.Stmt Γ)) Option.none then some (Λ'.normal q) else Option.none,
      var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit }
    (Option.map
      (fun (x : Prod.{u_2, u_1} Λ (TM0.Stmt Γ)) ↦
        { q := x.1,
          Tape :=
            match (motive := TM0.Stmt Γ → Tape Γ) x.2 with
            | TM0.Stmt.move d => Tape.move d T
            | TM0.Stmt.write a => Tape.write a T })
      Option.none)
⊢ FRespects (TM1.step (tr M)) (trCfg M) (trCfg M { q := q, Tape := T : TM0.Cfg Γ Λ })
    (TM0.step M { q := q, Tape := T : TM0.Cfg Γ Λ })

Tactic:
simp only [TM0.step, trCfg, e]

Premises used: Turing.TM0.step, Turing.TM0to1.trCfg
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
inst : Inhabited Γ
Λ : Type u_2
inst_1 : Inhabited Λ
M : TM0.Machine Γ Λ
x : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
e : M q T.head = none
⊢ FRespects (TM1.step (tr M)) (trCfg M)
    { l := bif Option.isSome (α := Prod.{u_2, u_1} Λ (TM0.Stmt Γ)) none then some (Λ'.normal q) else none, var := (),
      Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit }
    (Option.map
      (fun (x : Prod.{u_2, u_1} Λ (TM0.Stmt Γ)) ↦
        { q := x.1,
          Tape :=
            match (motive := TM0.Stmt Γ → Tape Γ) x.2 with
            | TM0.Stmt.move d => Tape.move d T
            | TM0.Stmt.write a => Tape.write a T })
      none)

Tactic:
Eq.refl none

Premises used: Turing.TM1.step, Option.none, Eq.refl, StateTransition.FRespects
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
inst : Inhabited Γ
Λ : Type u_2
inst_1 : Inhabited Λ
M : TM0.Machine Γ Λ
x : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
e : M q T.head = none
⊢ FRespects (TM1.step (tr M)) (trCfg M)
    { l := bif Option.isSome (α := Prod.{u_2, u_1} Λ (TM0.Stmt Γ)) none then some (Λ'.normal q) else none, var := (),
      Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit }
    (Option.map
      (fun (x : Prod.{u_2, u_1} Λ (TM0.Stmt Γ)) ↦
        { q := x.1,
          Tape :=
            match (motive := TM0.Stmt Γ → Tape Γ) x.2 with
            | TM0.Stmt.move d => Tape.move d T
            | TM0.Stmt.write a => Tape.write a T })
      none)

Tactic:
exact Eq.refl none

Premises used: Option.none, Eq.refl
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
inst : Inhabited Γ
Λ : Type u_2
inst_1 : Inhabited Λ
M : TM0.Machine Γ Λ
x : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
val : Prod.{u_2, u_1} Λ (TM0.Stmt Γ)
e : M q T.head = Option.some val
some :
  ∀ (q' : Λ) (s : TM0.Stmt Γ) (e : M q T.head = Option.some (q', s)),
    FRespects (TM1.step (tr M)) (trCfg M) (trCfg M { q := q, Tape := T : TM0.Cfg Γ Λ })
      (TM0.step M { q := q, Tape := T : TM0.Cfg Γ Λ })
⊢ FRespects (TM1.step (tr M)) (trCfg M) (trCfg M { q := q, Tape := T : TM0.Cfg Γ Λ })
    (TM0.step M { q := q, Tape := T : TM0.Cfg Γ Λ })

Tactic:
obtain ⟨q', s⟩ := val
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
inst : Inhabited Γ
Λ : Type u_2
inst_1 : Inhabited Λ
M : TM0.Machine Γ Λ
x : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
s : TM0.Stmt Γ
e : M q T.head = Option.some (q', s)
some :
  Reaches₁ (TM1.step (tr M)) { l := Option.some (Λ'.normal q), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit }
    {
      l :=
        match (motive := Bool → Option (Λ' Γ Λ))
          match (motive := Option (Prod.{u_2, u_1} Λ (TM0.Stmt Γ)) → Bool)
            M q'
              (Tape.head
                (match (motive := TM0.Stmt Γ → Tape Γ) s with
                | TM0.Stmt.move d => Tape.move d T
                | TM0.Stmt.write a => Tape.write a T)) with
          | Option.some val => true
          | none => false with
        | true => Option.some (Λ'.normal q')
        | false => none,
      var := (),
      Tape :=
        match (motive := TM0.Stmt Γ → Tape Γ) s with
        | TM0.Stmt.move d => Tape.move d T
        | TM0.Stmt.write a => Tape.write a T }
⊢ FRespects (TM1.step (tr M)) (trCfg M) (trCfg M { q := q, Tape := T : TM0.Cfg Γ Λ })
    (TM0.step M { q := q, Tape := T : TM0.Cfg Γ Λ })

Tactic:
simp only [FRespects, TM0.step, trCfg, e, Option.isSome, cond, Option.map_some]

Premises used: cond, Turing.TM0.step, Turing.TM0to1.trCfg, Option.map_some, StateTransition.FRespects, Option.isSome
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
inst : Inhabited Γ
Λ : Type u_2
inst_1 : Inhabited Λ
M : TM0.Machine Γ Λ
x : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
s : TM0.Stmt Γ
e : M q T.head = Option.some (q', s)
some :
  ∀ (e : M q T.head = Option.some (q', s)),
    Reaches₁ (TM1.step (tr M)) { l := Option.some (Λ'.normal q), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit }
      {
        l :=
          match (motive := Bool → Option (Λ' Γ Λ))
            match (motive := Option (Prod.{u_2, u_1} Λ (TM0.Stmt Γ)) → Bool)
              M q'
                (Tape.head
                  (match (motive := TM0.Stmt Γ → Tape Γ) s with
                  | TM0.Stmt.move d => Tape.move d T
                  | TM0.Stmt.write a => Tape.write a T)) with
            | Option.some val => true
            | none => false with
          | true => Option.some (Λ'.normal q')
          | false => none,
        var := (),
        Tape :=
          match (motive := TM0.Stmt Γ → Tape Γ) s with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }
⊢ Reaches₁ (TM1.step (tr M)) { l := Option.some (Λ'.normal q), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit }
    {
      l :=
        match (motive := Bool → Option (Λ' Γ Λ))
          match (motive := Option (Prod.{u_2, u_1} Λ (TM0.Stmt Γ)) → Bool)
            M q'
              (Tape.head
                (match (motive := TM0.Stmt Γ → Tape Γ) s with
                | TM0.Stmt.move d => Tape.move d T
                | TM0.Stmt.write a => Tape.write a T)) with
          | Option.some val => true
          | none => false with
        | true => Option.some (Λ'.normal q')
        | false => none,
      var := (),
      Tape :=
        match (motive := TM0.Stmt Γ → Tape Γ) s with
        | TM0.Stmt.move d => Tape.move d T
        | TM0.Stmt.write a => Tape.write a T }

Tactic:
revert e
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
inst : Inhabited Γ
Λ : Type u_2
inst_1 : Inhabited Λ
M : TM0.Machine Γ Λ
x : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
s : TM0.Stmt Γ
move :
  ∀ (a : Dir),
    TM1.step (tr M) { l := some (Λ'.act (TM0.Stmt.move a) q'), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit } =
      some
        { l := some (Λ'.normal q'), var := (),
          Tape :=
            match (motive := TM0.Stmt Γ → Tape Γ) TM0.Stmt.move a with
            | TM0.Stmt.move d => Tape.move d T
            | TM0.Stmt.write a => Tape.write a T }
write :
  ∀ (a : Γ),
    TM1.step (tr M) { l := some (Λ'.act (TM0.Stmt.write a) q'), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit } =
      some
        { l := some (Λ'.normal q'), var := (),
          Tape :=
            match (motive := TM0.Stmt Γ → Tape Γ) TM0.Stmt.write a with
            | TM0.Stmt.move d => Tape.move d T
            | TM0.Stmt.write a => Tape.write a T }
⊢ TM1.step (tr M) { l := some (Λ'.act s q'), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit } =
    some
      { l := some (Λ'.normal q'), var := (),
        Tape :=
          match (motive := TM0.Stmt Γ → Tape Γ) s with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }

Tactic:
cases s
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
inst : Inhabited Γ
Λ : Type u_2
inst_1 : Inhabited Λ
M : TM0.Machine Γ Λ
x : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
a : Dir
⊢ TM1.step (tr M) { l := some (Λ'.act (TM0.Stmt.move a) q'), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit } =
    some
      { l := some (Λ'.normal q'), var := (),
        Tape :=
          match (motive := TM0.Stmt Γ → Tape Γ) TM0.Stmt.move a with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
inst : Inhabited Γ
Λ : Type u_2
inst_1 : Inhabited Λ
M : TM0.Machine Γ Λ
x : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
a : Γ
⊢ TM1.step (tr M) { l := some (Λ'.act (TM0.Stmt.write a) q'), var := (), Tape := T : TM1.Cfg Γ (Λ' Γ Λ) Unit } =
    some
      { l := some (Λ'.normal q'), var := (),
        Tape :=
          match (motive := TM0.Stmt Γ → Tape Γ) TM0.Stmt.write a with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }

Tactic:
rfl