ι : Type u_2
α : Type u_1
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
l : List α
f : α → GradedMonoid A
⊢ List.prod (List.map f l) = List.prod (List.map (fun a => { fst := (f a).fst, snd := (f a).snd }) l)
ι : Type u_2
α : Type u_1
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
l : List α
f : α → GradedMonoid A
⊢ List.prod (List.map f l) =
    mk (List.dProdIndex l fun i => (f i).fst) (List.dProd l (fun i => (f i).fst) fun i => (f i).snd)
rw [GradedMonoid.mk_list_dProd, GradedMonoid.mk]
no goals
ι : Type u_2
α : Type u_1
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
l : List α
f : α → GradedMonoid A
⊢ List.prod (List.map f l) = List.prod (List.map (fun a => { fst := (f a).fst, snd := (f a).snd }) l)
simp_rw [Sigma.eta]