case zero
α : Type u_2
β : Type u_1
f : β → α → β
b : β
v : Vector α Nat.zero
⊢ head (scanl f b v) = b

case succ
α : Type u_2
β : Type u_1
f : β → α → β
b : β
n✝ : ℕ
v : Vector α (Nat.succ n✝)
⊢ head (scanl f b v) = b
n : ℕ
α : Type u_2
β : Type u_1
f : β → α → β
b : β
v : Vector α n
⊢ head (scanl f b v) = b
cases n
case zero
α : Type u_2
β : Type u_1
f : β → α → β
b : β
v : Vector α Nat.zero
this : v = nil
⊢ head (scanl f b v) = b
case zero
α : Type u_2
β : Type u_1
f : β → α → β
b : β
v : Vector α Nat.zero
⊢ head (scanl f b v) = b
have : v = nil := by simp only [Nat.zero_eq, eq_iff_true_of_subsingleton]
no goals
case zero
α : Type u_2
β : Type u_1
f : β → α → β
b : β
v : Vector α Nat.zero
this : v = nil
⊢ head (scanl f b v) = b
simp only [this, scanl_nil, head_cons]
no goals
α : Type u_2
β : Type u_1
f : β → α → β
b : β
v : Vector α Nat.zero
⊢ v = nil
simp only [Nat.zero_eq, eq_iff_true_of_subsingleton]
case succ
α : Type u_2
β : Type u_1
f : β → α → β
b : β
n✝ : ℕ
v : Vector α (Nat.succ n✝)
⊢ head (scanl f b (head v ::ᵥ tail v)) = b
case succ
α : Type u_2
β : Type u_1
f : β → α → β
b : β
n✝ : ℕ
v : Vector α (Nat.succ n✝)
⊢ head (scanl f b v) = b
rw [← cons_head_tail v]
no goals
case succ
α : Type u_2
β : Type u_1
f : β → α → β
b : β
n✝ : ℕ
v : Vector α (Nat.succ n✝)
⊢ head (scanl f b (head v ::ᵥ tail v)) = b
simp only [← get_zero, get_eq_get, toList_scanl, toList_cons, List.scanl, Fin.val_zero,
  List.get]