case nil
ι : Type ?u.240201
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : β → α → β
b : β
a : α
h : 0 < length (scanl f b [])
⊢ get (scanl f b []) { val := 0, isLt := h } = b

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