case zero
α : Type u_2
β : Type u_1
f : β → α → β
b : β
v : Vector α Nat.zero
i : Fin Nat.zero
⊢ get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (↑Fin.castSucc i)) (get v i)

case succ
α : Type u_2
β : Type u_1
f : β → α → β
b : β
n : ℕ
v : Vector α (Nat.succ n)
i : Fin (Nat.succ n)
⊢ get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (↑Fin.castSucc i)) (get v i)
n : ℕ
α : Type u_2
β : Type u_1
f : β → α → β
b : β
v : Vector α n
i : Fin n
⊢ get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (↑Fin.castSucc i)) (get v i)
cases' n with n
case succ.zero
α : Type u_2
β : Type u_1
f : β → α → β
b✝ : β
n : ℕ
v✝ : Vector α (Nat.succ n)
i✝ : Fin (Nat.succ n)
b : β
v : Vector α (Nat.succ Nat.zero)
i : Fin (Nat.succ Nat.zero)
⊢ get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (↑Fin.castSucc i)) (get v i)

case succ.succ
α : Type u_2
β : Type u_1
f : β → α → β
b✝ : β
n✝ : ℕ
v✝ : Vector α (Nat.succ n✝)
i✝ : Fin (Nat.succ n✝)
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (Nat.succ n)) (i : Fin (Nat.succ n)),
    get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (↑Fin.castSucc i)) (get v i)
b : β
v : Vector α (Nat.succ (Nat.succ n))
i : Fin (Nat.succ (Nat.succ n))
⊢ get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (↑Fin.castSucc i)) (get v i)
case succ
α : Type u_2
β : Type u_1
f : β → α → β
b : β
n : ℕ
v : Vector α (Nat.succ n)
i : Fin (Nat.succ n)
⊢ get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (↑Fin.castSucc i)) (get v i)
induction' n with n hn generalizing b
no goals
case zero
α : Type u_2
β : Type u_1
f : β → α → β
b : β
v : Vector α Nat.zero
i : Fin Nat.zero
⊢ get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (↑Fin.castSucc i)) (get v i)
exact i.elim0
case succ.zero
α : Type u_2
β : Type u_1
f : β → α → β
b✝ : β
n : ℕ
v✝ : Vector α (Nat.succ n)
i✝ : Fin (Nat.succ n)
b : β
v : Vector α (Nat.succ Nat.zero)
i : Fin (Nat.succ Nat.zero)
i0 : i = 0
⊢ get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (↑Fin.castSucc i)) (get v i)
case succ.zero
α : Type u_2
β : Type u_1
f : β → α → β
b✝ : β
n : ℕ
v✝ : Vector α (Nat.succ n)
i✝ : Fin (Nat.succ n)
b : β
v : Vector α (Nat.succ Nat.zero)
i : Fin (Nat.succ Nat.zero)
⊢ get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (↑Fin.castSucc i)) (get v i)
have i0 : i = 0 := Fin.eq_zero _
case succ.zero
α : Type u_2
β : Type u_1
f : β → α → β
b✝ : β
n : ℕ
v✝ : Vector α (Nat.succ n)
i✝ : Fin (Nat.succ n)
b : β
v : Vector α (Nat.succ Nat.zero)
i : Fin (Nat.succ Nat.zero)
i0 : i = 0
⊢ get (b ::ᵥ f b (head v) ::ᵥ nil) 1 = f b (head v)
case succ.zero
α : Type u_2
β : Type u_1
f : β → α → β
b✝ : β
n : ℕ
v✝ : Vector α (Nat.succ n)
i✝ : Fin (Nat.succ n)
b : β
v : Vector α (Nat.succ Nat.zero)
i : Fin (Nat.succ Nat.zero)
i0 : i = 0
⊢ get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (↑Fin.castSucc i)) (get v i)
simp [scanl_singleton, i0, get_zero]
no goals
case succ.zero
α : Type u_2
β : Type u_1
f : β → α → β
b✝ : β
n : ℕ
v✝ : Vector α (Nat.succ n)
i✝ : Fin (Nat.succ n)
b : β
v : Vector α (Nat.succ Nat.zero)
i : Fin (Nat.succ Nat.zero)
i0 : i = 0
⊢ get (b ::ᵥ f b (head v) ::ᵥ nil) 1 = f b (head v)
simp [get_eq_get]
case succ.succ
α : Type u_2
β : Type u_1
f : β → α → β
b✝ : β
n✝ : ℕ
v✝ : Vector α (Nat.succ n✝)
i✝ : Fin (Nat.succ n✝)
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (Nat.succ n)) (i : Fin (Nat.succ n)),
    get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (↑Fin.castSucc i)) (get v i)
b : β
v : Vector α (Nat.succ (Nat.succ n))
i : Fin (Nat.succ (Nat.succ n))
⊢ get (scanl f (f b (head v)) (tail v)) i =
    f (get (b ::ᵥ scanl f (f b (head v)) (tail v)) (↑Fin.castSucc i)) (get (head v ::ᵥ tail v) i)
case succ.succ
α : Type u_2
β : Type u_1
f : β → α → β
b✝ : β
n✝ : ℕ
v✝ : Vector α (Nat.succ n✝)
i✝ : Fin (Nat.succ n✝)
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (Nat.succ n)) (i : Fin (Nat.succ n)),
    get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (↑Fin.castSucc i)) (get v i)
b : β
v : Vector α (Nat.succ (Nat.succ n))
i : Fin (Nat.succ (Nat.succ n))
⊢ get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (↑Fin.castSucc i)) (get v i)
rw [← cons_head_tail v, scanl_cons, get_cons_succ]
case succ.succ.refine'_1
α : Type u_2
β : Type u_1
f : β → α → β
b✝ : β
n✝ : ℕ
v✝ : Vector α (Nat.succ n✝)
i✝ : Fin (Nat.succ n✝)
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (Nat.succ n)) (i : Fin (Nat.succ n)),
    get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (↑Fin.castSucc i)) (get v i)
b : β
v : Vector α (Nat.succ (Nat.succ n))
i : Fin (Nat.succ (Nat.succ n))
⊢ get (scanl f (f b (head v)) (tail v)) 0 =
    f (get (b ::ᵥ scanl f (f b (head v)) (tail v)) (↑Fin.castSucc 0)) (get (head v ::ᵥ tail v) 0)

case succ.succ.refine'_2
α : Type u_2
β : Type u_1
f : β → α → β
b✝ : β
n✝ : ℕ
v✝ : Vector α (Nat.succ n✝)
i✝ : Fin (Nat.succ n✝)
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (Nat.succ n)) (i : Fin (Nat.succ n)),
    get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (↑Fin.castSucc i)) (get v i)
b : β
v : Vector α (Nat.succ (Nat.succ n))
i : Fin (Nat.succ (Nat.succ n))
⊢ ∀ (i : Fin (n + 1)),
    get (scanl f (f b (head v)) (tail v)) (Fin.succ i) =
      f (get (b ::ᵥ scanl f (f b (head v)) (tail v)) (↑Fin.castSucc (Fin.succ i)))
        (get (head v ::ᵥ tail v) (Fin.succ i))
case succ.succ
α : Type u_2
β : Type u_1
f : β → α → β
b✝ : β
n✝ : ℕ
v✝ : Vector α (Nat.succ n✝)
i✝ : Fin (Nat.succ n✝)
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (Nat.succ n)) (i : Fin (Nat.succ n)),
    get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (↑Fin.castSucc i)) (get v i)
b : β
v : Vector α (Nat.succ (Nat.succ n))
i : Fin (Nat.succ (Nat.succ n))
⊢ get (scanl f (f b (head v)) (tail v)) i =
    f (get (b ::ᵥ scanl f (f b (head v)) (tail v)) (↑Fin.castSucc i)) (get (head v ::ᵥ tail v) i)
refine' Fin.cases _ _ i
no goals
case succ.succ.refine'_1
α : Type u_2
β : Type u_1
f : β → α → β
b✝ : β
n✝ : ℕ
v✝ : Vector α (Nat.succ n✝)
i✝ : Fin (Nat.succ n✝)
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (Nat.succ n)) (i : Fin (Nat.succ n)),
    get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (↑Fin.castSucc i)) (get v i)
b : β
v : Vector α (Nat.succ (Nat.succ n))
i : Fin (Nat.succ (Nat.succ n))
⊢ get (scanl f (f b (head v)) (tail v)) 0 =
    f (get (b ::ᵥ scanl f (f b (head v)) (tail v)) (↑Fin.castSucc 0)) (get (head v ::ᵥ tail v) 0)
simp only [get_zero, scanl_head, Fin.castSucc_zero, head_cons]
case succ.succ.refine'_2
α : Type u_2
β : Type u_1
f : β → α → β
b✝ : β
n✝ : ℕ
v✝ : Vector α (Nat.succ n✝)
i✝ : Fin (Nat.succ n✝)
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (Nat.succ n)) (i : Fin (Nat.succ n)),
    get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (↑Fin.castSucc i)) (get v i)
b : β
v : Vector α (Nat.succ (Nat.succ n))
i : Fin (Nat.succ (Nat.succ n))
i' : Fin (n + 1)
⊢ get (scanl f (f b (head v)) (tail v)) (Fin.succ i') =
    f (get (b ::ᵥ scanl f (f b (head v)) (tail v)) (↑Fin.castSucc (Fin.succ i')))
      (get (head v ::ᵥ tail v) (Fin.succ i'))
case succ.succ.refine'_2
α : Type u_2
β : Type u_1
f : β → α → β
b✝ : β
n✝ : ℕ
v✝ : Vector α (Nat.succ n✝)
i✝ : Fin (Nat.succ n✝)
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (Nat.succ n)) (i : Fin (Nat.succ n)),
    get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (↑Fin.castSucc i)) (get v i)
b : β
v : Vector α (Nat.succ (Nat.succ n))
i : Fin (Nat.succ (Nat.succ n))
⊢ ∀ (i : Fin (n + 1)),
    get (scanl f (f b (head v)) (tail v)) (Fin.succ i) =
      f (get (b ::ᵥ scanl f (f b (head v)) (tail v)) (↑Fin.castSucc (Fin.succ i)))
        (get (head v ::ᵥ tail v) (Fin.succ i))
intro i'
no goals
case succ.succ.refine'_2
α : Type u_2
β : Type u_1
f : β → α → β
b✝ : β
n✝ : ℕ
v✝ : Vector α (Nat.succ n✝)
i✝ : Fin (Nat.succ n✝)
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (Nat.succ n)) (i : Fin (Nat.succ n)),
    get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (↑Fin.castSucc i)) (get v i)
b : β
v : Vector α (Nat.succ (Nat.succ n))
i : Fin (Nat.succ (Nat.succ n))
i' : Fin (n + 1)
⊢ get (scanl f (f b (head v)) (tail v)) (Fin.succ i') =
    f (get (b ::ᵥ scanl f (f b (head v)) (tail v)) (↑Fin.castSucc (Fin.succ i')))
      (get (head v ::ᵥ tail v) (Fin.succ i'))
simp only [hn, Fin.castSucc_fin_succ, get_cons_succ]