ι : Type u_1
σ : Type u_3
S : Type ?u.170111
R : Type u_2
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'
ι : Type u_1
σ : Type u_3
S : Type ?u.170111
R : Type u_2
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'
rw [coe_mul_apply_eq_dfinsupp_sum, Dfinsupp.sum_comm]
ι : Type u_1
σ : Type u_3
S : Type ?u.170111
R : Type u_2
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_3
S : Type ?u.170111
R : Type u_2
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
ι : Type u_1
σ : Type u_3
S : Type ?u.170111
R : Type u_2
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'
apply (Dfinsupp.sum_single_index _).trans
ι : Type u_1
σ : Type u_3
S : Type ?u.170111
R : Type u_2
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

ι : Type u_1
σ : Type u_3
S : Type ?u.170111
R : Type u_2
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_3
S : Type ?u.170111
R : Type u_2
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_3
S : Type ?u.170111
R : Type u_2
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
swap
ι : Type u_1
σ : Type u_3
S : Type ?u.170111
R : Type u_2
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'
ι : Type u_1
σ : Type u_3
S : Type ?u.170111
R : Type u_2
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'
simp_rw [Dfinsupp.sum, H, Finset.sum_ite_eq']
case inl
ι : Type u_1
σ : Type u_3
S : Type ?u.170111
R : Type u_2
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 inr
ι : Type u_1
σ : Type u_3
S : Type ?u.170111
R : Type u_2
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'
ι : Type u_1
σ : Type u_3
S : Type ?u.170111
R : Type u_2
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'
split_ifs with h
case inr
ι : Type u_1
σ : Type u_3
S : Type ?u.170111
R : Type u_2
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'
case inl
ι : Type u_1
σ : Type u_3
S : Type ?u.170111
R : Type u_2
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 inr
ι : Type u_1
σ : Type u_3
S : Type ?u.170111
R : Type u_2
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'
rfl
no goals
case inr
ι : Type u_1
σ : Type u_3
S : Type ?u.170111
R : Type u_2
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'
rw [Dfinsupp.not_mem_support_iff.mp h, ZeroMemClass.coe_zero, MulZeroClass.zero_mul]
ι : Type u_1
σ : Type u_3
S : Type ?u.170111
R : Type u_2
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
ι : Type u_1
σ : Type u_3
S : Type ?u.170111
R : Type u_2
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
simp_rw [ZeroMemClass.coe_zero, MulZeroClass.mul_zero, ite_self]
no goals
ι : Type u_1
σ : Type u_3
S : Type ?u.170111
R : Type u_2
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
exact Dfinsupp.sum_zero