no goals
α : Type u_1
f : α → α
n : Nat
l : List α
⊢ get? (modifyNth f n l) 0 = (fun a => if n = 0 then f a else a) <$> get? l 0
cases l <;> cases n <;> rfl
no goals
α : Type u_1
f : α → α
n n✝ : Nat
⊢ get? (modifyNth f n []) (n✝ + 1) = (fun a => if n = n✝ + 1 then f a else a) <$> get? [] (n✝ + 1)
cases n <;> rfl
no goals
α : Type u_1
f : α → α
head✝ : α
l : List α
m : Nat
⊢ get? (modifyNth f 0 (head✝ :: l)) (m + 1) = (fun a => if 0 = m + 1 then f a else a) <$> get? (head✝ :: l) (m + 1)
cases l.get? m <;> rfl
no goals
α : Type u_1
f : α → α
n : Nat
a : α
l : List α
m : Nat
⊢ (fun a => if n = m then f a else a) <$> get? l m =
    (fun a => if n + 1 = m + 1 then f a else a) <$> get? (a :: l) (m + 1)
cases l.get? m <;> by_cases h : n = m <;>
  simp only [h, if_pos, if_true, if_false, Option.map, mt Nat.succ.inj, not_false_iff]