case zero
Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
⊢ ((move Dir.right^[Nat.zero]) T).head = nth T ↑Nat.zero

case succ
Γ : Type u_1
inst✝ : Inhabited Γ
n✝ : ℕ
n_ih✝ : ∀ (T : Tape Γ), ((move Dir.right^[n✝]) T).head = nth T ↑n✝
T : Tape Γ
⊢ ((move Dir.right^[Nat.succ n✝]) T).head = nth T ↑(Nat.succ n✝)
Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
i : ℕ
⊢ ((move Dir.right^[i]) T).head = nth T ↑i
induction i generalizing T
no goals
case zero
Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
⊢ ((move Dir.right^[Nat.zero]) T).head = nth T ↑Nat.zero
rfl
no goals
case succ
Γ : Type u_1
inst✝ : Inhabited Γ
n✝ : ℕ
n_ih✝ : ∀ (T : Tape Γ), ((move Dir.right^[n✝]) T).head = nth T ↑n✝
T : Tape Γ
⊢ ((move Dir.right^[Nat.succ n✝]) T).head = nth T ↑(Nat.succ n✝)
simp only [*, Tape.move_right_nth, Int.ofNat_succ, iterate_succ, Function.comp_apply]