case h.e'_2.h.e'_4
α : Type u_1
β : Type ?u.226607
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
⊢ ofFn f = take n (ofFn f)

case h.e'_3.h
α : Type u_1
β : Type ?u.226607
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
⊢ univ = Finset.filter (fun j => ↑j < n) univ
α : Type u_1
β : Type ?u.226607
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
⊢ prod (ofFn f) = ∏ i : Fin n, f i
convert prod_take_ofFn f n
no goals
case h.e'_2.h.e'_4
α : Type u_1
β : Type ?u.226607
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
⊢ ofFn f = take n (ofFn f)
rw [take_all_of_le (le_of_eq (length_ofFn f))]
no goals
case h.e'_3.h
α : Type u_1
β : Type ?u.226607
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
⊢ univ = Finset.filter (fun j => ↑j < n) univ
simp