Theorem: DirectSum.sum_of_support_le (DividedPowers/ForMathlib/GradedRingQuot.lean)

State before:
R : Type u_1
inst✝⁶ : CommSemiring R
ι✝ : Type u_2
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : AddCommMonoid ι✝
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
ι : Type u_4
dec_ι : DecidableEq ι
β : ι → Type u_5
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
x : ⨁ (i : ι), β i
s : Finset ι
hs : DFinsupp.support x ⊆ s
⊢ ∑ i ∈ s, (of β i) (x i) = x
Tactic:
conv_rhs => rw [← sum_support_of β x]
State after:
R : Type u_1
inst✝⁶ : CommSemiring R
ι✝ : Type u_2
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : AddCommMonoid ι✝
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
ι : Type u_4
dec_ι : DecidableEq ι
β : ι → Type u_5
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
x : ⨁ (i : ι), β i
s : Finset ι
hs : DFinsupp.support x ⊆ s
⊢ ∑ i ∈ s, (of β i) (x i) = ∑ i ∈ DFinsupp.support x, (of β i) (x i)

State before:
R : Type u_1
inst✝⁶ : CommSemiring R
ι✝ : Type u_2
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : AddCommMonoid ι✝
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
ι : Type u_4
dec_ι : DecidableEq ι
β : ι → Type u_5
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
x : ⨁ (i : ι), β i
s : Finset ι
hs : DFinsupp.support x ⊆ s
⊢ ∑ i ∈ s, (of β i) (x i) = ∑ i ∈ DFinsupp.support x, (of β i) (x i)
Tactic:
rw [eq_comm]
State after:
R : Type u_1
inst✝⁶ : CommSemiring R
ι✝ : Type u_2
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : AddCommMonoid ι✝
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
ι : Type u_4
dec_ι : DecidableEq ι
β : ι → Type u_5
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
x : ⨁ (i : ι), β i
s : Finset ι
hs : DFinsupp.support x ⊆ s
⊢ ∑ i ∈ DFinsupp.support x, (of β i) (x i) = ∑ i ∈ s, (of β i) (x i)

State before:
R : Type u_1
inst✝⁶ : CommSemiring R
ι✝ : Type u_2
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : AddCommMonoid ι✝
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
ι : Type u_4
dec_ι : DecidableEq ι
β : ι → Type u_5
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
x : ⨁ (i : ι), β i
s : Finset ι
hs : DFinsupp.support x ⊆ s
⊢ ∑ i ∈ DFinsupp.support x, (of β i) (x i) = ∑ i ∈ s, (of β i) (x i)
Tactic:
apply Finset.sum_subset hs
State after:
R : Type u_1
inst✝⁶ : CommSemiring R
ι✝ : Type u_2
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : AddCommMonoid ι✝
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
ι : Type u_4
dec_ι : DecidableEq ι
β : ι → Type u_5
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
x : ⨁ (i : ι), β i
s : Finset ι
hs : DFinsupp.support x ⊆ s
⊢ ∀ x_1 ∈ s, x_1 ∉ DFinsupp.support x → (of β x_1) (x x_1) = 0

State before:
R : Type u_1
inst✝⁶ : CommSemiring R
ι✝ : Type u_2
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : AddCommMonoid ι✝
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
ι : Type u_4
dec_ι : DecidableEq ι
β : ι → Type u_5
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
x : ⨁ (i : ι), β i
s : Finset ι
hs : DFinsupp.support x ⊆ s
⊢ ∀ x_1 ∈ s, x_1 ∉ DFinsupp.support x → (of β x_1) (x x_1) = 0
Tactic:
. intro i _ hi'
  simp only [DFinsupp.mem_support_toFun, ne_eq, not_not] at hi'
  rw [hi', map_zero]
State after:
no goals

State before:
R : Type u_1
inst✝⁶ : CommSemiring R
ι✝ : Type u_2
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : AddCommMonoid ι✝
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
ι : Type u_4
dec_ι : DecidableEq ι
β : ι → Type u_5
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
x : ⨁ (i : ι), β i
s : Finset ι
hs : DFinsupp.support x ⊆ s
⊢ ∀ x_1 ∈ s, x_1 ∉ DFinsupp.support x → (of β x_1) (x x_1) = 0
Tactic:
intro i _ hi'
State after:
R : Type u_1
inst✝⁶ : CommSemiring R
ι✝ : Type u_2
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : AddCommMonoid ι✝
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
ι : Type u_4
dec_ι : DecidableEq ι
β : ι → Type u_5
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
x : ⨁ (i : ι), β i
s : Finset ι
hs : DFinsupp.support x ⊆ s
i : ι
a✝ : i ∈ s
hi' : i ∉ DFinsupp.support x
⊢ (of β i) (x i) = 0

State before:
R : Type u_1
inst✝⁶ : CommSemiring R
ι✝ : Type u_2
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : AddCommMonoid ι✝
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
ι : Type u_4
dec_ι : DecidableEq ι
β : ι → Type u_5
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
x : ⨁ (i : ι), β i
s : Finset ι
hs : DFinsupp.support x ⊆ s
i : ι
a✝ : i ∈ s
hi' : i ∉ DFinsupp.support x
⊢ (of β i) (x i) = 0
Tactic:
simp only [DFinsupp.mem_support_toFun, ne_eq, not_not] at hi'
State after:
R : Type u_1
inst✝⁶ : CommSemiring R
ι✝ : Type u_2
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : AddCommMonoid ι✝
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
ι : Type u_4
dec_ι : DecidableEq ι
β : ι → Type u_5
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
x : ⨁ (i : ι), β i
s : Finset ι
hs : DFinsupp.support x ⊆ s
i : ι
a✝ : i ∈ s
hi' : x i = 0
⊢ (of β i) (x i) = 0

State before:
R : Type u_1
inst✝⁶ : CommSemiring R
ι✝ : Type u_2
inst✝⁵ : DecidableEq ι✝
inst✝⁴ : AddCommMonoid ι✝
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : DecidableEq A
inst✝¹ : Algebra R A
𝒜 : ι✝ → Submodule R A
rel : A → A → Prop
ι : Type u_4
dec_ι : DecidableEq ι
β : ι → Type u_5
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
x : ⨁ (i : ι), β i
s : Finset ι
hs : DFinsupp.support x ⊆ s
i : ι
a✝ : i ∈ s
hi' : x i = 0
⊢ (of β i) (x i) = 0
Tactic:
rw [hi', map_zero]
State after:
no goals