awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
inst : Inhabited Λ
σ : Type u_3
inst_1 : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst_2 : Inhabited Γ
l : List Γ
⊢ Eq (α := Part (ListBlank Γ))
    (Part.map (fun (c : TM0.Cfg Γ (Λ' M)) ↦ c.Tape.right₀)
      (trCfg M <$> eval (TM1.step M) { l := some default, var := default, Tape := Tape.mk₁ l }))
    (TM1.eval M l)
have rw : Eq.{u_1 + 1} (α := Part (ListBlank Γ))
  (Part.map (α := TM1.Cfg Γ Λ σ) ((fun (c : TM0.Cfg Γ (Λ' M)) ↦ c.Tape.right₀) ∘ trCfg M)
    (eval (TM1.step M) { l := some default, var := default, Tape := Tape.mk₁ l }))
  (Part.map (fun (c : TM1.Cfg Γ Λ σ) ↦ c.Tape.right₀) (eval (TM1.step M) (TM1.init l)))
Tactic: rw [Part.map_eq_map, Part.map_map, TM1.eval]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
inst_1 : Finite Γ
⊢ ∃ (n : ℕ) (enc : Γ → List.Vector Bool n) (dec : List.Vector Bool n → Γ),
    enc default = List.Vector.replicate n false ∧ ∀ (a : Γ), dec (enc a) = a
have 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
Tactic: rcases Finite.exists_equiv_fin Γ with ⟨n, ⟨e⟩⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
T : Tape Bool
⊢ stepAux (move n d q) v T = stepAux q v ((Tape.move d)^[n] T)
have suffices : ∀ (i : ℕ), stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T)
Tactic: suffices ∀ i, stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T) from this n
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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
⊢ stepAux ((Stmt.move d)^[i + 1] q) v T = stepAux q v ((Tape.move d)^[i + 1] T)
have succ : stepAux ((Stmt.move d ∘ (Stmt.move d)^[i]) q) v T = stepAux q v (((Tape.move d)^[i] ∘ Tape.move d) T)
Tactic: rw [iterate_succ', iterate_succ]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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
⊢ stepAux ((Stmt.move d ∘ (Stmt.move d)^[i]) q) v T = stepAux q v (((Tape.move d)^[i] ∘ Tape.move d) T)
have succ : stepAux ((Stmt.move d)^[i] q) v (Tape.move d T) = stepAux q v ((Tape.move d)^[i] (Tape.move d T))
Tactic: simp only [stepAux, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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
⊢ stepAux ((Stmt.move d)^[i] q) v (Tape.move d T) = stepAux q v ((Tape.move d)^[i] (Tape.move d T))
have succ : stepAux q v ((Tape.move d)^[i] (Tape.move d T)) = stepAux q v ((Tape.move d)^[i] (Tape.move d T))
Tactic: rw [IH]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
T : Tape Bool
i : ℕ
⊢ stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T)
have zero : ∀ (T : Tape Bool), stepAux ((Stmt.move d)^[0] q) v T = stepAux q v ((Tape.move d)^[0] 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]
Cleared hypotheses: T, i
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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)
⊢ stepAux ((Stmt.move d)^[i] q) v T = stepAux q v ((Tape.move d)^[i] T)
have 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)
Tactic: induction i generalizing T with
  | zero => rfl
  | succ i IH =>
    rw [iterate_succ', iterate_succ]
    simp only [stepAux, Function.comp_apply]
    rw [IH]
Cleared hypotheses: T, i
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
S : Finset (Λ' Γ Λ σ)
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
⊢ SupportsStmt S (move n d q) = SupportsStmt S q
have suffices : ∀ {i : ℕ}, SupportsStmt S ((Stmt.move d)^[i] q) = SupportsStmt S q
Tactic: suffices ∀ {i}, SupportsStmt S ((Stmt.move d)^[i] q) = _ from this
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
S : Finset (Λ' Γ Λ σ)
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
⊢ SupportsStmt S ((Stmt.move d)^[i] q) = SupportsStmt S q
have zero : ∀ {q : Stmt Bool (Λ' Γ Λ σ) σ}, SupportsStmt S ((Stmt.move d)^[0] q) = SupportsStmt S q
Tactic: induction i generalizing q
Cleared hypotheses: q, i
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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
⊢ SupportsStmt S ((Stmt.move d)^[i] q) = SupportsStmt S q
have 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
Tactic: induction i generalizing q
Cleared hypotheses: q, i
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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)^[n_1 + 1] q) = SupportsStmt S q
have succ : SupportsStmt S (Stmt.move d q) = SupportsStmt S q
Tactic: simp only [*, iterate]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
S : Finset (Λ' Γ Λ σ)
l : List Bool
q : Stmt Bool (Λ' Γ Λ σ) σ
⊢ SupportsStmt S (write l q) = SupportsStmt S q
have nil : SupportsStmt S (write [] q) = SupportsStmt S q
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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
⊢ SupportsStmt S (write l q) = SupportsStmt S q
have cons : ∀ (head : Bool) (tail : List Bool),
  SupportsStmt S (write tail q) = SupportsStmt S q → SupportsStmt S (write (head :: tail) q) = SupportsStmt S q
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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)
⊢ SupportsStmt S (readAux (i + 1) f)
have succ : SupportsStmt S (Stmt.move Dir.right (readAux i fun (v : List.Vector Bool i) ↦ f (true ::ᵥ v)))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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)))
⊢ SupportsStmt S (readAux (i + 1) f)
have succ₁ : SupportsStmt S (Stmt.move Dir.right (readAux i fun (v : List.Vector Bool i) ↦ f (false ::ᵥ v)))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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)
⊢ SupportsStmt S (Stmt.move Dir.right (readAux i fun (v : List.Vector Bool i) ↦ f (true ::ᵥ v)))
have succ : ∀ (v : List.Vector Bool i), SupportsStmt S (f (true ::ᵥ v))
Tactic: apply IH
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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)
⊢ SupportsStmt S (Stmt.move Dir.right (readAux i fun (v : List.Vector Bool i) ↦ f (false ::ᵥ v)))
have succ : ∀ (v : List.Vector Bool i), SupportsStmt S (f (false ::ᵥ v))
Tactic: apply IH
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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)
⊢ SupportsStmt S (readAux i f)
have zero : ∀ (f : List.Vector Bool 0 → Stmt Bool (Λ' Γ Λ σ) σ) (hf : ∀ (v : List.Vector Bool 0), SupportsStmt S (f v)),
  SupportsStmt S (readAux 0 f)
Tactic: induction i with
  | zero => exact hf _
  | succ i IH => constructor <;> apply IH <;> intro <;> apply hf
Cleared hypotheses: i, f, hf
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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)
⊢ SupportsStmt S (readAux i f)
have 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)
Tactic: induction i with
  | zero => exact hf _
  | succ i IH => constructor <;> apply IH <;> intro <;> apply hf
Cleared hypotheses: i, f, hf
-- 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 : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
⊢ Tape Bool
have refine_1 : Eq (α := List Bool) ((fun (x : Γ) ↦ (enc x).toList.reverse) default) (List.replicate n default)
Tactic: refine
      Tape.mk' (L.flatMap (fun x ↦ (enc x).toList.reverse) ⟨n, ?_⟩)
        (R.flatMap (fun x ↦ (enc x).toList) ⟨n, ?_⟩)
-- 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 : 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)
⊢ Tape Bool
have refine_2 : Eq (α := List Bool) ((fun (x : Γ) ↦ (enc x).toList) default) (List.replicate n default)
Tactic: refine
      Tape.mk' (L.flatMap (fun x ↦ (enc x).toList.reverse) ⟨n, ?_⟩)
        (R.flatMap (fun x ↦ (enc x).toList) ⟨n, ?_⟩)
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
⊢ (Tape.move Dir.left)^[n] (trTape' enc0 L R) = trTape' enc0 L.tail (ListBlank.cons L.head R)
have 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)
Tactic: obtain ⟨a, L, rfl⟩ := L.exists_cons
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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 Γ
⊢ (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)
have 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) sorry))
      (R.flatMap (fun (x : Γ) ↦ (enc x).toList) sorry)))
  (Tape.mk' (L.flatMap (fun (x : Γ) ↦ (enc x).toList.reverse) sorry)
    (ListBlank.append (enc a).toList (R.flatMap (fun (x : Γ) ↦ (enc x).toList) sorry)))
Tactic: simp only [trTape', ListBlank.cons_flatMap, ListBlank.head_cons, ListBlank.tail_cons]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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 Γ
⊢ 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) ⋯)))
have 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')
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
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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₂
⊢ (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')
have 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')
Tactic: cases e
Cleared hypotheses: l₂, e
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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)^[(b :: l₁).length] (Tape.mk' (ListBlank.append (b :: l₁) L') (ListBlank.append l₂ R')) =
    Tape.mk' L' (ListBlank.append (enc a).toList R')
have 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')
Tactic: simp only [List.length, iterate_succ_apply]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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.move Dir.left (Tape.mk' (ListBlank.append (b :: l₁) L') (ListBlank.append l₂ R'))) =
    Tape.mk' L' (ListBlank.append (enc a).toList R')
have h : Tape.move Dir.left (Tape.mk' (ListBlank.append (b :: l₁) L') (ListBlank.append l₂ R')) =
  Tape.mk' (ListBlank.append l₁ L') (ListBlank.append (b :: l₂) R')
Tactic: convert! IH e
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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₁ 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')
have nil : ∀ {l₂ : List Bool} (e : (enc a).toList = List.reverseAux [] l₂),
  (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: induction l₁ generalizing l₂ with
  | nil => cases e; rfl
  | cons b l₁ IH =>
    simp only [List.length, iterate_succ_apply]
    convert! IH e
    simp only [ListBlank.tail_cons, ListBlank.append, Tape.move_left_mk', ListBlank.head_cons]
Cleared hypotheses: l₁, l₂, e
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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₁ l₂ : List Bool
e : (enc a).toList = l₁.reverseAux l₂
nil :
  ∀ {l₂ : List Bool} (e : (enc a).toList = List.reverseAux [] l₂),
    (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')
⊢ (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')
have cons : ∀ (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)^[(b :: l₁).length] (Tape.mk' (ListBlank.append (b :: l₁) L') (ListBlank.append l₂ R')) =
    Tape.mk' L' (ListBlank.append (enc a).toList R')
Tactic: induction l₁ generalizing l₂ with
  | nil => cases e; rfl
  | cons b l₁ IH =>
    simp only [List.length, iterate_succ_apply]
    convert! IH e
    simp only [ListBlank.tail_cons, ListBlank.append, Tape.move_left_mk', ListBlank.head_cons]
Cleared hypotheses: l₁, l₂, e
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
this : ∀ (i : ℕ) (L : Tape Bool), (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L) = L
⊢ (Tape.move Dir.right)^[n] (trTape' enc0 L R) = trTape' enc0 (ListBlank.cons R.head L) R.tail
have refine : (Tape.move Dir.right)^[n] ((Tape.move Dir.left)^[n] (trTape' enc0 (ListBlank.cons R.head L) R.tail)) =
  (Tape.move Dir.right)^[n] (trTape' enc0 L R)
Tactic: refine (Eq.symm ?_).trans (this n _)
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
⊢ (Tape.move Dir.right)^[n] (trTape' enc0 L R) = trTape' enc0 (ListBlank.cons R.head L) R.tail
have suffices : ∀ (i : ℕ) (L : Tape Bool), (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L) = L
Tactic: suffices ∀ i L, (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L) = L by
    refine (Eq.symm ?_).trans (this n _)
    simp only [trTape'_move_left, ListBlank.cons_head_tail, ListBlank.head_cons,
      ListBlank.tail_cons]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
L_1 : Tape Bool
i : ℕ
IH : (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L_1) = L_1
⊢ (Tape.move Dir.right)^[i + 1] ((Tape.move Dir.left)^[i + 1] L_1) = L_1
have succ : (Tape.move Dir.right)^[i] (Tape.move Dir.right ((Tape.move Dir.left)^[i + 1] L_1)) = L_1
Tactic: rw [iterate_succ_apply, iterate_succ_apply', Tape.move_left_right, IH]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
L_1 : Tape Bool
i : ℕ
IH : (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L_1) = L_1
succ : (Tape.move Dir.right)^[i] (Tape.move Dir.right ((Tape.move Dir.left)^[i + 1] L_1)) = L_1
⊢ (Tape.move Dir.right)^[i + 1] ((Tape.move Dir.left)^[i + 1] L_1) = L_1
have succ₁ : (Tape.move Dir.right)^[i] (Tape.move Dir.right (Tape.move Dir.left ((Tape.move Dir.left)^[i] L_1))) = L_1
Tactic: rw [iterate_succ_apply, iterate_succ_apply', Tape.move_left_right, IH]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
Goal:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
L_1 : Tape Bool
i : ℕ
IH : (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L_1) = L_1
succ : (Tape.move Dir.right)^[i] (Tape.move Dir.right ((Tape.move Dir.left)^[i + 1] L_1)) = L_1
succ₁ : (Tape.move Dir.right)^[i] (Tape.move Dir.right (Tape.move Dir.left ((Tape.move Dir.left)^[i] L_1))) = L_1
succ₂ : (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L_1) = L_1
⊢ (Tape.move Dir.right)^[i + 1] ((Tape.move Dir.left)^[i + 1] L_1) = L_1
have succ₃ : L_1 = L_1
Tactic: rw [iterate_succ_apply, iterate_succ_apply', Tape.move_left_right, IH]