case zero
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
L✝ R✝ L R : ListBlank Γ
⊢ write (f (ListBlank.nth R Nat.zero)) ((move Dir.right^[Nat.zero]) (mk' L R)) =
    (move Dir.right^[Nat.zero]) (mk' L (ListBlank.modifyNth f Nat.zero R))

case succ
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
L✝ R✝ : ListBlank Γ
n : ℕ
IH :
  ∀ (L R : ListBlank Γ),
    write (f (ListBlank.nth R n)) ((move Dir.right^[n]) (mk' L R)) =
      (move Dir.right^[n]) (mk' L (ListBlank.modifyNth f n R))
L R : ListBlank Γ
⊢ write (f (ListBlank.nth R (Nat.succ n))) ((move Dir.right^[Nat.succ n]) (mk' L R)) =
    (move Dir.right^[Nat.succ n]) (mk' L (ListBlank.modifyNth f (Nat.succ n) R))
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
L R : ListBlank Γ
n : ℕ
⊢ write (f (ListBlank.nth R n)) ((move Dir.right^[n]) (mk' L R)) =
    (move Dir.right^[n]) (mk' L (ListBlank.modifyNth f n R))
induction' n with n IH generalizing L R
no goals
case succ
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
L✝ R✝ : ListBlank Γ
n : ℕ
IH :
  ∀ (L R : ListBlank Γ),
    write (f (ListBlank.nth R n)) ((move Dir.right^[n]) (mk' L R)) =
      (move Dir.right^[n]) (mk' L (ListBlank.modifyNth f n R))
L R : ListBlank Γ
⊢ write (f (ListBlank.nth R (Nat.succ n))) ((move Dir.right^[Nat.succ n]) (mk' L R)) =
    (move Dir.right^[Nat.succ n]) (mk' L (ListBlank.modifyNth f (Nat.succ n) R))
simp only [ListBlank.head_cons, ListBlank.nth_succ, ListBlank.modifyNth, Tape.move_right_mk',
  ListBlank.tail_cons, iterate_succ_apply, IH]
case zero
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
L✝ R✝ L R : ListBlank Γ
⊢ write (f (ListBlank.head R)) (mk' L R) = mk' L (ListBlank.cons (f (ListBlank.head R)) (ListBlank.tail R))
case zero
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
L✝ R✝ L R : ListBlank Γ
⊢ write (f (ListBlank.nth R Nat.zero)) ((move Dir.right^[Nat.zero]) (mk' L R)) =
    (move Dir.right^[Nat.zero]) (mk' L (ListBlank.modifyNth f Nat.zero R))
simp only [ListBlank.nth_zero, ListBlank.modifyNth, iterate_zero_apply, Nat.zero_eq]
no goals
case zero
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
L✝ R✝ L R : ListBlank Γ
⊢ write (f (ListBlank.head R)) (mk' L R) = mk' L (ListBlank.cons (f (ListBlank.head R)) (ListBlank.tail R))
rw [← Tape.write_mk', ListBlank.cons_head_tail]