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