case pos
k : ℕ
c : Code
n : ℕ
kn : n < k
⊢ (Option.bind (Option.map (evaln k c) (List.get? (List.range k) n)) fun b => b) = evaln k c n

case neg
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
⊢ (Option.bind (Option.map (evaln k c) (List.get? (List.range k) n)) fun b => b) = evaln k c n
k : ℕ
c : Code
n : ℕ
⊢ (Option.bind (Option.map (evaln k c) (List.get? (List.range k) n)) fun b => b) = evaln k c n
by_cases kn : n < k
no goals
case pos
k : ℕ
c : Code
n : ℕ
kn : n < k
⊢ (Option.bind (Option.map (evaln k c) (List.get? (List.range k) n)) fun b => b) = evaln k c n
simp [List.get?_range kn]
case neg
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
⊢ (Option.bind (Option.map (evaln k c) Option.none) fun b => b) = evaln k c n

case neg
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
⊢ List.length (List.range k) ≤ n
case neg
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
⊢ (Option.bind (Option.map (evaln k c) (List.get? (List.range k) n)) fun b => b) = evaln k c n
rw [List.get?_len_le]
no goals
case neg
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
⊢ List.length (List.range k) ≤ n
simpa using kn
case neg.none
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
e : evaln k c n = Option.none
⊢ (Option.bind (Option.map (evaln k c) Option.none) fun b => b) = Option.none

case neg.some
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
val✝ : ℕ
e : evaln k c n = some val✝
⊢ (Option.bind (Option.map (evaln k c) Option.none) fun b => b) = some val✝
case neg
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
⊢ (Option.bind (Option.map (evaln k c) Option.none) fun b => b) = evaln k c n
cases e : evaln k c n
no goals
case neg.some
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
val✝ : ℕ
e : evaln k c n = some val✝
⊢ (Option.bind (Option.map (evaln k c) Option.none) fun b => b) = some val✝
exact kn.elim (evaln_bound e)
no goals
case neg.none
k : ℕ
c : Code
n : ℕ
kn : ¬n < k
e : evaln k c n = Option.none
⊢ (Option.bind (Option.map (evaln k c) Option.none) fun b => b) = Option.none
rfl