no goals
ι : Type u_2
α : Type u_1
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
l : List α
fι : α → ι
fA : (a : α) → A (fι a)
⊢ mk (List.dProdIndex l fι) (List.dProd l fι fA) = List.prod (List.map (fun a => mk (fι a) (fA a)) l)
match l with
| [] => simp; rfl
| head::tail =>
  simp[← GradedMonoid.mk_list_dProd tail _ _, GradedMonoid.mk_mul_mk, List.prod_cons]
ι : Type u_2
α : Type u_1
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
l : List α
fι : α → ι
fA : (a : α) → A (fι a)
⊢ mk 0 GOne.one = 1
ι : Type u_2
α : Type u_1
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
l : List α
fι : α → ι
fA : (a : α) → A (fι a)
⊢ mk (List.dProdIndex [] fι) (List.dProd [] fι fA) = List.prod (List.map (fun a => mk (fι a) (fA a)) [])
simp
no goals
ι : Type u_2
α : Type u_1
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
l : List α
fι : α → ι
fA : (a : α) → A (fι a)
⊢ mk 0 GOne.one = 1
rfl
no goals
ι : Type u_2
α : Type u_1
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
l : List α
fι : α → ι
fA : (a : α) → A (fι a)
head : α
tail : List α
⊢ mk (List.dProdIndex (head :: tail) fι) (List.dProd (head :: tail) fι fA) =
    List.prod (List.map (fun a => mk (fι a) (fA a)) (head :: tail))
simp[← GradedMonoid.mk_list_dProd tail _ _, GradedMonoid.mk_mul_mk, List.prod_cons]