case nil
ι : Type ?u.240790
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
b✝ : β
a : α
l : List α
i✝ : ℕ
b : β
i : ℕ
⊢ get? (scanl f b []) (i + 1) = Option.bind (get? (scanl f b []) i) fun x => Option.map (fun y => f x y) (get? [] i)

case cons
ι : Type ?u.240790
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
b✝ : β
a : α
l : List α
i✝ : ℕ
hd : α
tl : List α
hl :
  ∀ {b : β} {i : ℕ},
    get? (scanl f b tl) (i + 1) = Option.bind (get? (scanl f b tl) i) fun x => Option.map (fun y => f x y) (get? tl i)
b : β
i : ℕ
⊢ get? (scanl f b (hd :: tl)) (i + 1) =
    Option.bind (get? (scanl f b (hd :: tl)) i) fun x => Option.map (fun y => f x y) (get? (hd :: tl) i)
ι : Type ?u.240790
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
b : β
a : α
l : List α
i : ℕ
⊢ get? (scanl f b l) (i + 1) = Option.bind (get? (scanl f b l) i) fun x => Option.map (fun y => f x y) (get? l i)
induction' l with hd tl hl generalizing b i
case nil
ι : Type ?u.240790
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
b✝ : β
a : α
l : List α
i✝ : ℕ
b : β
i : ℕ
⊢ (Option.bind (get? (scanl f b []) i) fun x => Option.map (fun y => f x y) (get? [] i)) = get? (scanl f b []) (i + 1)
case nil
ι : Type ?u.240790
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
b✝ : β
a : α
l : List α
i✝ : ℕ
b : β
i : ℕ
⊢ get? (scanl f b []) (i + 1) = Option.bind (get? (scanl f b []) i) fun x => Option.map (fun y => f x y) (get? [] i)
symm
no goals
case nil
ι : Type ?u.240790
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
b✝ : β
a : α
l : List α
i✝ : ℕ
b : β
i : ℕ
⊢ (Option.bind (get? (scanl f b []) i) fun x => Option.map (fun y => f x y) (get? [] i)) = get? (scanl f b []) (i + 1)
simp only [Option.bind_eq_none', get?, forall₂_true_iff, not_false_iff, Option.map_none',
  scanl_nil, Option.not_mem_none, forall_true_iff]
case cons
ι : Type ?u.240790
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
b✝ : β
a : α
l : List α
i✝ : ℕ
hd : α
tl : List α
hl :
  ∀ {b : β} {i : ℕ},
    get? (scanl f b tl) (i + 1) = Option.bind (get? (scanl f b tl) i) fun x => Option.map (fun y => f x y) (get? tl i)
b : β
i : ℕ
⊢ get? (b :: scanl f (f b hd) tl) (i + 1) =
    Option.bind (get? (b :: scanl f (f b hd) tl) i) fun x => Option.map (fun y => f x y) (get? (hd :: tl) i)
case cons
ι : Type ?u.240790
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
b✝ : β
a : α
l : List α
i✝ : ℕ
hd : α
tl : List α
hl :
  ∀ {b : β} {i : ℕ},
    get? (scanl f b tl) (i + 1) = Option.bind (get? (scanl f b tl) i) fun x => Option.map (fun y => f x y) (get? tl i)
b : β
i : ℕ
⊢ get? (scanl f b (hd :: tl)) (i + 1) =
    Option.bind (get? (scanl f b (hd :: tl)) i) fun x => Option.map (fun y => f x y) (get? (hd :: tl) i)
simp only [scanl_cons, singleton_append]
case cons.zero
ι : Type ?u.240790
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
b✝ : β
a : α
l : List α
i : ℕ
hd : α
tl : List α
hl :
  ∀ {b : β} {i : ℕ},
    get? (scanl f b tl) (i + 1) = Option.bind (get? (scanl f b tl) i) fun x => Option.map (fun y => f x y) (get? tl i)
b : β
⊢ get? (b :: scanl f (f b hd) tl) (zero + 1) =
    Option.bind (get? (b :: scanl f (f b hd) tl) zero) fun x => Option.map (fun y => f x y) (get? (hd :: tl) zero)

case cons.succ
ι : Type ?u.240790
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
b✝ : β
a : α
l : List α
i : ℕ
hd : α
tl : List α
hl :
  ∀ {b : β} {i : ℕ},
    get? (scanl f b tl) (i + 1) = Option.bind (get? (scanl f b tl) i) fun x => Option.map (fun y => f x y) (get? tl i)
b : β
n✝ : ℕ
⊢ get? (b :: scanl f (f b hd) tl) (succ n✝ + 1) =
    Option.bind (get? (b :: scanl f (f b hd) tl) (succ n✝)) fun x =>
      Option.map (fun y => f x y) (get? (hd :: tl) (succ n✝))
case cons
ι : Type ?u.240790
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
b✝ : β
a : α
l : List α
i✝ : ℕ
hd : α
tl : List α
hl :
  ∀ {b : β} {i : ℕ},
    get? (scanl f b tl) (i + 1) = Option.bind (get? (scanl f b tl) i) fun x => Option.map (fun y => f x y) (get? tl i)
b : β
i : ℕ
⊢ get? (b :: scanl f (f b hd) tl) (i + 1) =
    Option.bind (get? (b :: scanl f (f b hd) tl) i) fun x => Option.map (fun y => f x y) (get? (hd :: tl) i)
cases i
no goals
case cons.zero
ι : Type ?u.240790
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
b✝ : β
a : α
l : List α
i : ℕ
hd : α
tl : List α
hl :
  ∀ {b : β} {i : ℕ},
    get? (scanl f b tl) (i + 1) = Option.bind (get? (scanl f b tl) i) fun x => Option.map (fun y => f x y) (get? tl i)
b : β
⊢ get? (b :: scanl f (f b hd) tl) (zero + 1) =
    Option.bind (get? (b :: scanl f (f b hd) tl) zero) fun x => Option.map (fun y => f x y) (get? (hd :: tl) zero)
simp only [Option.map_some', get?_zero_scanl, get?, Option.some_bind']
no goals
case cons.succ
ι : Type ?u.240790
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
b✝ : β
a : α
l : List α
i : ℕ
hd : α
tl : List α
hl :
  ∀ {b : β} {i : ℕ},
    get? (scanl f b tl) (i + 1) = Option.bind (get? (scanl f b tl) i) fun x => Option.map (fun y => f x y) (get? tl i)
b : β
n✝ : ℕ
⊢ get? (b :: scanl f (f b hd) tl) (succ n✝ + 1) =
    Option.bind (get? (b :: scanl f (f b hd) tl) (succ n✝)) fun x =>
      Option.map (fun y => f x y) (get? (hd :: tl) (succ n✝))
simp only [hl, get?]