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

ι : Type u_3
σ : Type u_2
S : Type ?u.273217
R : Type u_1
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_3
σ : Type u_2
S : Type ?u.273217
R : Type u_1
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_3
σ : Type u_2
S : Type ?u.273217
R : Type u_1
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
swap
ι : Type u_3
σ : Type u_2
S : Type ?u.273217
R : Type u_1
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
ι : Type u_3
σ : Type u_2
S : Type ?u.273217
R : Type u_1
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
simp_rw [ZeroMemClass.coe_zero, MulZeroClass.zero_mul, ite_self]
no goals
ι : Type u_3
σ : Type u_2
S : Type ?u.273217
R : Type u_1
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
exact Dfinsupp.sum_zero
ι : Type u_3
σ : Type u_2
S : Type ?u.273217
R : Type u_1
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
ι : Type u_3
σ : Type u_2
S : Type ?u.273217
R : Type u_1
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
rw [Dfinsupp.sum, Finset.sum_ite_of_false _ _ fun x _ H => _, Finset.sum_const_zero]
no goals
ι : Type u_3
σ : Type u_2
S : Type ?u.273217
R : Type u_1
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
exact fun x _ H => h ((self_le_add_right i x).trans_eq H)