no goals
ι : Type u_1
α : Type ?u.51491
A : ι → Type u_2
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
n : ℕ
f : Fin n → GradedMonoid A
⊢ List.prod (List.ofFn f) =
    mk (List.dProdIndex (List.finRange n) fun i => (f i).fst)
      (List.dProd (List.finRange n) (fun i => (f i).fst) fun i => (f i).snd)
rw [List.ofFn_eq_map, GradedMonoid.list_prod_map_eq_dProd]