no goals
ι : Type u_4
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_1
l : List ι'
i : ι' → ι
r : ι' → R
h : ∀ (j : ι'), j ∈ l → r j ∈ A (i j)
⊢ List.prod (List.map r l) ∈ A (List.sum (List.map i l))
match l with
| [] =>
  rw [List.map_nil, List.map_nil, List.prod_nil, List.sum_nil]
  exact one_mem_graded _
| head::tail =>
  rw [List.map_cons, List.map_cons, List.prod_cons, List.sum_cons]
  exact
    mul_mem_graded (h _ <| List.mem_cons_self _ _)
      (list_prod_map_mem_graded tail _ _ <| fun j hj => h _ <| List.mem_cons_of_mem _ hj)
ι : Type u_4
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_1
l : List ι'
i : ι' → ι
r : ι' → R
h : ∀ (j : ι'), j ∈ [] → r j ∈ A (i j)
⊢ 1 ∈ A 0
ι : Type u_4
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_1
l : List ι'
i : ι' → ι
r : ι' → R
h : ∀ (j : ι'), j ∈ [] → r j ∈ A (i j)
⊢ List.prod (List.map r []) ∈ A (List.sum (List.map i []))
rw [List.map_nil, List.map_nil, List.prod_nil, List.sum_nil]
no goals
ι : Type u_4
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_1
l : List ι'
i : ι' → ι
r : ι' → R
h : ∀ (j : ι'), j ∈ [] → r j ∈ A (i j)
⊢ 1 ∈ A 0
exact one_mem_graded _
ι : Type u_4
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_1
l : List ι'
i : ι' → ι
r : ι' → R
head : ι'
tail : List ι'
h : ∀ (j : ι'), j ∈ head :: tail → r j ∈ A (i j)
⊢ r head * List.prod (List.map r tail) ∈ A (i head + List.sum (List.map i tail))
ι : Type u_4
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_1
l : List ι'
i : ι' → ι
r : ι' → R
head : ι'
tail : List ι'
h : ∀ (j : ι'), j ∈ head :: tail → r j ∈ A (i j)
⊢ List.prod (List.map r (head :: tail)) ∈ A (List.sum (List.map i (head :: tail)))
rw [List.map_cons, List.map_cons, List.prod_cons, List.sum_cons]
no goals
ι : Type u_4
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_1
l : List ι'
i : ι' → ι
r : ι' → R
head : ι'
tail : List ι'
h : ∀ (j : ι'), j ∈ head :: tail → r j ∈ A (i j)
⊢ r head * List.prod (List.map r tail) ∈ A (i head + List.sum (List.map i tail))
exact
  mul_mem_graded (h _ <| List.mem_cons_self _ _)
    (list_prod_map_mem_graded tail _ _ <| fun j hj => h _ <| List.mem_cons_of_mem _ hj)