α : Type u_1
β : Type ?u.93394
inst✝ : Monoid α
n : ℕ
f : Fin (n + 1) → α
j : Fin (n + 1)
⊢ f 0 * List.prod (List.take (↑j) (List.ofFn fun i => f (succ i))) =
    f 0 * List.prod (List.take (↑j) (List.ofFn (tail f)))
α : Type u_1
β : Type ?u.93394
inst✝ : Monoid α
n : ℕ
f : Fin (n + 1) → α
j : Fin (n + 1)
⊢ partialProd f (succ j) = f 0 * partialProd (tail f) j
simp [partialProd]
no goals
α : Type u_1
β : Type ?u.93394
inst✝ : Monoid α
n : ℕ
f : Fin (n + 1) → α
j : Fin (n + 1)
⊢ f 0 * List.prod (List.take (↑j) (List.ofFn fun i => f (succ i))) =
    f 0 * List.prod (List.take (↑j) (List.ofFn (tail f)))
rfl