[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝² : Semiring R
inst✝¹ : SetLike σ R
inst✝ : AddSubmonoidClass σ R
A : ι → σ
i : ι
⊢ AddCommMonoid { x // x ∈ A i }
[PROOFSTEP]
infer_instance
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝² : Ring R
inst✝¹ : SetLike σ R
inst✝ : AddSubgroupClass σ R
A : ι → σ
i : ι
⊢ AddCommGroup { x // x ∈ A i }
[PROOFSTEP]
infer_instance
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : CommSemiring S
inst✝² : Semiring R
inst✝¹ : Algebra S R
A : ι → Submodule S R
inst✝ : GradedOne A
s : S
⊢ ↑(algebraMap S R) s ∈ A 0
[PROOFSTEP]
rw [Algebra.algebraMap_eq_smul_one]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : CommSemiring S
inst✝² : Semiring R
inst✝¹ : Algebra S R
A : ι → Submodule S R
inst✝ : GradedOne A
s : S
⊢ s • 1 ∈ A 0
[PROOFSTEP]
exact (A 0).smul_mem s <| SetLike.one_mem_graded _
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : GradedOne A
n : ℕ
⊢ ↑n ∈ A 0
[PROOFSTEP]
induction' n with _ n_ih
[GOAL]
case zero
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : GradedOne A
⊢ ↑Nat.zero ∈ A 0
[PROOFSTEP]
rw [Nat.cast_zero]
[GOAL]
case zero
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : GradedOne A
⊢ 0 ∈ A 0
[PROOFSTEP]
exact zero_mem (A 0)
[GOAL]
case succ
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : GradedOne A
n✝ : ℕ
n_ih : ↑n✝ ∈ A 0
⊢ ↑(Nat.succ n✝) ∈ A 0
[PROOFSTEP]
rw [Nat.cast_succ]
[GOAL]
case succ
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : GradedOne A
n✝ : ℕ
n_ih : ↑n✝ ∈ A 0
⊢ ↑n✝ + 1 ∈ A 0
[PROOFSTEP]
exact add_mem n_ih (SetLike.one_mem_graded _)
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
z : ℤ
⊢ ↑z ∈ A 0
[PROOFSTEP]
induction z
[GOAL]
case ofNat
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
a✝ : ℕ
⊢ ↑(Int.ofNat a✝) ∈ A 0
[PROOFSTEP]
rw [Int.ofNat_eq_coe, Int.cast_ofNat]
[GOAL]
case ofNat
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
a✝ : ℕ
⊢ ↑a✝ ∈ A 0
[PROOFSTEP]
exact SetLike.nat_cast_mem_graded _ _
[GOAL]
case negSucc
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
a✝ : ℕ
⊢ ↑(Int.negSucc a✝) ∈ A 0
[PROOFSTEP]
rw [Int.cast_negSucc]
[GOAL]
case negSucc
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
a✝ : ℕ
⊢ -↑(a✝ + 1) ∈ A 0
[PROOFSTEP]
exact neg_mem (SetLike.nat_cast_mem_graded _ _)
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
⊢ ↑(↑(r * r') n) =
    ∑ ij in Finset.filter (fun ij => ij.fst + ij.snd = n) (DFinsupp.support r ×ˢ DFinsupp.support r'),
      ↑(↑r ij.fst) * ↑(↑r' ij.snd)
[PROOFSTEP]
rw [mul_eq_sum_support_ghas_mul, DFinsupp.finset_sum_apply, AddSubmonoidClass.coe_finset_sum]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
⊢ ∑ i in DFinsupp.support r ×ˢ DFinsupp.support r',
      ↑(↑(↑(of (fun i => (fun i => { x // x ∈ A i }) i) (i.fst + i.snd)) (GradedMonoid.GMul.mul (↑r i.fst) (↑r' i.snd)))
          n) =
    ∑ ij in Finset.filter (fun ij => ij.fst + ij.snd = n) (DFinsupp.support r ×ˢ DFinsupp.support r'),
      ↑(↑r ij.fst) * ↑(↑r' ij.snd)
[PROOFSTEP]
simp_rw [coe_of_apply, apply_ite, ZeroMemClass.coe_zero, ← Finset.sum_filter, SetLike.coe_gMul]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
⊢ ↑(↑(r * r') n) = DFinsupp.sum r fun i ri => DFinsupp.sum r' fun j rj => if i + j = n then ↑ri * ↑rj else 0
[PROOFSTEP]
rw [mul_eq_dfinsupp_sum]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
⊢ ↑(↑(DFinsupp.sum r fun i ai =>
            DFinsupp.sum r' fun j aj => ↑(of (fun i => { x // x ∈ A i }) (i + j)) (GradedMonoid.GMul.mul ai aj))
        n) =
    DFinsupp.sum r fun i ri => DFinsupp.sum r' fun j rj => if i + j = n then ↑ri * ↑rj else 0
[PROOFSTEP]
iterate 2 rw [DFinsupp.sum_apply, DFinsupp.sum, AddSubmonoidClass.coe_finset_sum]; congr; ext
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
⊢ ↑(↑(DFinsupp.sum r fun i ai =>
            DFinsupp.sum r' fun j aj => ↑(of (fun i => { x // x ∈ A i }) (i + j)) (GradedMonoid.GMul.mul ai aj))
        n) =
    DFinsupp.sum r fun i ri => DFinsupp.sum r' fun j rj => if i + j = n then ↑ri * ↑rj else 0
[PROOFSTEP]
rw [DFinsupp.sum_apply, DFinsupp.sum, AddSubmonoidClass.coe_finset_sum]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
⊢ ∑ i in DFinsupp.support r,
      ↑(↑(DFinsupp.sum r' fun j aj => ↑(of (fun i => { x // x ∈ A i }) (i + j)) (GradedMonoid.GMul.mul (↑r i) aj)) n) =
    DFinsupp.sum r fun i ri => DFinsupp.sum r' fun j rj => if i + j = n then ↑ri * ↑rj else 0
[PROOFSTEP]
congr
[GOAL]
case e_f
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
⊢ (fun i =>
      ↑(↑(DFinsupp.sum r' fun j aj => ↑(of (fun i => { x // x ∈ A i }) (i + j)) (GradedMonoid.GMul.mul (↑r i) aj)) n)) =
    fun i => (fun i ri => DFinsupp.sum r' fun j rj => if i + j = n then ↑ri * ↑rj else 0) i (↑r i)
[PROOFSTEP]
ext
[GOAL]
case e_f.h
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
n x✝ : ι
⊢ ↑(↑(DFinsupp.sum r' fun j aj => ↑(of (fun i => { x // x ∈ A i }) (x✝ + j)) (GradedMonoid.GMul.mul (↑r x✝) aj)) n) =
    (fun i ri => DFinsupp.sum r' fun j rj => if i + j = n then ↑ri * ↑rj else 0) x✝ (↑r x✝)
[PROOFSTEP]
rw [DFinsupp.sum_apply, DFinsupp.sum, AddSubmonoidClass.coe_finset_sum]
[GOAL]
case e_f.h
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
n x✝ : ι
⊢ ∑ i in DFinsupp.support r',
      ↑(↑(↑(of (fun i => { x // x ∈ A i }) (x✝ + i)) (GradedMonoid.GMul.mul (↑r x✝) (↑r' i))) n) =
    (fun i ri => DFinsupp.sum r' fun j rj => if i + j = n then ↑ri * ↑rj else 0) x✝ (↑r x✝)
[PROOFSTEP]
congr
[GOAL]
case e_f.h.e_f
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
n x✝ : ι
⊢ (fun i => ↑(↑(↑(of (fun i => { x // x ∈ A i }) (x✝ + i)) (GradedMonoid.GMul.mul (↑r x✝) (↑r' i))) n)) = fun i =>
    (fun j rj => if x✝ + j = n then ↑(↑r x✝) * ↑rj else 0) i (↑r' i)
[PROOFSTEP]
ext
[GOAL]
case e_f.h.e_f.h
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
n x✝¹ x✝ : ι
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) (x✝¹ + x✝)) (GradedMonoid.GMul.mul (↑r x✝¹) (↑r' x✝))) n) =
    (fun j rj => if x✝¹ + j = n then ↑(↑r x✝¹) * ↑rj else 0) x✝ (↑r' x✝)
[PROOFSTEP]
dsimp only
[GOAL]
case e_f.h.e_f.h
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
n x✝¹ x✝ : ι
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) (x✝¹ + x✝)) (GradedMonoid.GMul.mul (↑r x✝¹) (↑r' x✝))) n) =
    if x✝¹ + x✝ = n then ↑(↑r x✝¹) * ↑(↑r' x✝) else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
n x✝¹ x✝ : ι
h : x✝¹ + x✝ = n
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) (x✝¹ + x✝)) (GradedMonoid.GMul.mul (↑r x✝¹) (↑r' x✝))) n) = ↑(↑r x✝¹) * ↑(↑r' x✝)
[PROOFSTEP]
subst h
[GOAL]
case pos
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
x✝¹ x✝ : ι
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) (x✝¹ + x✝)) (GradedMonoid.GMul.mul (↑r x✝¹) (↑r' x✝))) (x✝¹ + x✝)) =
    ↑(↑r x✝¹) * ↑(↑r' x✝)
[PROOFSTEP]
rw [of_eq_same]
[GOAL]
case pos
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
x✝¹ x✝ : ι
⊢ ↑(GradedMonoid.GMul.mul (↑r x✝¹) (↑r' x✝)) = ↑(↑r x✝¹) * ↑(↑r' x✝)
[PROOFSTEP]
rfl
[GOAL]
case neg
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
n x✝¹ x✝ : ι
h : ¬x✝¹ + x✝ = n
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) (x✝¹ + x✝)) (GradedMonoid.GMul.mul (↑r x✝¹) (↑r' x✝))) n) = 0
[PROOFSTEP]
rw [of_eq_of_ne _ _ _ _ h]
[GOAL]
case neg
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), { x // x ∈ A i }
n x✝¹ x✝ : ι
h : ¬x✝¹ + x✝ = n
⊢ ↑0 = 0
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) i) r * r') n) = ↑r * ↑(↑r' j)
[PROOFSTEP]
classical
rw [coe_mul_apply_eq_dfinsupp_sum]
apply (DFinsupp.sum_single_index _).trans
swap
· simp_rw [ZeroMemClass.coe_zero, zero_mul, ite_self]
  exact DFinsupp.sum_zero
simp_rw [DFinsupp.sum, H, Finset.sum_ite_eq']
split_ifs with h
rfl
rw [DFinsupp.not_mem_support_iff.mp h, ZeroMemClass.coe_zero, mul_zero]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) i) r * r') n) = ↑r * ↑(↑r' j)
[PROOFSTEP]
rw [coe_mul_apply_eq_dfinsupp_sum]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ (DFinsupp.sum (↑(of (fun i => { x // x ∈ A i }) i) r) fun i ri =>
      DFinsupp.sum r' fun j rj => if i + j = n then ↑ri * ↑rj else 0) =
    ↑r * ↑(↑r' j)
[PROOFSTEP]
apply (DFinsupp.sum_single_index _).trans
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ (DFinsupp.sum r' fun j rj => if i + j = n then ↑r * ↑rj else 0) = ↑r * ↑(↑r' j)
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ (DFinsupp.sum r' fun j rj => if i + j = n then ↑0 * ↑rj else 0) = 0
[PROOFSTEP]
swap
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ (DFinsupp.sum r' fun j rj => if i + j = n then ↑0 * ↑rj else 0) = 0
[PROOFSTEP]
simp_rw [ZeroMemClass.coe_zero, zero_mul, ite_self]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ (DFinsupp.sum r' fun j rj => 0) = 0
[PROOFSTEP]
exact DFinsupp.sum_zero
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ (DFinsupp.sum r' fun j rj => if i + j = n then ↑r * ↑rj else 0) = ↑r * ↑(↑r' j)
[PROOFSTEP]
simp_rw [DFinsupp.sum, H, Finset.sum_ite_eq']
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ (if j ∈ DFinsupp.support r' then ↑r * ↑(↑r' j) else 0) = ↑r * ↑(↑r' j)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
h : j ∈ DFinsupp.support r'
⊢ ↑r * ↑(↑r' j) = ↑r * ↑(↑r' j)
case neg
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
h : ¬j ∈ DFinsupp.support r'
⊢ 0 = ↑r * ↑(↑r' j)
[PROOFSTEP]
rfl
[GOAL]
case neg
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
h : ¬j ∈ DFinsupp.support r'
⊢ 0 = ↑r * ↑(↑r' j)
[PROOFSTEP]
rw [DFinsupp.not_mem_support_iff.mp h, ZeroMemClass.coe_zero, mul_zero]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ ↑(↑(r * ↑(of (fun i => { x // x ∈ A i }) i) r') n) = ↑(↑r j) * ↑r'
[PROOFSTEP]
classical
rw [coe_mul_apply_eq_dfinsupp_sum, DFinsupp.sum_comm]
apply (DFinsupp.sum_single_index _).trans
swap
· simp_rw [ZeroMemClass.coe_zero, mul_zero, ite_self]
  exact DFinsupp.sum_zero
simp_rw [DFinsupp.sum, H, Finset.sum_ite_eq']
split_ifs with h
rfl
rw [DFinsupp.not_mem_support_iff.mp h, ZeroMemClass.coe_zero, zero_mul]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ ↑(↑(r * ↑(of (fun i => { x // x ∈ A i }) i) r') n) = ↑(↑r j) * ↑r'
[PROOFSTEP]
rw [coe_mul_apply_eq_dfinsupp_sum, DFinsupp.sum_comm]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ (DFinsupp.sum (↑(of (fun i => { x // x ∈ A i }) i) r') fun i₂ x₂ =>
      DFinsupp.sum r fun i₁ x₁ => if i₁ + i₂ = n then ↑x₁ * ↑x₂ else 0) =
    ↑(↑r j) * ↑r'
[PROOFSTEP]
apply (DFinsupp.sum_single_index _).trans
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ (DFinsupp.sum r fun i₁ x₁ => if i₁ + i = n then ↑x₁ * ↑r' else 0) = ↑(↑r j) * ↑r'
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ (DFinsupp.sum r fun i₁ x₁ => if i₁ + i = n then ↑x₁ * ↑0 else 0) = 0
[PROOFSTEP]
swap
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ (DFinsupp.sum r fun i₁ x₁ => if i₁ + i = n then ↑x₁ * ↑0 else 0) = 0
[PROOFSTEP]
simp_rw [ZeroMemClass.coe_zero, mul_zero, ite_self]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ (DFinsupp.sum r fun i₁ x₁ => 0) = 0
[PROOFSTEP]
exact DFinsupp.sum_zero
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ (DFinsupp.sum r fun i₁ x₁ => if i₁ + i = n then ↑x₁ * ↑r' else 0) = ↑(↑r j) * ↑r'
[PROOFSTEP]
simp_rw [DFinsupp.sum, H, Finset.sum_ite_eq']
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ (if j ∈ DFinsupp.support r then ↑(↑r j) * ↑r' else 0) = ↑(↑r j) * ↑r'
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
h : j ∈ DFinsupp.support r
⊢ ↑(↑r j) * ↑r' = ↑(↑r j) * ↑r'
case neg
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
h : ¬j ∈ DFinsupp.support r
⊢ 0 = ↑(↑r j) * ↑r'
[PROOFSTEP]
rfl
[GOAL]
case neg
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
h : ¬j ∈ DFinsupp.support r
⊢ 0 = ↑(↑r j) * ↑r'
[PROOFSTEP]
rw [DFinsupp.not_mem_support_iff.mp h, ZeroMemClass.coe_zero, zero_mul]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) i) r * r') n) = 0
[PROOFSTEP]
classical
rw [coe_mul_apply_eq_dfinsupp_sum]
apply (DFinsupp.sum_single_index _).trans
swap
· simp_rw [ZeroMemClass.coe_zero, zero_mul, ite_self]
  exact DFinsupp.sum_zero
· rw [DFinsupp.sum, Finset.sum_ite_of_false _ _ fun x _ H => _, Finset.sum_const_zero]
  exact fun x _ H => h ((self_le_add_right i x).trans_eq H)
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) i) r * r') n) = 0
[PROOFSTEP]
rw [coe_mul_apply_eq_dfinsupp_sum]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum (↑(of (fun i => { x // x ∈ A i }) i) r) fun i ri =>
      DFinsupp.sum r' fun j rj => if i + j = n then ↑ri * ↑rj else 0) =
    0
[PROOFSTEP]
apply (DFinsupp.sum_single_index _).trans
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r' fun j rj => if i + j = n then ↑r * ↑rj else 0) = 0
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r' fun j rj => if i + j = n then ↑0 * ↑rj else 0) = 0
[PROOFSTEP]
swap
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r' fun j rj => if i + j = n then ↑0 * ↑rj else 0) = 0
[PROOFSTEP]
simp_rw [ZeroMemClass.coe_zero, zero_mul, ite_self]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r' fun j rj => 0) = 0
[PROOFSTEP]
exact DFinsupp.sum_zero
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r' fun j rj => if i + j = n then ↑r * ↑rj else 0) = 0
[PROOFSTEP]
rw [DFinsupp.sum, Finset.sum_ite_of_false _ _ fun x _ H => _, Finset.sum_const_zero]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ ∀ (x : ι), x ∈ DFinsupp.support r' → i + x = n → False
[PROOFSTEP]
exact fun x _ H => h ((self_le_add_right i x).trans_eq H)
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ ↑(↑(r * ↑(of (fun i => { x // x ∈ A i }) i) r') n) = 0
[PROOFSTEP]
classical
rw [coe_mul_apply_eq_dfinsupp_sum, DFinsupp.sum_comm]
apply (DFinsupp.sum_single_index _).trans
swap
· simp_rw [ZeroMemClass.coe_zero, mul_zero, ite_self]
  exact DFinsupp.sum_zero
· rw [DFinsupp.sum, Finset.sum_ite_of_false _ _ fun x _ H => _, Finset.sum_const_zero]
  exact fun x _ H => h ((self_le_add_left i x).trans_eq H)
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ ↑(↑(r * ↑(of (fun i => { x // x ∈ A i }) i) r') n) = 0
[PROOFSTEP]
rw [coe_mul_apply_eq_dfinsupp_sum, DFinsupp.sum_comm]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum (↑(of (fun i => { x // x ∈ A i }) i) r') fun i₂ x₂ =>
      DFinsupp.sum r fun i₁ x₁ => if i₁ + i₂ = n then ↑x₁ * ↑x₂ else 0) =
    0
[PROOFSTEP]
apply (DFinsupp.sum_single_index _).trans
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r fun i₁ x₁ => if i₁ + i = n then ↑x₁ * ↑r' else 0) = 0
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r fun i₁ x₁ => if i₁ + i = n then ↑x₁ * ↑0 else 0) = 0
[PROOFSTEP]
swap
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r fun i₁ x₁ => if i₁ + i = n then ↑x₁ * ↑0 else 0) = 0
[PROOFSTEP]
simp_rw [ZeroMemClass.coe_zero, mul_zero, ite_self]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r fun i₁ x₁ => 0) = 0
[PROOFSTEP]
exact DFinsupp.sum_zero
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r fun i₁ x₁ => if i₁ + i = n then ↑x₁ * ↑r' else 0) = 0
[PROOFSTEP]
rw [DFinsupp.sum, Finset.sum_ite_of_false _ _ fun x _ H => _, Finset.sum_const_zero]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : CanonicallyOrderedAddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
n : ι
h : ¬i ≤ n
⊢ ∀ (x : ι), x ∈ DFinsupp.support r → x + i = n → False
[PROOFSTEP]
exact fun x _ H => h ((self_le_add_left i x).trans_eq H)
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁸ : DecidableEq ι
inst✝⁷ : Semiring R
inst✝⁶ : SetLike σ R
inst✝⁵ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁴ : CanonicallyOrderedAddMonoid ι
inst✝³ : SetLike.GradedMonoid A
inst✝² : Sub ι
inst✝¹ : OrderedSub ι
inst✝ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
h : i ≤ n
x : ι
⊢ i + x = n ↔ x = n - i
[PROOFSTEP]
rw [eq_tsub_iff_add_eq_of_le h, add_comm]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁹ : DecidableEq ι
inst✝⁸ : Semiring R
inst✝⁷ : SetLike σ R
inst✝⁶ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁵ : CanonicallyOrderedAddMonoid ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
n : ι
inst✝ : Decidable (i ≤ n)
⊢ ↑(↑(r * ↑(of (fun i => { x // x ∈ A i }) i) r') n) = if i ≤ n then ↑(↑r (n - i)) * ↑r' else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁹ : DecidableEq ι
inst✝⁸ : Semiring R
inst✝⁷ : SetLike σ R
inst✝⁶ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁵ : CanonicallyOrderedAddMonoid ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
n : ι
inst✝ : Decidable (i ≤ n)
h : i ≤ n
⊢ ↑(↑(r * ↑(of (fun i => { x // x ∈ A i }) i) r') n) = ↑(↑r (n - i)) * ↑r'
case neg
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁹ : DecidableEq ι
inst✝⁸ : Semiring R
inst✝⁷ : SetLike σ R
inst✝⁶ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁵ : CanonicallyOrderedAddMonoid ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
r : ⨁ (i : ι), { x // x ∈ A i }
i : ι
r' : { x // x ∈ A i }
n : ι
inst✝ : Decidable (i ≤ n)
h : ¬i ≤ n
⊢ ↑(↑(r * ↑(of (fun i => { x // x ∈ A i }) i) r') n) = 0
[PROOFSTEP]
exacts [coe_mul_of_apply_of_le _ _ _ n h, coe_mul_of_apply_of_not_le _ _ _ n h]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁹ : DecidableEq ι
inst✝⁸ : Semiring R
inst✝⁷ : SetLike σ R
inst✝⁶ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁵ : CanonicallyOrderedAddMonoid ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
inst✝ : Decidable (i ≤ n)
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) i) r * r') n) = if i ≤ n then ↑r * ↑(↑r' (n - i)) else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁹ : DecidableEq ι
inst✝⁸ : Semiring R
inst✝⁷ : SetLike σ R
inst✝⁶ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁵ : CanonicallyOrderedAddMonoid ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
inst✝ : Decidable (i ≤ n)
h : i ≤ n
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) i) r * r') n) = ↑r * ↑(↑r' (n - i))
case neg
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁹ : DecidableEq ι
inst✝⁸ : Semiring R
inst✝⁷ : SetLike σ R
inst✝⁶ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁵ : CanonicallyOrderedAddMonoid ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
inst✝ : Decidable (i ≤ n)
h : ¬i ≤ n
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) i) r * r') n) = 0
[PROOFSTEP]
exacts [coe_of_mul_apply_of_le _ _ _ n h, coe_of_mul_apply_of_not_le _ _ _ n h]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝³ : DecidableEq ι
inst✝² : CommSemiring S
inst✝¹ : Semiring R
inst✝ : Algebra S R
p : Submodule S R
⊢ 1 ∈ p ^ 0
[PROOFSTEP]
rw [← one_le, pow_zero]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝³ : DecidableEq ι
inst✝² : CommSemiring S
inst✝¹ : Semiring R
inst✝ : Algebra S R
p✝ : Submodule S R
i j : ℕ
p q : R
hp : p ∈ p✝ ^ i
hq : q ∈ p✝ ^ j
⊢ p * q ∈ p✝ ^ (i + j)
[PROOFSTEP]
rw [pow_add]
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝³ : DecidableEq ι
inst✝² : CommSemiring S
inst✝¹ : Semiring R
inst✝ : Algebra S R
p✝ : Submodule S R
i j : ℕ
p q : R
hp : p ∈ p✝ ^ i
hq : q ∈ p✝ ^ j
⊢ p * q ∈ p✝ ^ i * p✝ ^ j
[PROOFSTEP]
exact Submodule.mul_mem_mul hp hq
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
inst✝³ : CommSemiring S
inst✝² : Semiring R
inst✝¹ : Algebra S R
A : ι → Submodule S R
inst✝ : SetLike.GradedMonoid A
i : ι
x : { x // x ∈ A i }
⊢ ↑((fun i => LinearMap.toAddMonoidHom ((fun i => Submodule.subtype (A i)) i)) 0) GradedMonoid.GOne.one = 1
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
inst✝³ : CommSemiring S
inst✝² : Semiring R
inst✝¹ : Algebra S R
A : ι → Submodule S R
inst✝ : SetLike.GradedMonoid A
i : ι
x : { x // x ∈ A i }
i✝ j✝ : ι
x✝¹ : { x // x ∈ A i✝ }
x✝ : { x // x ∈ A j✝ }
⊢ ↑((fun i => LinearMap.toAddMonoidHom ((fun i => Submodule.subtype (A i)) i)) (i✝ + j✝))
      (GradedMonoid.GMul.mul x✝¹ x✝) =
    ↑((fun i => LinearMap.toAddMonoidHom ((fun i => Submodule.subtype (A i)) i)) i✝) x✝¹ *
      ↑((fun i => LinearMap.toAddMonoidHom ((fun i => Submodule.subtype (A i)) i)) j✝) x✝
[PROOFSTEP]
rfl
