no goals
α : Type u_1
β : Type ?u.87636
inst✝ : Monoid α
n : ℕ
f : Fin n → α
j : Fin n
⊢ partialProd f (succ j) = partialProd f (↑castSucc j) * f j
simp [partialProd, List.take_succ, List.ofFnNthVal, dif_pos j.is_lt, ← Option.coe_def]