α : Type ?u.22461
β : Type u_1
inst✝ : CommMonoid β
f : Fin 5 → β
⊢ f (↑castSucc 0) * f (↑castSucc 1) * f (↑castSucc 2) * f (↑castSucc 3) * f (last 4) = f 0 * f 1 * f 2 * f 3 * f 4
α : Type ?u.22461
β : Type u_1
inst✝ : CommMonoid β
f : Fin 5 → β
⊢ ∏ i : Fin 5, f i = f 0 * f 1 * f 2 * f 3 * f 4
rw [prod_univ_castSucc, prod_univ_four]
no goals
α : Type ?u.22461
β : Type u_1
inst✝ : CommMonoid β
f : Fin 5 → β
⊢ f (↑castSucc 0) * f (↑castSucc 1) * f (↑castSucc 2) * f (↑castSucc 3) * f (last 4) = f 0 * f 1 * f 2 * f 3 * f 4
rfl