[GOAL]
ι : Type u_1
A : ι → Type u_2
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
i : ι
a : A i
n : ℕ
⊢ mk i a ^ n = mk (n • i) (GMonoid.gnpow n a)
[PROOFSTEP]
match n with
| 0 =>
  rw [pow_zero]
  exact (GMonoid.gnpow_zero' ⟨_, a⟩).symm
| n + 1 =>
  rw [pow_succ, mk_pow a n, mk_mul_mk]
  exact (GMonoid.gnpow_succ' n ⟨_, a⟩).symm
[GOAL]
ι : Type u_1
A : ι → Type u_2
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
i : ι
a : A i
n : ℕ
⊢ mk i a ^ 0 = mk (0 • i) (GMonoid.gnpow 0 a)
[PROOFSTEP]
rw [pow_zero]
[GOAL]
ι : Type u_1
A : ι → Type u_2
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
i : ι
a : A i
n : ℕ
⊢ 1 = mk (0 • i) (GMonoid.gnpow 0 a)
[PROOFSTEP]
exact (GMonoid.gnpow_zero' ⟨_, a⟩).symm
[GOAL]
ι : Type u_1
A : ι → Type u_2
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
i : ι
a : A i
n✝ n : ℕ
⊢ mk i a ^ (n + 1) = mk ((n + 1) • i) (GMonoid.gnpow (n + 1) a)
[PROOFSTEP]
rw [pow_succ, mk_pow a n, mk_mul_mk]
[GOAL]
ι : Type u_1
A : ι → Type u_2
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
i : ι
a : A i
n✝ n : ℕ
⊢ mk (i + n • i) (GMul.mul a (GMonoid.gnpow n a)) = mk ((n + 1) • i) (GMonoid.gnpow (n + 1) a)
[PROOFSTEP]
exact (GMonoid.gnpow_succ' n ⟨_, a⟩).symm
[GOAL]
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GradedMonoid.GMonoid A
l : List α
fι : α → ι
⊢ dProdIndex l fι = sum (map fι l)
[PROOFSTEP]
match l with
| [] => simp
| head :: tail => simp [List.dProdIndex_eq_map_sum tail fι]
[GOAL]
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GradedMonoid.GMonoid A
l : List α
fι : α → ι
⊢ dProdIndex [] fι = sum (map fι [])
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GradedMonoid.GMonoid A
l : List α
fι : α → ι
head : α
tail : List α
⊢ dProdIndex (head :: tail) fι = sum (map fι (head :: tail))
[PROOFSTEP]
simp [List.dProdIndex_eq_map_sum tail fι]
[GOAL]
ι : Type u_1
α : Type u_2
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)
[PROOFSTEP]
match l with
| [] => simp; rfl
| head :: tail => simp [← GradedMonoid.mk_list_dProd tail _ _, GradedMonoid.mk_mul_mk, List.prod_cons]
[GOAL]
ι : Type u_1
α : Type u_2
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)) [])
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
l : List α
fι : α → ι
fA : (a : α) → A (fι a)
⊢ mk 0 GOne.one = 1
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
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))
[PROOFSTEP]
simp [← GradedMonoid.mk_list_dProd tail _ _, GradedMonoid.mk_mul_mk, List.prod_cons]
[GOAL]
ι : Type u_1
α : Type u_2
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)
[PROOFSTEP]
rw [GradedMonoid.mk_list_dProd, GradedMonoid.mk]
[GOAL]
ι : Type u_1
α : Type u_2
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)
[PROOFSTEP]
simp_rw [Sigma.eta]
[GOAL]
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
n : ℕ
f : Fin n → GradedMonoid A
⊢ List.prod (List.ofFn f) =
    mk (List.dProdIndex (List.finRange n) fun i => (f i).fst)
      (List.dProd (List.finRange n) (fun i => (f i).fst) fun i => (f i).snd)
[PROOFSTEP]
rw [List.ofFn_eq_map, GradedMonoid.list_prod_map_eq_dProd]
[GOAL]
ι : Type u_1
R : Type u_2
α : Type u_3
inst✝¹ : AddMonoid ι
inst✝ : Monoid R
l : List α
fι : α → ι
fA : α → R
⊢ dProd l fι fA = prod (map fA l)
[PROOFSTEP]
match l with
| [] =>
  rw [List.dProd_nil, List.map_nil, List.prod_nil]
  rfl
| head :: tail =>
  rw [List.dProd_cons, List.map_cons, List.prod_cons, List.dProd_monoid tail _ _]
  rfl
[GOAL]
ι : Type u_1
R : Type u_2
α : Type u_3
inst✝¹ : AddMonoid ι
inst✝ : Monoid R
l : List α
fι : α → ι
fA : α → R
⊢ dProd [] fι fA = prod (map fA [])
[PROOFSTEP]
rw [List.dProd_nil, List.map_nil, List.prod_nil]
[GOAL]
ι : Type u_1
R : Type u_2
α : Type u_3
inst✝¹ : AddMonoid ι
inst✝ : Monoid R
l : List α
fι : α → ι
fA : α → R
⊢ GradedMonoid.GOne.one = 1
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
R : Type u_2
α : Type u_3
inst✝¹ : AddMonoid ι
inst✝ : Monoid R
l : List α
fι : α → ι
fA : α → R
head : α
tail : List α
⊢ dProd (head :: tail) fι fA = prod (map fA (head :: tail))
[PROOFSTEP]
rw [List.dProd_cons, List.map_cons, List.prod_cons, List.dProd_monoid tail _ _]
[GOAL]
ι : Type u_1
R : Type u_2
α : Type u_3
inst✝¹ : AddMonoid ι
inst✝ : Monoid R
l : List α
fι : α → ι
fA : α → R
head : α
tail : List α
⊢ GradedMonoid.GMul.mul (fA head) (prod (map fA tail)) = fA head * prod (map fA tail)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n : ℕ
r : R
i : ι
h : r ∈ A i
⊢ r ^ n ∈ A (n • i)
[PROOFSTEP]
match n with
| 0 =>
  rw [pow_zero, zero_nsmul]
  exact one_mem_graded _
| n + 1 =>
  rw [pow_succ', succ_nsmul']
  exact mul_mem_graded (pow_mem_graded n h) h
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n : ℕ
r : R
i : ι
h : r ∈ A i
⊢ r ^ 0 ∈ A (0 • i)
[PROOFSTEP]
rw [pow_zero, zero_nsmul]
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n : ℕ
r : R
i : ι
h : r ∈ A i
⊢ 1 ∈ A 0
[PROOFSTEP]
exact one_mem_graded _
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n✝ : ℕ
r : R
i : ι
h : r ∈ A i
n : ℕ
⊢ r ^ (n + 1) ∈ A ((n + 1) • i)
[PROOFSTEP]
rw [pow_succ', succ_nsmul']
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n✝ : ℕ
r : R
i : ι
h : r ∈ A i
n : ℕ
⊢ r ^ n * r ∈ A (n • i + i)
[PROOFSTEP]
exact mul_mem_graded (pow_mem_graded n h) h
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_4
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))
[PROOFSTEP]
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)
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
h : ∀ (j : ι'), j ∈ [] → r j ∈ A (i j)
⊢ List.prod (List.map r []) ∈ A (List.sum (List.map i []))
[PROOFSTEP]
rw [List.map_nil, List.map_nil, List.prod_nil, List.sum_nil]
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
h : ∀ (j : ι'), j ∈ [] → r j ∈ A (i j)
⊢ 1 ∈ A 0
[PROOFSTEP]
exact one_mem_graded _
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_4
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)))
[PROOFSTEP]
rw [List.map_cons, List.map_cons, List.prod_cons, List.sum_cons]
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_4
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))
[PROOFSTEP]
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)
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n : ℕ
i : Fin n → ι
r : Fin n → R
h : ∀ (j : Fin n), r j ∈ A (i j)
⊢ List.prod (List.ofFn r) ∈ A (List.sum (List.ofFn i))
[PROOFSTEP]
rw [List.ofFn_eq_map, List.ofFn_eq_map]
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n : ℕ
i : Fin n → ι
r : Fin n → R
h : ∀ (j : Fin n), r j ∈ A (i j)
⊢ List.prod (List.map r (List.finRange n)) ∈ A (List.sum (List.map i (List.finRange n)))
[PROOFSTEP]
exact list_prod_map_mem_graded _ _ _ fun _ _ => h _
[GOAL]
ι : Type u_1
R : Type u_2
α : Type u_3
S : Type u_4
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)
[PROOFSTEP]
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]
[GOAL]
ι : Type u_1
R : Type u_2
α : Type u_3
S : Type u_4
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)) [])
[PROOFSTEP]
rw [List.dProd_nil, coe_gOne, List.map_nil, List.prod_nil]
[GOAL]
ι : Type u_1
R : Type u_2
α : Type u_3
S : Type u_4
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))
[PROOFSTEP]
rw [List.dProd_cons, coe_gMul, List.map_cons, List.prod_cons, SetLike.coe_list_dProd _ _ _ tail]
