no goals
ι : Type u_1
R : Type u_2
α : Type u_4
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
fι : α → ι
fA : (a : α) → { x // x ∈ A (fι a) }
l : List α
⊢ ↑(List.dProd l fι fA) = List.prod (List.map (fun a => ↑(fA a)) l)
match l with
| [] =>
  rw [List.dProd_nil, coe_gOne, List.map_nil, List.prod_nil]
| head::tail =>
  rw [List.dProd_cons, coe_gMul, List.map_cons, List.prod_cons,
    SetLike.coe_list_dProd _ _ _ tail]
no goals
ι : Type u_1
R : Type u_2
α : Type u_4
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
fι : α → ι
fA : (a : α) → { x // x ∈ A (fι a) }
l : List α
⊢ ↑(List.dProd [] fι fA) = List.prod (List.map (fun a => ↑(fA a)) [])
rw [List.dProd_nil, coe_gOne, List.map_nil, List.prod_nil]
no goals
ι : Type u_1
R : Type u_2
α : Type u_4
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
fι : α → ι
fA : (a : α) → { x // x ∈ A (fι a) }
l : List α
head : α
tail : List α
⊢ ↑(List.dProd (head :: tail) fι fA) = List.prod (List.map (fun a => ↑(fA a)) (head :: tail))
rw [List.dProd_cons, coe_gMul, List.map_cons, List.prod_cons,
  SetLike.coe_list_dProd _ _ _ tail]