-- Mathlib/Data/List/Scan.lean
theorem getElem?_succ_scanl {i : ℕ} : (scanl f b l)[i + 1]? =
    (scanl f b l)[i]?.bind fun x => l[i]?.map fun y => f x y

Proof state:
case cons
α : Type u_1
β : Type u_2
f : β → α → β
hd : α
tl : List α
hl : ∀ {b : β} {i : ℕ}, (scanl f b tl)[i + 1]? = (scanl f b tl)[i]?.bind fun x => Option.map (fun y => f x y) tl[i]?
b : β
i : ℕ
⊢ (b :: scanl f (f b hd) tl)[i + 1]? =
    (b :: scanl f (f b hd) tl)[i]?.bind fun a => Option.map (fun y => f a y) (hd :: tl)[i]?

Tactic:
cases i

Result:
case cons.zero
α : Type u_1
β : Type u_2
f : β → α → β
hd : α
tl : List α
hl : ∀ {b : β} {i : ℕ}, (scanl f b tl)[i + 1]? = (scanl f b tl)[i]?.bind fun x => Option.map (fun y => f x y) tl[i]?
b : β
⊢ (b :: scanl f (f b hd) tl)[0 + 1]? =
    (b :: scanl f (f b hd) tl)[0]?.bind fun a => Option.map (fun y => f a y) (hd :: tl)[0]?

case cons.succ
α : Type u_1
β : Type u_2
f : β → α → β
hd : α
tl : List α
hl : ∀ {b : β} {i : ℕ}, (scanl f b tl)[i + 1]? = (scanl f b tl)[i]?.bind fun x => Option.map (fun y => f x y) tl[i]?
b : β
n✝ : ℕ
⊢ (b :: scanl f (f b hd) tl)[n✝ + 1 + 1]? =
    (b :: scanl f (f b hd) tl)[n✝ + 1]?.bind fun a => Option.map (fun y => f a y) (hd :: tl)[n✝ + 1]?

Proof state:
case cons.zero
α : Type u_1
β : Type u_2
f : β → α → β
hd : α
tl : List α
hl : ∀ {b : β} {i : ℕ}, (scanl f b tl)[i + 1]? = (scanl f b tl)[i]?.bind fun x => Option.map (fun y => f x y) tl[i]?
b : β
⊢ (b :: scanl f (f b hd) tl)[0 + 1]? =
    (b :: scanl f (f b hd) tl)[0]?.bind fun a => Option.map (fun y => f a y) (hd :: tl)[0]?

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : β → α → β
b : β
l : List α
i : ℕ
⊢ (scanl f b l)[i + 1]? = (scanl f b l)[i]?.bind fun x => Option.map (fun y => f x y) l[i]?

Tactic:
induction' l with hd tl hl generalizing b i

Result:
case nil
α : Type u_1
β : Type u_2
f : β → α → β
b : β
i : ℕ
⊢ (scanl f b [])[i + 1]? = (scanl f b [])[i]?.bind fun x => Option.map (fun y => f x y) [][i]?

case cons
α : Type u_1
β : Type u_2
f : β → α → β
hd : α
tl : List α
hl : ∀ {b : β} {i : ℕ}, (scanl f b tl)[i + 1]? = (scanl f b tl)[i]?.bind fun x => Option.map (fun y => f x y) tl[i]?
b : β
i : ℕ
⊢ (scanl f b (hd :: tl))[i + 1]? = (scanl f b (hd :: tl))[i]?.bind fun x => Option.map (fun y => f x y) (hd :: tl)[i]?

Proof state:
case nil
α : Type u_1
β : Type u_2
f : β → α → β
b : β
i : ℕ
⊢ ((scanl f b [])[i]?.bind fun x => Option.map (fun y => f x y) [][i]?) = (scanl f b [])[i + 1]?

Tactic:
simp only [scanl, getElem?_nil, Option.map_none', Option.bind_none, getElem?_cons_succ]

Result:
no goals

Proof state:
case cons.succ
α : Type u_1
β : Type u_2
f : β → α → β
hd : α
tl : List α
hl : ∀ {b : β} {i : ℕ}, (scanl f b tl)[i + 1]? = (scanl f b tl)[i]?.bind fun x => Option.map (fun y => f x y) tl[i]?
b : β
n✝ : ℕ
⊢ (b :: scanl f (f b hd) tl)[n✝ + 1 + 1]? =
    (b :: scanl f (f b hd) tl)[n✝ + 1]?.bind fun a => Option.map (fun y => f a y) (hd :: tl)[n✝ + 1]?

Tactic:
simp only [hl, getElem?_cons_succ]

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
f : β → α → β
b : β
i : ℕ
⊢ (scanl f b [])[i + 1]? = (scanl f b [])[i]?.bind fun x => Option.map (fun y => f x y) [][i]?

Tactic:
symm

Result:
case nil
α : Type u_1
β : Type u_2
f : β → α → β
b : β
i : ℕ
⊢ ((scanl f b [])[i]?.bind fun x => Option.map (fun y => f x y) [][i]?) = (scanl f b [])[i + 1]?

Proof state:
case cons
α : Type u_1
β : Type u_2
f : β → α → β
hd : α
tl : List α
hl : ∀ {b : β} {i : ℕ}, (scanl f b tl)[i + 1]? = (scanl f b tl)[i]?.bind fun x => Option.map (fun y => f x y) tl[i]?
b : β
i : ℕ
⊢ (scanl f b (hd :: tl))[i + 1]? = (scanl f b (hd :: tl))[i]?.bind fun x => Option.map (fun y => f x y) (hd :: tl)[i]?

Tactic:
simp only [scanl_cons, singleton_append]

Result:
case cons
α : Type u_1
β : Type u_2
f : β → α → β
hd : α
tl : List α
hl : ∀ {b : β} {i : ℕ}, (scanl f b tl)[i + 1]? = (scanl f b tl)[i]?.bind fun x => Option.map (fun y => f x y) tl[i]?
b : β
i : ℕ
⊢ (b :: scanl f (f b hd) tl)[i + 1]? =
    (b :: scanl f (f b hd) tl)[i]?.bind fun a => Option.map (fun y => f a y) (hd :: tl)[i]?