case nil
ι : Type ?u.239850
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
b : β
a : α
⊢ get? (scanl f b []) 0 = some b

case cons
ι : Type ?u.239850
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
b : β
a head✝ : α
tail✝ : List α
⊢ get? (scanl f b (head✝ :: tail✝)) 0 = some b
ι : Type ?u.239850
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
b : β
a : α
l : List α
⊢ get? (scanl f b l) 0 = some b
cases l
no goals
case nil
ι : Type ?u.239850
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
b : β
a : α
⊢ get? (scanl f b []) 0 = some b
simp only [get?, scanl_nil]
no goals
case cons
ι : Type ?u.239850
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
b : β
a head✝ : α
tail✝ : List α
⊢ get? (scanl f b (head✝ :: tail✝)) 0 = some b
simp only [get?, scanl_cons, singleton_append]