awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
inst : Inhabited Γ
inst_1 : Finite Γ
rcases :
  ∀ (n : ℕ) (e : Γ ≃ Fin n),
    ∃ (n : ℕ) (enc : Γ → List.Vector Bool n) (dec : List.Vector Bool n → Γ),
      enc default = List.Vector.replicate n false ∧ ∀ (a : Γ), dec (enc a) = a
⊢ ∃ (n : ℕ) (enc : Γ → List.Vector Bool n) (dec : List.Vector Bool n → Γ),
    enc default = List.Vector.replicate n false ∧ ∀ (a : Γ), dec (enc a) = a

Tactic:
rcases Finite.exists_equiv_fin Γ with ⟨n, ⟨e⟩⟩

Premises used: Finite.exists_equiv_fin
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
inst : Inhabited Γ
inst_1 : Finite Γ
n : ℕ
e : Γ ≃ Fin n
this : DecidableEq Γ := e.decidableEq
G : Fin n ↪ Fin n → Bool := { toFun := fun (a b : Fin n) ↦ decide (a = b), inj' := ⋯ }
H : Γ ↪ List.Vector Bool n := (e.toEmbedding.trans G).trans (Equiv.vectorEquivFin Bool n).symm.toEmbedding
enc : Γ ↪ List.Vector Bool n := H.setValue default (List.Vector.replicate n false)
⊢ ∃ (n : ℕ) (enc : Γ → List.Vector Bool n) (dec : List.Vector Bool n → Γ),
    enc default = List.Vector.replicate n false ∧ ∀ (a : Γ), dec (enc a) = a

Tactic:
⟨_, enc, Function.invFun enc, H.setValue_eq _ _, Function.leftInverse_invFun enc.2⟩

Premises used: Function.invFun, Function.Embedding.setValue_eq, Function.Embedding.inj', Function.leftInverse_invFun, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
inst : Inhabited Γ
inst_1 : Finite Γ
n : ℕ
e : Γ ≃ Fin n
this : DecidableEq Γ := e.decidableEq
G : Fin n ↪ Fin n → Bool := { toFun := fun (a b : Fin n) ↦ decide (a = b), inj' := ⋯ }
H : Γ ↪ List.Vector Bool n := (e.toEmbedding.trans G).trans (Equiv.vectorEquivFin Bool n).symm.toEmbedding
enc : Γ ↪ List.Vector Bool n := H.setValue default (List.Vector.replicate n false)
⊢ ∃ (n : ℕ) (enc : Γ → List.Vector Bool n) (dec : List.Vector Bool n → Γ),
    enc default = List.Vector.replicate n false ∧ ∀ (a : Γ), dec (enc a) = a

Tactic:
exact ⟨_, enc, Function.invFun enc, H.setValue_eq _ _, Function.leftInverse_invFun enc.2⟩
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
T : Tape Bool
suffices : ∀ (i : ℕ), stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T)
⊢ stepAux (move n d q) v T = stepAux q v ((Tape.move d)^[n] T)

Tactic:
suffices ∀ i, stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T) from this n
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
T : Tape Bool
⊢ stepAux ((Stmt.move d)^[0] q) v T = stepAux q v ((Tape.move d)^[0] T)

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
i : ℕ
IH : ∀ (T : Tape Bool), stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T)
T : Tape Bool
succ : stepAux ((Stmt.move d ∘ (Stmt.move d)^[i]) q) v T = stepAux q v (((Tape.move d)^[i] ∘ Tape.move d) T)
⊢ stepAux ((Stmt.move d)^[i + 1] q) v T = stepAux q v ((Tape.move d)^[i + 1] T)

Tactic:
rw [iterate_succ', iterate_succ]

Premises used: Function.iterate_succ, Function.iterate_succ'
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
i : ℕ
IH : ∀ (T : Tape Bool), stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T)
T : Tape Bool
succ : stepAux ((Stmt.move d)^[i] q) v (Tape.move d T) = stepAux q v ((Tape.move d)^[i] (Tape.move d T))
⊢ stepAux ((Stmt.move d ∘ (Stmt.move d)^[i]) q) v T = stepAux q v (((Tape.move d)^[i] ∘ Tape.move d) T)

Tactic:
simp only [stepAux, Function.comp_apply]

Premises used: Turing.TM1.stepAux, Function.comp_apply
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
i : ℕ
IH : ∀ (T : Tape Bool), stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T)
T : Tape Bool
succ succ₁ : stepAux q v ((Tape.move d)^[i] (Tape.move d T)) = stepAux q v ((Tape.move d)^[i] (Tape.move d T))
⊢ stepAux ((Stmt.move d)^[i] q) v (Tape.move d T) = stepAux q v ((Tape.move d)^[i] (Tape.move d T))

Tactic:
rw [IH]
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
T : Tape Bool
i : ℕ
zero : ∀ (T : Tape Bool), stepAux ((Stmt.move d)^[0] q) v T = stepAux q v ((Tape.move d)^[0] T)
succ :
  ∀ (i : ℕ) (IH : ∀ (T : Tape Bool), stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T))
    (T : Tape Bool), stepAux ((Stmt.move d)^[i + 1] q) v T = stepAux q v ((Tape.move d)^[i + 1] T)
⊢ stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T)

Tactic:
induction i generalizing T with
  | zero => rfl
  | succ i IH =>
    rw [iterate_succ', iterate_succ]
    simp only [stepAux, Function.comp_apply]
    rw [IH]

Premises used: Function.iterate_succ, Function.iterate_succ', Turing.TM1.stepAux, Function.comp_apply
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
S : Finset (Λ' Γ Λ σ)
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
suffices : ∀ {i : ℕ}, SupportsStmt S ((Stmt.move d)^[i] q) = SupportsStmt S q
⊢ SupportsStmt S (move n d q) = SupportsStmt S q

Tactic:
suffices ∀ {i}, SupportsStmt S ((Stmt.move d)^[i] q) = _ from this
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
S : Finset (Λ' Γ Λ σ)
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
zero : ∀ {q : Stmt Bool (Λ' Γ Λ σ) σ}, SupportsStmt S ((Stmt.move d)^[0] q) = SupportsStmt S q
succ :
  ∀ (n : ℕ),
    (∀ {q : Stmt Bool (Λ' Γ Λ σ) σ}, SupportsStmt S ((Stmt.move d)^[n] q) = SupportsStmt S q) →
      ∀ {q : Stmt Bool (Λ' Γ Λ σ) σ}, SupportsStmt S ((Stmt.move d)^[n + 1] q) = SupportsStmt S q
⊢ SupportsStmt S ((Stmt.move d)^[i] q) = SupportsStmt S q

Tactic:
induction i generalizing q
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
S : Finset (Λ' Γ Λ σ)
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
⊢ SupportsStmt S ((Stmt.move d)^[0] q) = SupportsStmt S q

Tactic:
simp only [*, iterate]

Premises used: Nat.iterate
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
S : Finset (Λ' Γ Λ σ)
d : Dir
n_1 : ℕ
h : ∀ {q : Stmt Bool (Λ' Γ Λ σ) σ}, SupportsStmt S ((Stmt.move d)^[n_1] q) = SupportsStmt S q
q : Stmt Bool (Λ' Γ Λ σ) σ
succ : SupportsStmt S (Stmt.move d q) = SupportsStmt S q
⊢ SupportsStmt S ((Stmt.move d)^[n_1 + 1] q) = SupportsStmt S q

Tactic:
simp only [*, iterate]

Premises used: Nat.iterate
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
S : Finset (Λ' Γ Λ σ)
d : Dir
n_1 : ℕ
h : ∀ {q : Stmt Bool (Λ' Γ Λ σ) σ}, SupportsStmt S ((Stmt.move d)^[n_1] q) = SupportsStmt S q
q : Stmt Bool (Λ' Γ Λ σ) σ
⊢ SupportsStmt S (Stmt.move d q) = SupportsStmt S q

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset (Λ' Γ Λ σ)
l : List Bool
q : Stmt Bool (Λ' Γ Λ σ) σ
nil : SupportsStmt S (write [] q) = SupportsStmt S q
cons :
  ∀ (head : Bool) (tail : List Bool),
    SupportsStmt S (write tail q) = SupportsStmt S q → SupportsStmt S (write (head :: tail) q) = SupportsStmt S q
⊢ SupportsStmt S (write l q) = SupportsStmt S q

Tactic:
induction l
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset (Λ' Γ Λ σ)
q : Stmt Bool (Λ' Γ Λ σ) σ
⊢ SupportsStmt S (write [] q) = SupportsStmt S q

Tactic:
simp only [write, SupportsStmt, *]

Premises used: Turing.TM1to1.write, Turing.TM1.SupportsStmt
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset (Λ' Γ Λ σ)
q : Stmt Bool (Λ' Γ Λ σ) σ
head : Bool
tail : List Bool
tail_ih : SupportsStmt S (write tail q) = SupportsStmt S q
⊢ SupportsStmt S (write (head :: tail) q) = SupportsStmt S q

Tactic:
simp only [write, SupportsStmt, *]

Premises used: Turing.TM1to1.write, Turing.TM1.SupportsStmt
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f_1 : Γ → Stmt Bool (Λ' Γ Λ σ) σ
f : List.Vector Bool 0 → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool 0), SupportsStmt S (f v)
⊢ SupportsStmt S (readAux 0 f)

Tactic:
hf _

Premises used: Turing.TM1to1.readAux
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f_1 : Γ → Stmt Bool (Λ' Γ Λ σ) σ
f : List.Vector Bool 0 → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool 0), SupportsStmt S (f v)
⊢ SupportsStmt S (readAux 0 f)

Tactic:
exact hf _
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f_1 : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ) (hf : ∀ (v : List.Vector Bool i), SupportsStmt S (f v)),
    SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
succ : SupportsStmt S (Stmt.move Dir.right (readAux i fun (v : List.Vector Bool i) ↦ f (true ::ᵥ v)))
succ₁ : SupportsStmt S (Stmt.move Dir.right (readAux i fun (v : List.Vector Bool i) ↦ f (false ::ᵥ v)))
⊢ SupportsStmt S (readAux (i + 1) f)

Tactic:
constructor
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f_1 : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ) (hf : ∀ (v : List.Vector Bool i), SupportsStmt S (f v)),
    SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
succ : ∀ (v : List.Vector Bool i), SupportsStmt S (f (true ::ᵥ v))
⊢ SupportsStmt S (Stmt.move Dir.right (readAux i fun (v : List.Vector Bool i) ↦ f (true ::ᵥ v)))

Tactic:
apply IH
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f_1 : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ) (hf : ∀ (v : List.Vector Bool i), SupportsStmt S (f v)),
    SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
succ : ∀ (v : List.Vector Bool i), SupportsStmt S (f (false ::ᵥ v))
⊢ SupportsStmt S (Stmt.move Dir.right (readAux i fun (v : List.Vector Bool i) ↦ f (false ::ᵥ v)))

Tactic:
apply IH
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f_1 : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ) (hf : ∀ (v : List.Vector Bool i), SupportsStmt S (f v)),
    SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
v : List.Vector Bool i
⊢ SupportsStmt S (f (true ::ᵥ v))

Tactic:
apply hf
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f_1 : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
IH :
  ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ) (hf : ∀ (v : List.Vector Bool i), SupportsStmt S (f v)),
    SupportsStmt S (readAux i f)
f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)
v : List.Vector Bool i
⊢ SupportsStmt S (f (false ::ᵥ v))

Tactic:
apply hf
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f_1 : Γ → Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ
hf : ∀ (v : List.Vector Bool i), SupportsStmt S (f v)
zero :
  ∀ (f : List.Vector Bool 0 → Stmt Bool (Λ' Γ Λ σ) σ) (hf : ∀ (v : List.Vector Bool 0), SupportsStmt S (f v)),
    SupportsStmt S (readAux 0 f)
succ :
  ∀ (i : ℕ)
    (IH :
      ∀ (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ) (hf : ∀ (v : List.Vector Bool i), SupportsStmt S (f v)),
        SupportsStmt S (readAux i f))
    (f : List.Vector Bool (i + 1) → Stmt Bool (Λ' Γ Λ σ) σ)
    (hf : ∀ (v : List.Vector Bool (i + 1)), SupportsStmt S (f v)), SupportsStmt S (readAux (i + 1) f)
⊢ SupportsStmt S (readAux i f)

Tactic:
induction i with
  | zero => exact hf _
  | succ i IH => constructor <;> apply IH <;> intro <;> apply hf
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
dec : List.Vector Bool n → Γ
S : Finset (Λ' Γ Λ σ)
f : Γ → Stmt Bool (Λ' Γ Λ σ) σ
this :
  ∀ (i : ℕ) (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ),
    (∀ (v : List.Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
hf : ∀ (a : Γ), SupportsStmt S (f a)
v : List.Vector Bool n
⊢ SupportsStmt S (move n Dir.left (f (dec v)))

Tactic:
simp only [supportsStmt_move, hf]

Premises used: 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 : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
refine_1 : Eq (α := List Bool) ((fun (x : Γ) ↦ (enc x).toList.reverse) default) (List.replicate n default)
refine_2 : Eq (α := List Bool) ((fun (x : Γ) ↦ (enc x).toList) default) (List.replicate n default)
⊢ Tape Bool

Tactic:
refine
      Tape.mk' (L.flatMap (fun x ↦ (enc x).toList.reverse) ⟨n, ?_⟩)
        (R.flatMap (fun x ↦ (enc x).toList) ⟨n, ?_⟩)

Premises used: Turing.Tape.mk', Turing.ListBlank.flatMap, Exists.intro, List.reverse, List.Vector.toList
-- 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
L R : ListBlank Γ
⊢ Eq (α := List Bool) ((fun (x : Γ) ↦ (enc x).toList.reverse) default) (List.replicate n default)

Tactic:
simp only [enc0, List.Vector.replicate, List.reverse_replicate, Bool.default_bool,
      List.Vector.toList_mk]

Premises used: List.Vector.toList_mk, List.Vector.replicate, Bool.default_bool, List.reverse_replicate
-- 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
L R : ListBlank Γ
⊢ Eq (α := List Bool) ((fun (x : Γ) ↦ (enc x).toList) default) (List.replicate n default)

Tactic:
simp only [enc0, List.Vector.replicate, List.reverse_replicate, Bool.default_bool,
      List.Vector.toList_mk]

Premises used: List.Vector.toList_mk, List.Vector.replicate, Bool.default_bool, List.reverse_replicate
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
⊢ trTape enc0 (Tape.mk' L R) = trTape' enc0 L R

Tactic:
simp only [trTape, Tape.mk'_left, Tape.mk'_right₀]

Premises used: Turing.TM1to1.trTape, Turing.Tape.mk'_left, Turing.Tape.mk'_right₀
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
obtain :
  ∀ (a : Γ) (L : ListBlank Γ),
    (Tape.move Dir.left)^[n] (trTape' enc0 (ListBlank.cons a L) R) =
      trTape' enc0 (ListBlank.cons a L).tail (ListBlank.cons (ListBlank.cons a L).head R)
⊢ (Tape.move Dir.left)^[n] (trTape' enc0 L R) = trTape' enc0 L.tail (ListBlank.cons L.head R)

Tactic:
obtain ⟨a, L, rfl⟩ := L.exists_cons

Premises used: Turing.ListBlank.exists_cons, rfl
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
simp :
  Eq (α := Tape Bool)
    ((Tape.move Dir.left)^[n]
      (Tape.mk' (ListBlank.append (enc a).toList.reverse (L.flatMap (fun (x : Γ) ↦ (enc x).toList.reverse) ⋯))
        (R.flatMap (fun (x : Γ) ↦ (enc x).toList) ⋯)))
    (Tape.mk' (L.flatMap (fun (x : Γ) ↦ (enc x).toList.reverse) ⋯)
      (ListBlank.append (enc a).toList (R.flatMap (fun (x : Γ) ↦ (enc x).toList) ⋯)))
⊢ (Tape.move Dir.left)^[n] (trTape' enc0 (ListBlank.cons a L) R) =
    trTape' enc0 (ListBlank.cons a L).tail (ListBlank.cons (ListBlank.cons a L).head R)

Tactic:
simp only [trTape', ListBlank.cons_flatMap, ListBlank.head_cons, ListBlank.tail_cons]

Premises used: Turing.TM1to1.trTape', Turing.ListBlank.head_cons, Turing.ListBlank.tail_cons, Turing.ListBlank.cons_flatMap
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
this :
  ∀ {L' R' : ListBlank Bool} {l₁ l₂ : List Bool},
    (enc a).toList = l₁.reverseAux l₂ →
      (Tape.move Dir.left)^[l₁.length] (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
        Tape.mk' L' (ListBlank.append (enc a).toList R')
⊢ Eq (α := Tape Bool)
    ((Tape.move Dir.left)^[n]
      (Tape.mk' (ListBlank.append (enc a).toList.reverse (L.flatMap (fun (x : Γ) ↦ (enc x).toList.reverse) ⋯))
        (R.flatMap (fun (x : Γ) ↦ (enc x).toList) ⋯)))
    (Tape.mk' (L.flatMap (fun (x : Γ) ↦ (enc x).toList.reverse) ⋯)
      (ListBlank.append (enc a).toList (R.flatMap (fun (x : Γ) ↦ (enc x).toList) ⋯)))

Tactic:
simpa only [List.length_reverse, Vector.toList_length] using this (List.reverse_reverse _).symm

Premises used: List.length_reverse, List.Vector.toList_length, List.reverse_reverse, Eq.symm
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
suffices :
  ∀ {L' R' : ListBlank Bool} {l₁ l₂ : List Bool},
    (enc a).toList = l₁.reverseAux l₂ →
      (Tape.move Dir.left)^[l₁.length] (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
        Tape.mk' L' (ListBlank.append (enc a).toList R')
⊢ Eq (α := Tape Bool)
    ((Tape.move Dir.left)^[n]
      (Tape.mk' (ListBlank.append (enc a).toList.reverse (L.flatMap (fun (x : Γ) ↦ (enc x).toList.reverse) ⋯))
        (R.flatMap (fun (x : Γ) ↦ (enc x).toList) ⋯)))
    (Tape.mk' (L.flatMap (fun (x : Γ) ↦ (enc x).toList.reverse) ⋯)
      (ListBlank.append (enc a).toList (R.flatMap (fun (x : Γ) ↦ (enc x).toList) ⋯)))

Tactic:
suffices ∀ {L' R' l₁ l₂} (_ : List.Vector.toList (enc a) = List.reverseAux l₁ l₂),
      (Tape.move Dir.left)^[l₁.length]
      (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      Tape.mk' L' (ListBlank.append (List.Vector.toList (enc a)) R') by
    simpa only [List.length_reverse, Vector.toList_length] using this (List.reverse_reverse _).symm
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
L' : ListBlank Bool
_ :
  ∀ {R' : ListBlank Bool} {l₁ l₂ : List Bool},
    (enc a).toList = l₁.reverseAux l₂ →
      (Tape.move Dir.left)^[l₁.length] (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
        Tape.mk' L' (ListBlank.append (enc a).toList R')
⊢ ∀ {R' : ListBlank Bool} {l₁ l₂ : List Bool},
    (enc a).toList = l₁.reverseAux l₂ →
      (Tape.move Dir.left)^[l₁.length] (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
        Tape.mk' L' (ListBlank.append (enc a).toList R')

Tactic:
_
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
L' R' : ListBlank Bool
l₂ : List Bool
e : (enc a).toList = List.reverseAux [] l₂
nil :
  (Tape.move Dir.left)^[List.length (α := Bool) []]
      (Tape.mk' (ListBlank.append [] L') (ListBlank.append (enc a).1 R')) =
    Tape.mk' L' (ListBlank.append (enc a).toList R')
⊢ (Tape.move Dir.left)^[List.length (α := Bool) []] (Tape.mk' (ListBlank.append [] L') (ListBlank.append l₂ R')) =
    Tape.mk' L' (ListBlank.append (enc a).toList R')

Tactic:
cases e
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
L' R' : ListBlank Bool
⊢ (Tape.move Dir.left)^[List.length (α := Bool) []]
      (Tape.mk' (ListBlank.append [] L') (ListBlank.append (enc a).1 R')) =
    Tape.mk' L' (ListBlank.append (enc a).toList R')

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
L' R' : ListBlank Bool
b : Bool
l₁ : List Bool
IH :
  ∀ {l₂ : List Bool} (e : (enc a).toList = l₁.reverseAux l₂),
    (Tape.move Dir.left)^[l₁.length] (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      Tape.mk' L' (ListBlank.append (enc a).toList R')
l₂ : List Bool
e : (enc a).toList = (b :: l₁).reverseAux l₂
cons :
  (Tape.move Dir.left)^[l₁.length]
      (Tape.move Dir.left (Tape.mk' (ListBlank.append (b :: l₁) L') (ListBlank.append l₂ R'))) =
    Tape.mk' L' (ListBlank.append (enc a).toList R')
⊢ (Tape.move Dir.left)^[(b :: l₁).length] (Tape.mk' (ListBlank.append (b :: l₁) L') (ListBlank.append l₂ R')) =
    Tape.mk' L' (ListBlank.append (enc a).toList R')

Tactic:
simp only [List.length, iterate_succ_apply]

Premises used: Function.iterate_succ_apply, List.length
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
L' R' : ListBlank Bool
b : Bool
l₁ : List Bool
IH :
  ∀ {l₂ : List Bool} (e : (enc a).toList = l₁.reverseAux l₂),
    (Tape.move Dir.left)^[l₁.length] (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      Tape.mk' L' (ListBlank.append (enc a).toList R')
l₂ : List Bool
e : (enc a).toList = (b :: l₁).reverseAux l₂
⊢ (Tape.move Dir.left)^[l₁.length] (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append (b :: l₂) R')) =
    Tape.mk' L' (ListBlank.append (enc a).toList R')

Tactic:
IH e