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 : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x : Cfg Γ Λ σ
l : Γ → σ → Λ
v : σ
L R : ListBlank Γ
⊢ Reaches (step (tr enc dec M))
    { l := some (Λ'.normal (l R.head v)), var := v, Tape := trTape' enc0 L R : Cfg Bool (Λ' Γ Λ σ) σ }
    { l := Option.map Λ'.normal (some (l (Tape.mk' L R).head v)), var := v, Tape := trTape' enc0 L R }

Tactic:
apply ReflTransGen.refl

Premises used: Relation.ReflTransGen.refl
-- 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 : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x : Cfg Γ Λ σ
v : σ
L R : ListBlank Γ
some :
  Reaches (step (tr enc dec M)) { l := none, var := v, Tape := trTape' enc0 L R : Cfg Bool (Λ' Γ Λ σ) σ }
    { l := Option.map Λ'.normal none, var := v, Tape := trTape' enc0 L R }
⊢ Reaches (step (tr enc dec M)) (stepAux (trNormal dec Stmt.halt) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux Stmt.halt v (Tape.mk' L R)))

Tactic:
simp only [trNormal, stepAux, trCfg,
        trTape_mk']

Premises used: Turing.TM1to1.trTape_mk', Turing.TM1to1.trNormal, Turing.TM1.stepAux, Turing.TM1to1.trCfg
-- 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 : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x : Cfg Γ Λ σ
v : σ
L R : ListBlank Γ
⊢ Reaches (step (tr enc dec M)) { l := none, var := v, Tape := trTape' enc0 L R : Cfg Bool (Λ' Γ Λ σ) σ }
    { l := Option.map Λ'.normal none, var := v, Tape := trTape' enc0 L R }

Tactic:
apply ReflTransGen.refl

Premises used: Relation.ReflTransGen.refl
-- 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
this :
  ∀ (q : Stmt Γ Λ σ),
    SupportsStmt S 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')
rcases :
  ∀ (l : Λ) (hl : l ∈ S) (h : q ∈ insert (Λ'.normal l) (writes (M l))), SupportsStmt (trSupp M S) (tr enc dec M q)
⊢ SupportsStmt (trSupp M S) (tr enc dec M q)

Tactic:
rcases Finset.mem_biUnion.1 h with ⟨l, hl, h⟩

Premises used: Iff.mp, 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_1 : q ∈ trSupp M S
this :
  ∀ (q : Stmt Γ Λ σ),
    SupportsStmt S 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')
l : Λ
hl : l ∈ S
h : q ∈ insert (Λ'.normal l) (writes (M l))
⊢ SupportsStmt (trSupp M S) (trNormal dec (M l)) ∧ ∀ q' ∈ writes (M l), SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
have :=
        this _ (ss.2 _ hl) fun q' hq ↦ Finset.mem_biUnion.2 ⟨_, hl, Finset.mem_insert_of_mem 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_1 : q ∈ trSupp M S
this_1 :
  ∀ (q : Stmt Γ Λ σ),
    SupportsStmt S 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')
l : Λ
hl : l ∈ S
h : q ∈ insert (Λ'.normal l) (writes (M l))
this : SupportsStmt (trSupp M S) (trNormal dec (M l)) ∧ ∀ q' ∈ writes (M l), SupportsStmt (trSupp M S) (tr enc dec M q')
inl :
  ∀ (h : Λ'.normal l ∈ trSupp M S) (h : Λ'.normal l ∈ insert (Λ'.normal l) (writes (M l))),
    SupportsStmt (trSupp M S) (tr enc dec M (Λ'.normal l))
inr : ∀ (h : q ∈ writes (M l)), SupportsStmt (trSupp M S) (tr enc dec M q)
⊢ SupportsStmt (trSupp M S) (tr enc dec M q)

Tactic:
rcases Finset.mem_insert.1 h with (rfl | h)

Premises used: Finset.mem_insert, Iff.mp, rfl
-- 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
this_1 :
  ∀ (q : Stmt Γ Λ σ),
    SupportsStmt S 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')
l : Λ
hl : l ∈ S
this : SupportsStmt (trSupp M S) (trNormal dec (M l)) ∧ ∀ q' ∈ writes (M l), SupportsStmt (trSupp M S) (tr enc dec M q')
h_1 : Λ'.normal l ∈ trSupp M S
h : Λ'.normal l ∈ insert (Λ'.normal l) (writes (M l))
⊢ SupportsStmt (trSupp M S) (tr enc dec M (Λ'.normal l))

Tactic:
this.1

Premises used: Turing.TM1to1.tr, And.left
-- 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_1 : q ∈ trSupp M S
this_1 :
  ∀ (q : Stmt Γ Λ σ),
    SupportsStmt S 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')
l : Λ
hl : l ∈ S
h_2 : q ∈ insert (Λ'.normal l) (writes (M l))
this : SupportsStmt (trSupp M S) (trNormal dec (M l)) ∧ ∀ q' ∈ writes (M l), SupportsStmt (trSupp M S) (tr enc dec M q')
h : q ∈ writes (M l)
⊢ SupportsStmt (trSupp M S) (tr enc dec M q)

Tactic:
this.2 _ h

Premises used: And.right
-- 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
this_1 :
  ∀ (q : Stmt Γ Λ σ),
    SupportsStmt S 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')
l : Λ
hl : l ∈ S
this : SupportsStmt (trSupp M S) (trNormal dec (M l)) ∧ ∀ q' ∈ writes (M l), SupportsStmt (trSupp M S) (tr enc dec M q')
h_1 : Λ'.normal l ∈ trSupp M S
h : Λ'.normal l ∈ insert (Λ'.normal l) (writes (M l))
⊢ SupportsStmt (trSupp M S) (tr enc dec M (Λ'.normal l))

Tactic:
exacts [this.1, this.2 _ h]

Premises used: And.right, And.left
-- 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
suffices :
  ∀ (q : Stmt Γ Λ σ),
    SupportsStmt S 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')
⊢ SupportsStmt (trSupp M S) (tr enc dec M q)

Tactic:
suffices ∀ q, SupportsStmt S 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') by
      rcases Finset.mem_biUnion.1 h with ⟨l, hl, h⟩
      have :=
        this _ (ss.2 _ hl) fun q' hq ↦ Finset.mem_biUnion.2 ⟨_, hl, Finset.mem_insert_of_mem hq⟩
      rcases Finset.mem_insert.1 h with (rfl | h)
      exacts [this.1, this.2 _ h]
-- 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
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
move :
  ∀ (hw : ∀ q' ∈ writes q, q' ∈ trSupp M S),
    SupportsStmt (trSupp M S) (trNormal dec (Stmt.move d q)) ∧
      ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
⊢ 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:
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_1 : Λ' Γ Λ σ
h : q_1 ∈ trSupp M S
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 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 hw
-- 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
d : Dir
q : Stmt Γ Λ σ
hs : SupportsStmt S (Stmt.move d 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.move d q)) ∧
    ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
⟨?_, IH.2⟩

Premises used: And.right, 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_1 : Λ' Γ Λ σ
h : q_1 ∈ trSupp M S
d : Dir
q : Stmt Γ Λ σ
hs : SupportsStmt S (Stmt.move d 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')
move : SupportsStmt (trSupp M S) (trNormal dec (Stmt.move d q))
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.move d q)) ∧
    ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
refine ⟨?_, 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_1 : Λ' Γ Λ σ
h : q_1 ∈ trSupp M S
d : Dir
q : Stmt Γ Λ σ
hs : SupportsStmt S (Stmt.move d 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')
move : ∀ (hs : SupportsStmt S (Stmt.move Dir.left q)), SupportsStmt (trSupp M S) (trNormal dec (Stmt.move Dir.left q))
move₁ :
  ∀ (hs : SupportsStmt S (Stmt.move Dir.right q)), SupportsStmt (trSupp M S) (trNormal dec (Stmt.move Dir.right q))
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.move d q))

Tactic:
cases d
-- 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
q : Stmt Γ Λ σ
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')
hs : SupportsStmt S (Stmt.move Dir.left q)
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.move Dir.left q))

Tactic:
simp only [trNormal, supportsStmt_move, IH]

Premises used: Turing.TM1to1.trNormal, Turing.TM1to1.supportsStmt_move
-- 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
q : Stmt Γ Λ σ
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')
hs : SupportsStmt S (Stmt.move Dir.right q)
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.move Dir.right q))

Tactic:
simp only [trNormal, supportsStmt_move, IH]

Premises used: Turing.TM1to1.trNormal, Turing.TM1to1.supportsStmt_move
-- 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
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
⊢ ∀ q' ∈ Finset.image (fun (a : Γ) ↦ Λ'.write a q) Finset.univ ∪ 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_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' ∈ Finset.image (fun (a : Γ) ↦ Λ'.write a q) Finset.univ ∪ writes q, q' ∈ trSupp M S
write :
  ∀ (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')
⊢ SupportsStmt (trSupp M S) (trNormal dec (Stmt.write f q)) ∧
    ∀ q' ∈ Finset.image (fun (a : Γ) ↦ Λ'.write a q) Finset.univ ∪ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
simp only [Finset.mem_image, Finset.mem_union, Finset.mem_univ, true_and]
        at hw ⊢

Premises used: Finset.mem_univ, Finset.mem_image, Finset.mem_union, true_and
-- 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
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 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)
-- 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
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')

Tactic:
⟨supportsStmt_read _ fun a _ s ↦ hw _ (Or.inl ⟨_, rfl⟩), fun q' hq ↦ ?_⟩

Premises used: Turing.TM1to1.supportsStmt_read, And.intro, Exists.intro, Or.inl, Turing.TM1to1.Λ'.write, rfl
-- 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
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')
write :
  ∀ (q' : Λ' Γ Λ σ) (hq : (∃ (a : Γ), Λ'.write a q = 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')

Tactic:
refine ⟨supportsStmt_read _ fun a _ s ↦ hw _ (Or.inl ⟨_, rfl⟩), fun q' 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_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))
write₁ : ∀ (hq : q' ∈ writes q), SupportsStmt (trSupp M S) (tr enc dec M q')
⊢ SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
rcases hq with (⟨a, q₂, rfl⟩ | hq)

Premises used: rfl
-- 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
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')
a : Γ
⊢ SupportsStmt (trSupp M S) (tr enc dec M (Λ'.write a q))

Tactic:
simp only [tr, supportsStmt_write, supportsStmt_move, IH.1]

Premises used: Turing.TM1to1.tr, And.left, Turing.TM1to1.supportsStmt_write, Turing.TM1to1.supportsStmt_move
-- 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
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 : q' ∈ writes q
⊢ SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
IH.2 _ hq

Premises used: And.right
-- 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
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 : q' ∈ writes q
⊢ SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
exact IH.2 _ hq

Premises used: And.right
-- 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 Γ Λ σ
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
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')
⊢ 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')

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_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 q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
replace IH := IH hs hw
-- 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:
⟨supportsStmt_read _ fun _ ↦ IH.1, IH.2⟩

Premises used: Turing.TM1to1.supportsStmt_read, And.right, And.left, And.intro