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

case succ
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
i✝ : ℕ
L✝ : ListBlank Γ
n : ℕ
IH : ∀ (i : ℕ) (L : ListBlank Γ), nth (modifyNth f n L) i = if i = n then f (nth L i) else nth L i
i : ℕ
L : ListBlank Γ
⊢ nth (modifyNth f (Nat.succ n) L) i = if i = Nat.succ n then f (nth L i) else nth L i
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
n i : ℕ
L : ListBlank Γ
⊢ nth (modifyNth f n L) i = if i = n then f (nth L i) else nth L i
induction' n with n IH generalizing i L
no goals
case zero
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
i✝ : ℕ
L✝ : ListBlank Γ
i : ℕ
L : ListBlank Γ
⊢ nth (modifyNth f Nat.zero L) i = if i = Nat.zero then f (nth L i) else nth L i
cases i <;> simp only [ListBlank.nth_zero, if_true, ListBlank.head_cons, ListBlank.modifyNth,
  ListBlank.nth_succ, if_false, ListBlank.tail_cons, Nat.zero_eq]
case succ.zero
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
i : ℕ
L✝ : ListBlank Γ
n : ℕ
IH : ∀ (i : ℕ) (L : ListBlank Γ), nth (modifyNth f n L) i = if i = n then f (nth L i) else nth L i
L : ListBlank Γ
⊢ nth (modifyNth f (Nat.succ n) L) Nat.zero = if Nat.zero = Nat.succ n then f (nth L Nat.zero) else nth L Nat.zero

case succ.succ
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
i : ℕ
L✝ : ListBlank Γ
n : ℕ
IH : ∀ (i : ℕ) (L : ListBlank Γ), nth (modifyNth f n L) i = if i = n then f (nth L i) else nth L i
L : ListBlank Γ
n✝ : ℕ
⊢ nth (modifyNth f (Nat.succ n) L) (Nat.succ n✝) =
    if Nat.succ n✝ = Nat.succ n then f (nth L (Nat.succ n✝)) else nth L (Nat.succ n✝)
case succ
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
i✝ : ℕ
L✝ : ListBlank Γ
n : ℕ
IH : ∀ (i : ℕ) (L : ListBlank Γ), nth (modifyNth f n L) i = if i = n then f (nth L i) else nth L i
i : ℕ
L : ListBlank Γ
⊢ nth (modifyNth f (Nat.succ n) L) i = if i = Nat.succ n then f (nth L i) else nth L i
cases i
case succ.zero
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
i : ℕ
L✝ : ListBlank Γ
n : ℕ
IH : ∀ (i : ℕ) (L : ListBlank Γ), nth (modifyNth f n L) i = if i = n then f (nth L i) else nth L i
L : ListBlank Γ
⊢ nth (modifyNth f (Nat.succ n) L) Nat.zero = nth L Nat.zero
case succ.zero
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
i : ℕ
L✝ : ListBlank Γ
n : ℕ
IH : ∀ (i : ℕ) (L : ListBlank Γ), nth (modifyNth f n L) i = if i = n then f (nth L i) else nth L i
L : ListBlank Γ
⊢ nth (modifyNth f (Nat.succ n) L) Nat.zero = if Nat.zero = Nat.succ n then f (nth L Nat.zero) else nth L Nat.zero
rw [if_neg (Nat.succ_ne_zero _).symm]
no goals
case succ.zero
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
i : ℕ
L✝ : ListBlank Γ
n : ℕ
IH : ∀ (i : ℕ) (L : ListBlank Γ), nth (modifyNth f n L) i = if i = n then f (nth L i) else nth L i
L : ListBlank Γ
⊢ nth (modifyNth f (Nat.succ n) L) Nat.zero = nth L Nat.zero
simp only [ListBlank.nth_zero, ListBlank.head_cons, ListBlank.modifyNth, Nat.zero_eq]
no goals
case succ.succ
Γ : Type u_1
inst✝ : Inhabited Γ
f : Γ → Γ
i : ℕ
L✝ : ListBlank Γ
n : ℕ
IH : ∀ (i : ℕ) (L : ListBlank Γ), nth (modifyNth f n L) i = if i = n then f (nth L i) else nth L i
L : ListBlank Γ
n✝ : ℕ
⊢ nth (modifyNth f (Nat.succ n) L) (Nat.succ n✝) =
    if Nat.succ n✝ = Nat.succ n then f (nth L (Nat.succ n✝)) else nth L (Nat.succ n✝)
simp only [IH, ListBlank.modifyNth, ListBlank.nth_succ, ListBlank.tail_cons, Nat.succ.injEq]