case nil
ι : Type u_2
inst✝³ : DecidableEq ι
A : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_1
fι : α → ι
fA : (a : α) → A (fι a)
⊢ ↑(of A (List.dProdIndex [] fι)) (List.dProd [] fι fA) = List.prod (List.map (fun a => ↑(of A (fι a)) (fA a)) [])

case cons
ι : Type u_2
inst✝³ : DecidableEq ι
A : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_1
fι : α → ι
fA : (a : α) → A (fι a)
head : α
tail : List α
tail_ih✝ :
  ↑(of A (List.dProdIndex tail fι)) (List.dProd tail fι fA) = List.prod (List.map (fun a => ↑(of A (fι a)) (fA a)) tail)
⊢ ↑(of A (List.dProdIndex (head :: tail) fι)) (List.dProd (head :: tail) fι fA) =
    List.prod (List.map (fun a => ↑(of A (fι a)) (fA a)) (head :: tail))
ι : Type u_2
inst✝³ : DecidableEq ι
A : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_1
l : List α
fι : α → ι
fA : (a : α) → A (fι a)
⊢ ↑(of A (List.dProdIndex l fι)) (List.dProd l fι fA) = List.prod (List.map (fun a => ↑(of A (fι a)) (fA a)) l)
induction' l with head tail
case nil
ι : Type u_2
inst✝³ : DecidableEq ι
A : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_1
fι : α → ι
fA : (a : α) → A (fι a)
⊢ ↑(of A (List.dProdIndex [] fι)) GradedMonoid.GOne.one = 1
case nil
ι : Type u_2
inst✝³ : DecidableEq ι
A : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_1
fι : α → ι
fA : (a : α) → A (fι a)
⊢ ↑(of A (List.dProdIndex [] fι)) (List.dProd [] fι fA) = List.prod (List.map (fun a => ↑(of A (fι a)) (fA a)) [])
simp only [List.map_nil, List.prod_nil, List.dProd_nil]
no goals
case nil
ι : Type u_2
inst✝³ : DecidableEq ι
A : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_1
fι : α → ι
fA : (a : α) → A (fι a)
⊢ ↑(of A (List.dProdIndex [] fι)) GradedMonoid.GOne.one = 1
rfl
case cons
ι : Type u_2
inst✝³ : DecidableEq ι
A : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_1
fι : α → ι
fA : (a : α) → A (fι a)
head : α
tail : List α
ih :
  ↑(of A (List.dProdIndex tail fι)) (List.dProd tail fι fA) = List.prod (List.map (fun a => ↑(of A (fι a)) (fA a)) tail)
⊢ ↑(of A (List.dProdIndex (head :: tail) fι)) (List.dProd (head :: tail) fι fA) =
    List.prod (List.map (fun a => ↑(of A (fι a)) (fA a)) (head :: tail))
case cons
ι : Type u_2
inst✝³ : DecidableEq ι
A : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_1
fι : α → ι
fA : (a : α) → A (fι a)
head : α
tail : List α
tail_ih✝ :
  ↑(of A (List.dProdIndex tail fι)) (List.dProd tail fι fA) = List.prod (List.map (fun a => ↑(of A (fι a)) (fA a)) tail)
⊢ ↑(of A (List.dProdIndex (head :: tail) fι)) (List.dProd (head :: tail) fι fA) =
    List.prod (List.map (fun a => ↑(of A (fι a)) (fA a)) (head :: tail))
rename_i ih
case cons
ι : Type u_2
inst✝³ : DecidableEq ι
A : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_1
fι : α → ι
fA : (a : α) → A (fι a)
head : α
tail : List α
ih :
  ↑(of A (List.dProdIndex tail fι)) (List.dProd tail fι fA) = List.prod (List.map (fun a => ↑(of A (fι a)) (fA a)) tail)
⊢ ↑(of A (List.dProdIndex (head :: tail) fι)) (GradedMonoid.GMul.mul (fA head) (List.dProd tail fι fA)) =
    ↑(of A (fι head)) (fA head) * ↑(of A (List.dProdIndex tail fι)) (List.dProd tail fι fA)
case cons
ι : Type u_2
inst✝³ : DecidableEq ι
A : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_1
fι : α → ι
fA : (a : α) → A (fι a)
head : α
tail : List α
ih :
  ↑(of A (List.dProdIndex tail fι)) (List.dProd tail fι fA) = List.prod (List.map (fun a => ↑(of A (fι a)) (fA a)) tail)
⊢ ↑(of A (List.dProdIndex (head :: tail) fι)) (List.dProd (head :: tail) fι fA) =
    List.prod (List.map (fun a => ↑(of A (fι a)) (fA a)) (head :: tail))
simp only [List.map_cons, List.prod_cons, List.dProd_cons, ← ih]
case cons
ι : Type u_2
inst✝³ : DecidableEq ι
A : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_1
fι : α → ι
fA : (a : α) → A (fι a)
head : α
tail : List α
ih :
  ↑(of A (List.dProdIndex tail fι)) (List.dProd tail fι fA) = List.prod (List.map (fun a => ↑(of A (fι a)) (fA a)) tail)
⊢ ↑(of A (List.dProdIndex (head :: tail) fι)) (GradedMonoid.GMul.mul (fA head) (List.dProd tail fι fA)) =
    ↑(of A (fι head + List.dProdIndex tail fι)) (GradedMonoid.GMul.mul (fA head) (List.dProd tail fι fA))
case cons
ι : Type u_2
inst✝³ : DecidableEq ι
A : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_1
fι : α → ι
fA : (a : α) → A (fι a)
head : α
tail : List α
ih :
  ↑(of A (List.dProdIndex tail fι)) (List.dProd tail fι fA) = List.prod (List.map (fun a => ↑(of A (fι a)) (fA a)) tail)
⊢ ↑(of A (List.dProdIndex (head :: tail) fι)) (GradedMonoid.GMul.mul (fA head) (List.dProd tail fι fA)) =
    ↑(of A (fι head)) (fA head) * ↑(of A (List.dProdIndex tail fι)) (List.dProd tail fι fA)
rw [DirectSum.of_mul_of (fA head)]
no goals
case cons
ι : Type u_2
inst✝³ : DecidableEq ι
A : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_1
fι : α → ι
fA : (a : α) → A (fι a)
head : α
tail : List α
ih :
  ↑(of A (List.dProdIndex tail fι)) (List.dProd tail fι fA) = List.prod (List.map (fun a => ↑(of A (fι a)) (fA a)) tail)
⊢ ↑(of A (List.dProdIndex (head :: tail) fι)) (GradedMonoid.GMul.mul (fA head) (List.dProd tail fι fA)) =
    ↑(of A (fι head + List.dProdIndex tail fι)) (GradedMonoid.GMul.mul (fA head) (List.dProd tail fι fA))
rfl