-- Mathlib/Computability/PostTuringMachine.lean
theorem trTape'_move_right (L R : ListBlank Γ) :
    (Tape.move Dir.right)^[n] (trTape' enc0 L R) = trTape' enc0 (L.cons R.head) R.tail

Proof state:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = 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] ((Tape.move Dir.left)^[n] (trTape' enc0 (ListBlank.cons R.head L) R.tail)) =
    (Tape.move Dir.right)^[n] (trTape' enc0 L R)

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

Result:
no goals

Proof state:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = 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

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]

Result:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
L R : ListBlank Γ
⊢ ∀ (i : ℕ) (L : Tape Bool), (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L) = L

Proof state:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
L R : ListBlank Γ
this : ∀ (i : ℕ) (L : Tape (?m.108546 i)), (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

Tactic:
refine (Eq.symm ?_).trans (this n _)

Result:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = 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] ((Tape.move Dir.left)^[n] (trTape' enc0 (ListBlank.cons R.head L) R.tail)) =
    (Tape.move Dir.right)^[n] (trTape' enc0 L R)

Proof state:
case zero
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
L R : ListBlank Γ
L✝ : Tape Bool
⊢ (Tape.move Dir.right)^[0] ((Tape.move Dir.left)^[0] L✝) = L✝

Tactic:
rfl

Result:
no goals

Proof state:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
L R : ListBlank Γ
i : ℕ
L✝ : Tape Bool
⊢ (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L✝) = L✝

Tactic:
induction' i with i IH

Result:
case zero
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
L R : ListBlank Γ
L✝ : Tape Bool
⊢ (Tape.move Dir.right)^[0] ((Tape.move Dir.left)^[0] L✝) = L✝

case succ
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
L R : ListBlank Γ
L✝ : Tape Bool
i : ℕ
IH : (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L✝) = L✝
⊢ (Tape.move Dir.right)^[i + 1] ((Tape.move Dir.left)^[i + 1] L✝) = L✝

Proof state:
case succ
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
L R : ListBlank Γ
L✝ : Tape Bool
i : ℕ
IH : (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L✝) = L✝
⊢ (Tape.move Dir.right)^[i + 1] ((Tape.move Dir.left)^[i + 1] L✝) = L✝

Tactic:
rw [iterate_succ_apply, iterate_succ_apply', Tape.move_left_right, IH]

Result:
no goals

Proof state:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
L R : ListBlank Γ
⊢ ∀ (i : ℕ) (L : Tape Bool), (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L) = L

Tactic:
intro i _

Result:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
L R : ListBlank Γ
i : ℕ
L✝ : Tape Bool
⊢ (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L✝) = L✝