awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (hypothesis)
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
f : Γ → σ → Γ
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.write f q)
hw : ∀ (q' : Λ' Γ Λ σ), (∃ (a : Γ), Λ'.write a q = q') ∨ q' ∈ writes q → q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.write f q)) ∧
    ∀ (q' : Λ' Γ Λ σ), (∃ (a : Γ), Λ'.write a q = q') ∨ q' ∈ writes q → SupportsStmt (trSupp M S) (tr enc dec M q')
have IH₁ : SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
Tactic: replace IH := IH hs fun q hq ↦ hw q (Or.inr hq)
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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
f : Γ → σ → Γ
q : Stmt Γ Λ σ
hs : SupportsStmt S (Stmt.write f q)
hw : ∀ (q' : Λ' Γ Λ σ), (∃ (a : Γ), Λ'.write a q = 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 (Stmt.write f q)) ∧
    ∀ (q' : Λ' Γ Λ σ), (∃ (a : Γ), Λ'.write a q = q') ∨ q' ∈ writes q → SupportsStmt (trSupp M S) (tr enc dec M q')
have write : ∀ (q' : Λ' Γ Λ σ) (hq : (∃ (a : Γ), Λ'.write a q = q') ∨ q' ∈ writes q), SupportsStmt (trSupp M S) (tr enc dec M q')
Tactic: refine ⟨supportsStmt_read _ fun a _ s ↦ hw _ (Or.inl ⟨_, rfl⟩), fun q' hq ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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
f : Γ → σ → Γ
q : Stmt Γ Λ σ
hs : SupportsStmt S (Stmt.write f q)
hw : ∀ (q' : Λ' Γ Λ σ), (∃ (a : Γ), Λ'.write a q = 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')
q' : Λ' Γ Λ σ
hq : (∃ (a : Γ), Λ'.write a q = q') ∨ q' ∈ writes q
⊢ SupportsStmt (trSupp M S) (tr enc dec M q')
have write : ∀ (a : Γ), SupportsStmt (trSupp M S) (tr enc dec M (Λ'.write a q))
Tactic: rcases hq with (⟨a, q₂, rfl⟩ | hq)
Cleared hypotheses: q', hq
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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
f : Γ → σ → Γ
q : Stmt Γ Λ σ
hs : SupportsStmt S (Stmt.write f q)
hw : ∀ (q' : Λ' Γ Λ σ), (∃ (a : Γ), Λ'.write a q = 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')
q' : Λ' Γ Λ σ
hq : (∃ (a : Γ), Λ'.write a q = q') ∨ q' ∈ writes q
write : ∀ (a : Γ), SupportsStmt (trSupp M S) (tr enc dec M (Λ'.write a q))
⊢ SupportsStmt (trSupp M S) (tr enc dec M q')
have write₁ : ∀ (hq : q' ∈ writes q), SupportsStmt (trSupp M S) (tr enc dec M q')
Tactic: rcases hq with (⟨a, q₂, rfl⟩ | hq)
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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 Γ Λ σ
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.load a q)
hw : ∀ q' ∈ writes (Stmt.load a q), q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.load a q)) ∧
    ∀ q' ∈ writes (Stmt.load a q), SupportsStmt (trSupp M S) (tr enc dec M q')
have load : ∀ (hw : ∀ q' ∈ writes q, q' ∈ trSupp M S),
  SupportsStmt (trSupp M S) (trNormal dec (Stmt.load a q)) ∧
    ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
Tactic: unfold writes at hw ⊢
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (hypothesis)
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 Γ Λ σ
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.load a q)
hw : ∀ q' ∈ writes q, q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.load a q)) ∧
    ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
have IH₁ : SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
Tactic: replace IH := IH hs hw
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (hypothesis)
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
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.branch p q₁ q₂)) ∧
    ∀ q' ∈ writes (Stmt.branch p q₁ q₂), SupportsStmt (trSupp M S) (tr enc dec M q')
have hw₁ : ∀ q' ∈ writes q₁ ∪ writes q₂, q' ∈ trSupp M S
Tactic: unfold writes at hw ⊢
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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
⊢ 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')
have 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')
Tactic: simp only [Finset.mem_union] at hw ⊢
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (hypothesis)
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 (Stmt.branch p q₁ q₂)) ∧
    ∀ (q' : Λ' Γ Λ σ), q' ∈ writes q₁ ∨ q' ∈ writes q₂ → SupportsStmt (trSupp M S) (tr enc dec M q')
have IH₃ : 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)
Cleared hypotheses: IH₁
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (hypothesis)
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 (Stmt.branch p q₁ q₂)) ∧
    ∀ (q' : Λ' Γ Λ σ), q' ∈ writes q₁ ∨ q' ∈ writes q₂ → SupportsStmt (trSupp M S) (tr enc dec M q')
have IH₃ : 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)
Cleared hypotheses: IH₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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' ∈ writes (Stmt.goto l), SupportsStmt (trSupp M S) (tr enc dec M q')
have goto : SupportsStmt (trSupp M S) (trNormal dec (Stmt.goto l)) ∧
  ∀ (q' : Λ' Γ Λ σ), False → SupportsStmt (trSupp M S) (tr enc dec M q')
Tactic: simp only [writes, Finset.notMem_empty]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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')
have goto : SupportsStmt (trSupp M S) (trNormal dec (Stmt.goto l))
Tactic: refine ⟨?_, fun _ ↦ False.elim⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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))
have goto : ∀ (a : Γ) (x : Bool) (s : σ), (fun (x : Bool) (s : σ) ↦ (Λ'.normal (l a s) : Λ' Γ Λ σ)) x s ∈ trSupp M S
Tactic: refine supportsStmt_read _ fun a _ s ↦ ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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' : Λ' Γ Λ σ),
      Membership.mem (γ := Finset (Λ' Γ Λ σ)) (writes Stmt.halt) q' → SupportsStmt (trSupp M S) (tr enc dec M q')
have halt : SupportsStmt (trSupp M S) (trNormal dec Stmt.halt) ∧
  ∀ (q' : Λ' Γ Λ σ), False → SupportsStmt (trSupp M S) (tr enc dec M q')
Tactic: simp only [writes, Finset.notMem_empty]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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')
have halt : SupportsStmt (trSupp M S) (trNormal dec Stmt.halt)
Tactic: refine ⟨?_, fun _ ↦ False.elim⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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
q : Stmt Γ Λ σ
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')
have move : ∀ (d : Dir) (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.move d q)) (hw : ∀ q' ∈ writes (Stmt.move d q), q' ∈ trSupp M S),
  SupportsStmt (trSupp M S) (trNormal dec (Stmt.move d q)) ∧
    ∀ q' ∈ writes (Stmt.move d q), SupportsStmt (trSupp M S) (tr enc dec M q')
Tactic: induction q with
    | move d q IH =>
      unfold writes at hw ⊢
      replace IH := IH hs hw; refine ⟨?_, IH.2⟩
      cases d <;> simp only [trNormal, supportsStmt_move, IH]
    | write f q IH =>
      unfold writes at hw ⊢
      simp only [Finset.mem_image, Finset.mem_union, Finset.mem_univ, true_and]
        at hw ⊢
      replace IH := IH hs fun q hq ↦ hw q (Or.inr hq)
      refine ⟨supportsStmt_read _ fun a _ s ↦ hw _ (Or.inl ⟨_, rfl⟩), fun q' hq ↦ ?_⟩
      rcases hq with (⟨a, q₂, rfl⟩ | hq)
      · simp only [tr, supportsStmt_write, supportsStmt_move, IH.1]
      · exact IH.2 _ hq
    | load a q IH =>
      unfold writes at hw ⊢
      replace IH := IH hs hw
      exact ⟨supportsStmt_read _ fun _ ↦ IH.1, IH.2⟩
    | branch p q₁ q₂ IH₁ IH₂ =>
      unfold writes at hw ⊢
      simp only [Finset.mem_union] at hw ⊢
      replace IH₁ := IH₁ hs.1 fun q hq ↦ hw q (Or.inl hq)
      replace IH₂ := IH₂ hs.2 fun q hq ↦ hw q (Or.inr hq)
      exact ⟨supportsStmt_read _ fun _ ↦ ⟨IH₁.1, IH₂.1⟩, fun q ↦ Or.rec (IH₁.2 _) (IH₂.2 _)⟩
    | goto l =>
      simp only [writes, Finset.notMem_empty]; refine ⟨?_, fun _ ↦ False.elim⟩
      refine supportsStmt_read _ fun a _ s ↦ ?_
      exact Finset.mem_biUnion.2 ⟨_, hs _ _, Finset.mem_insert_self _ _⟩
    | halt =>
      simp only [writes, Finset.notMem_empty]; refine ⟨?_, fun _ ↦ False.elim⟩
      simp only [SupportsStmt, trNormal]
Cleared hypotheses: q, hs, hw
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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
q : Stmt Γ Λ σ
hs : SupportsStmt S q
hw : ∀ q' ∈ writes q, q' ∈ trSupp M S
move :
  ∀ (d : Dir) (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.move d q)) (hw : ∀ q' ∈ writes (Stmt.move d q), q' ∈ trSupp M S),
    SupportsStmt (trSupp M S) (trNormal dec (Stmt.move d q)) ∧
      ∀ q' ∈ writes (Stmt.move d 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')
have write : ∀ (f : Γ → σ → Γ) (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.write f q)) (hw : ∀ q' ∈ writes (Stmt.write f q), q' ∈ trSupp M S),
  SupportsStmt (trSupp M S) (trNormal dec (Stmt.write f q)) ∧
    ∀ q' ∈ writes (Stmt.write f q), SupportsStmt (trSupp M S) (tr enc dec M q')
Tactic: induction q with
    | move d q IH =>
      unfold writes at hw ⊢
      replace IH := IH hs hw; refine ⟨?_, IH.2⟩
      cases d <;> simp only [trNormal, supportsStmt_move, IH]
    | write f q IH =>
      unfold writes at hw ⊢
      simp only [Finset.mem_image, Finset.mem_union, Finset.mem_univ, true_and]
        at hw ⊢
      replace IH := IH hs fun q hq ↦ hw q (Or.inr hq)
      refine ⟨supportsStmt_read _ fun a _ s ↦ hw _ (Or.inl ⟨_, rfl⟩), fun q' hq ↦ ?_⟩
      rcases hq with (⟨a, q₂, rfl⟩ | hq)
      · simp only [tr, supportsStmt_write, supportsStmt_move, IH.1]
      · exact IH.2 _ hq
    | load a q IH =>
      unfold writes at hw ⊢
      replace IH := IH hs hw
      exact ⟨supportsStmt_read _ fun _ ↦ IH.1, IH.2⟩
    | branch p q₁ q₂ IH₁ IH₂ =>
      unfold writes at hw ⊢
      simp only [Finset.mem_union] at hw ⊢
      replace IH₁ := IH₁ hs.1 fun q hq ↦ hw q (Or.inl hq)
      replace IH₂ := IH₂ hs.2 fun q hq ↦ hw q (Or.inr hq)
      exact ⟨supportsStmt_read _ fun _ ↦ ⟨IH₁.1, IH₂.1⟩, fun q ↦ Or.rec (IH₁.2 _) (IH₂.2 _)⟩
    | goto l =>
      simp only [writes, Finset.notMem_empty]; refine ⟨?_, fun _ ↦ False.elim⟩
      refine supportsStmt_read _ fun a _ s ↦ ?_
      exact Finset.mem_biUnion.2 ⟨_, hs _ _, Finset.mem_insert_self _ _⟩
    | halt =>
      simp only [writes, Finset.notMem_empty]; refine ⟨?_, fun _ ↦ False.elim⟩
      simp only [SupportsStmt, trNormal]
Cleared hypotheses: q, hs, hw
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
Λ : Type u_2
inst_1 : Inhabited Λ
M : TM0.Machine Γ Λ
x : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
⊢ FRespects (TM1.step (tr M)) (trCfg M) (trCfg M { q := q, Tape := T : TM0.Cfg Γ Λ })
    (TM0.step M { q := q, Tape := T : TM0.Cfg Γ Λ })
have none : ∀ (e : M q T.head = 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: rcases e : M q T.1 with - | val
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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 Γ Λ })
⊢ FRespects (TM1.step (tr M)) (trCfg M) (trCfg M { q := q, Tape := T : TM0.Cfg Γ Λ })
    (TM0.step M { q := q, Tape := T : TM0.Cfg Γ Λ })
have some : ∀ (val : Prod.{u_2, u_1} Λ (TM0.Stmt Γ)) (e : M q T.head = 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 Γ Λ })
Tactic: rcases e : M q T.1 with - | val
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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) (trCfg M { q := q, Tape := T : TM0.Cfg Γ Λ })
    (TM0.step M { q := q, Tape := T : TM0.Cfg Γ Λ })
have 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: simp only [TM0.step, trCfg, e]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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 = 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 Γ Λ })
have some : ∀ (q' : Λ) (s : TM0.Stmt Γ) (e : M q T.head = 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 Γ Λ })
Tactic: obtain ⟨q', s⟩ := val
Cleared hypotheses: val, e
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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 = 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 Γ Λ })
have some : Reaches₁ (TM1.step (tr M)) { l := 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
        | some val => true
        | none => false with
      | true => 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: simp only [FRespects, TM0.step, trCfg, e, Option.isSome, cond, Option.map_some]