n : ℕ
α : Type u_1
β : Type ?u.60631
γ : Type ?u.60634
inst✝ : Monoid α
v : Vector α n
i : Fin n
a : α
⊢ (List.prod (List.take (↑i) (toList v)) * if ↑i < List.length (toList v) then a else 1) *
      List.prod (List.drop (↑i + 1) (toList v)) =
    List.prod (toList (take (↑i) v)) * a * List.prod (toList (drop (↑i + 1) v))
n : ℕ
α : Type u_1
β : Type ?u.60631
γ : Type ?u.60634
inst✝ : Monoid α
v : Vector α n
i : Fin n
a : α
⊢ List.prod (toList (set v i a)) = List.prod (toList (take (↑i) v)) * a * List.prod (toList (drop (↑i + 1) v))
refine' (List.prod_set v.toList i a).trans _
no goals
n : ℕ
α : Type u_1
β : Type ?u.60631
γ : Type ?u.60634
inst✝ : Monoid α
v : Vector α n
i : Fin n
a : α
⊢ (List.prod (List.take (↑i) (toList v)) * if ↑i < List.length (toList v) then a else 1) *
      List.prod (List.drop (↑i + 1) (toList v)) =
    List.prod (toList (take (↑i) v)) * a * List.prod (toList (drop (↑i + 1) v))
simp_all