Theorem: DFinsupp.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
M : Type u_4
inst✝¹ : AddCommMonoid M
ι : Type u_5
dec_ι : DecidableEq ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
h : (i : ι) → β i →+ M
x : DFinsupp β
s : Finset ι
hs : x.support ⊆ s
⊢ (x.sum fun i y => (h i) y) = ∑ i ∈ s, (h i) (x i)
Tactic:
simp only [DFinsupp.sum]
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
M : Type u_4
inst✝¹ : AddCommMonoid M
ι : Type u_5
dec_ι : DecidableEq ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
h : (i : ι) → β i →+ M
x : DFinsupp β
s : Finset ι
hs : x.support ⊆ s
⊢ ∑ x_1 ∈ x.support, (h x_1) (x x_1) = ∑ x_1 ∈ s, (h x_1) (x x_1)

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
M : Type u_4
inst✝¹ : AddCommMonoid M
ι : Type u_5
dec_ι : DecidableEq ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
h : (i : ι) → β i →+ M
x : DFinsupp β
s : Finset ι
hs : x.support ⊆ s
⊢ ∑ x_1 ∈ x.support, (h x_1) (x x_1) = ∑ x_1 ∈ s, (h x_1) (x x_1)
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
M : Type u_4
inst✝¹ : AddCommMonoid M
ι : Type u_5
dec_ι : DecidableEq ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
h : (i : ι) → β i →+ M
x : DFinsupp β
s : Finset ι
hs : x.support ⊆ s
⊢ ∀ x_1 ∈ s, x_1 ∉ x.support → (h 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
M : Type u_4
inst✝¹ : AddCommMonoid M
ι : Type u_5
dec_ι : DecidableEq ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
h : (i : ι) → β i →+ M
x : DFinsupp β
s : Finset ι
hs : x.support ⊆ s
⊢ ∀ x_1 ∈ s, x_1 ∉ x.support → (h 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
M : Type u_4
inst✝¹ : AddCommMonoid M
ι : Type u_5
dec_ι : DecidableEq ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
h : (i : ι) → β i →+ M
x : DFinsupp β
s : Finset ι
hs : x.support ⊆ s
⊢ ∀ x_1 ∈ s, x_1 ∉ x.support → (h 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
M : Type u_4
inst✝¹ : AddCommMonoid M
ι : Type u_5
dec_ι : DecidableEq ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
h : (i : ι) → β i →+ M
x : DFinsupp β
s : Finset ι
hs : x.support ⊆ s
i : ι
a✝ : i ∈ s
hi' : i ∉ x.support
⊢ (h 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
M : Type u_4
inst✝¹ : AddCommMonoid M
ι : Type u_5
dec_ι : DecidableEq ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
h : (i : ι) → β i →+ M
x : DFinsupp β
s : Finset ι
hs : x.support ⊆ s
i : ι
a✝ : i ∈ s
hi' : i ∉ x.support
⊢ (h 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
M : Type u_4
inst✝¹ : AddCommMonoid M
ι : Type u_5
dec_ι : DecidableEq ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
h : (i : ι) → β i →+ M
x : DFinsupp β
s : Finset ι
hs : x.support ⊆ s
i : ι
a✝ : i ∈ s
hi' : x i = 0
⊢ (h 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
M : Type u_4
inst✝¹ : AddCommMonoid M
ι : Type u_5
dec_ι : DecidableEq ι
β : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (β i)
inst : (i : ι) → (x : β i) → Decidable (x ≠ 0)
h : (i : ι) → β i →+ M
x : DFinsupp β
s : Finset ι
hs : x.support ⊆ s
i : ι
a✝ : i ∈ s
hi' : x i = 0
⊢ (h i) (x i) = 0
Tactic:
rw [hi', map_zero]
State after:
no goals