n : ℕ
α : Type u_2
β : Type u_1
f : β → α → β
b : β
v : Vector α n
x : α
⊢ { val := b :: List.scanl f (f b x) ↑v,
      property := (_ : (fun l => List.length l = Nat.succ n + 1) (b :: List.scanl f (f b x) ↑v)) } =
    b ::ᵥ
      { val := List.scanl f (f b x) (toList v),
        property := (_ : List.length (List.scanl f (f b x) (toList v)) = n + 1) }
n : ℕ
α : Type u_2
β : Type u_1
f : β → α → β
b : β
v : Vector α n
x : α
⊢ scanl f b (x ::ᵥ v) = b ::ᵥ scanl f (f b x) v
simp only [scanl, toList_cons, List.scanl]
n : ℕ
α : Type u_2
β : Type u_1
f : β → α → β
b : β
v : Vector α n
x : α
⊢ { val := b :: List.scanl f (f b x) ↑v,
      property := (_ : List.length (List.scanl f b (toList (x ::ᵥ v))) = Nat.succ n + 1) } =
    b ::ᵥ
      { val := List.scanl f (f b x) (toList v),
        property := (_ : List.length (List.scanl f (f b x) (toList v)) = n + 1) }
n : ℕ
α : Type u_2
β : Type u_1
f : β → α → β
b : β
v : Vector α n
x : α
⊢ { val := b :: List.scanl f (f b x) ↑v,
      property := (_ : (fun l => List.length l = Nat.succ n + 1) (b :: List.scanl f (f b x) ↑v)) } =
    b ::ᵥ
      { val := List.scanl f (f b x) (toList v),
        property := (_ : List.length (List.scanl f (f b x) (toList v)) = n + 1) }
dsimp
n : ℕ
α : Type u_2
β : Type u_1
f : β → α → β
b : β
v : Vector α n
x : α
⊢ { val := b :: List.scanl f (f b x) ↑v,
      property := (_ : List.length (List.scanl f b (toList (x ::ᵥ v))) = Nat.succ n + 1) } =
    { val := b :: List.scanl f (f b x) (toList v),
      property := (_ : Nat.succ (List.length (List.scanl f (f b x) (toList v))) = Nat.succ (n + 1)) }
n : ℕ
α : Type u_2
β : Type u_1
f : β → α → β
b : β
v : Vector α n
x : α
⊢ { val := b :: List.scanl f (f b x) ↑v,
      property := (_ : List.length (List.scanl f b (toList (x ::ᵥ v))) = Nat.succ n + 1) } =
    b ::ᵥ
      { val := List.scanl f (f b x) (toList v),
        property := (_ : List.length (List.scanl f (f b x) (toList v)) = n + 1) }
simp only [cons]
no goals
n : ℕ
α : Type u_2
β : Type u_1
f : β → α → β
b : β
v : Vector α n
x : α
⊢ { val := b :: List.scanl f (f b x) ↑v,
      property := (_ : List.length (List.scanl f b (toList (x ::ᵥ v))) = Nat.succ n + 1) } =
    { val := b :: List.scanl f (f b x) (toList v),
      property := (_ : Nat.succ (List.length (List.scanl f (f b x) (toList v))) = Nat.succ (n + 1)) }
rfl