no goals
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
n : ℕ
fι : Fin n → ι
fA : (a : Fin n) → A (fι a)
⊢ List.prod (List.ofFn fun a => ↑(of A (fι a)) (fA a)) =
    ↑(of A (List.dProdIndex (List.finRange n) fι)) (List.dProd (List.finRange n) fι fA)
rw [List.ofFn_eq_map, ofList_dProd]