no goals
α : Type ?u.63689
β : Type ?u.63692
M : Type u_1
inst✝ : CommMonoid M
n : ℕ
v : Fin (Nat.succ n) → M
⊢ ∏ i in Ioi 0, v i = ∏ j : Fin n, v (succ j)
rw [Ioi_zero_eq_map, Finset.prod_map, RelEmbedding.coe_toEmbedding, val_succEmbedding]