no goals
α : Type ?u.4109
β : Type u_1
inst✝ : CommMonoid β
n : ℕ
f : Fin (n + 1) → β
x : Fin (n + 1)
⊢ ∏ i : Fin (n + 1), f i = f x * ∏ i : Fin n, f (↑(succAbove x) i)
rw [univ_succAbove, prod_cons, Finset.prod_map _ x.succAbove.toEmbedding,
  RelEmbedding.coe_toEmbedding]