n : ℕ
α : Type u_1
β : Type ?u.63254
γ : Type ?u.63257
inst✝ : CommGroup α
v : Vector α n
i : Fin n
a : α
⊢ (List.prod (toList v) * if hn : ↑i < List.length (toList v) then (List.nthLe (toList v) (↑i) hn)⁻¹ * a else 1) =
    List.prod (toList v) * (get v i)⁻¹ * a
n : ℕ
α : Type u_1
β : Type ?u.63254
γ : Type ?u.63257
inst✝ : CommGroup α
v : Vector α n
i : Fin n
a : α
⊢ List.prod (toList (set v i a)) = List.prod (toList v) * (get v i)⁻¹ * a
refine' (List.prod_set' v.toList i a).trans _
n : ℕ
α : Type u_1
β : Type ?u.63254
γ : Type ?u.63257
inst✝ : CommGroup α
v : Vector α n
i : Fin n
a : α
⊢ List.nthLe (toList v) ↑i (_ : ↑i < List.length (toList v)) =
    List.get (toList v) (↑(Fin.cast (_ : n = List.length (toList v))) i)
n : ℕ
α : Type u_1
β : Type ?u.63254
γ : Type ?u.63257
inst✝ : CommGroup α
v : Vector α n
i : Fin n
a : α
⊢ (List.prod (toList v) * if hn : ↑i < List.length (toList v) then (List.nthLe (toList v) (↑i) hn)⁻¹ * a else 1) =
    List.prod (toList v) * (get v i)⁻¹ * a
simp [get_eq_get, mul_assoc]
no goals
n : ℕ
α : Type u_1
β : Type ?u.63254
γ : Type ?u.63257
inst✝ : CommGroup α
v : Vector α n
i : Fin n
a : α
⊢ List.nthLe (toList v) ↑i (_ : ↑i < List.length (toList v)) =
    List.get (toList v) (↑(Fin.cast (_ : n = List.length (toList v))) i)
rfl