-- Mathlib/Computability/Tape.lean
theorem ListBlank.nth_modifyNth {Γ} [Inhabited Γ] (f : Γ → Γ) (n i) (L : ListBlank Γ) :
    (L.modifyNth f n).nth i = if i = n then f (L.nth i) else L.nth i

Proof state:
case succ.zero
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
n : ℕ
IH : ∀ (i : ℕ) (L : ListBlank Γ), (modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i
L : ListBlank Γ
⊢ (modifyNth f (n + 1) L).nth 0 = L.nth 0

Tactic:
simp only [ListBlank.nth_zero, ListBlank.head_cons, ListBlank.modifyNth]

Result:
no goals

Proof state:
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
n i : ℕ
L : ListBlank Γ
⊢ (modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i

Tactic:
induction' n with n IH generalizing i L

Result:
case zero
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
i : ℕ
L : ListBlank Γ
⊢ (modifyNth f 0 L).nth i = if i = 0 then f (L.nth i) else L.nth i

case succ
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
n : ℕ
IH : ∀ (i : ℕ) (L : ListBlank Γ), (modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i
i : ℕ
L : ListBlank Γ
⊢ (modifyNth f (n + 1) L).nth i = if i = n + 1 then f (L.nth i) else L.nth i

Proof state:
case zero
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
i : ℕ
L : ListBlank Γ
⊢ (modifyNth f 0 L).nth i = if i = 0 then f (L.nth i) else L.nth i

Tactic:
cases i <;> simp only [ListBlank.nth_zero, if_true, ListBlank.head_cons, ListBlank.modifyNth,
  ListBlank.nth_succ, if_false, ListBlank.tail_cons, reduceCtorEq]

Result:
no goals

Proof state:
case succ.zero
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
n : ℕ
IH : ∀ (i : ℕ) (L : ListBlank Γ), (modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i
L : ListBlank Γ
⊢ (modifyNth f (n + 1) L).nth 0 = if 0 = n + 1 then f (L.nth 0) else L.nth 0

Tactic:
rw [if_neg (Nat.succ_ne_zero _).symm]

Result:
case succ.zero
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
n : ℕ
IH : ∀ (i : ℕ) (L : ListBlank Γ), (modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i
L : ListBlank Γ
⊢ (modifyNth f (n + 1) L).nth 0 = L.nth 0

Proof state:
case succ.succ
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
n : ℕ
IH : ∀ (i : ℕ) (L : ListBlank Γ), (modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i
L : ListBlank Γ
n✝ : ℕ
⊢ (modifyNth f (n + 1) L).nth (n✝ + 1) = if n✝ + 1 = n + 1 then f (L.nth (n✝ + 1)) else L.nth (n✝ + 1)

Tactic:
simp only [IH, ListBlank.modifyNth, ListBlank.nth_succ, ListBlank.tail_cons, Nat.succ.injEq]

Result:
no goals

Proof state:
case succ
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
n : ℕ
IH : ∀ (i : ℕ) (L : ListBlank Γ), (modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i
i : ℕ
L : ListBlank Γ
⊢ (modifyNth f (n + 1) L).nth i = if i = n + 1 then f (L.nth i) else L.nth i

Tactic:
cases i

Result:
case succ.zero
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
n : ℕ
IH : ∀ (i : ℕ) (L : ListBlank Γ), (modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i
L : ListBlank Γ
⊢ (modifyNth f (n + 1) L).nth 0 = if 0 = n + 1 then f (L.nth 0) else L.nth 0

case succ.succ
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
n : ℕ
IH : ∀ (i : ℕ) (L : ListBlank Γ), (modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i
L : ListBlank Γ
n✝ : ℕ
⊢ (modifyNth f (n + 1) L).nth (n✝ + 1) = if n✝ + 1 = n + 1 then f (L.nth (n✝ + 1)) else L.nth (n✝ + 1)