Theorem: DFinsupp.mk_eq_sum (DividedPowers/ForMathlib/GradedRingQuot.lean)

State before:
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ι) → β i
⊢ (DFinsupp.mk s fun i => f ↑i) = ∑ i ∈ s, (of β i) (f i)
Tactic:
ext i
State after:
case h
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ι) → β i
i : ι
⊢ (DFinsupp.mk s fun i => f ↑i) i = (∑ i ∈ s, (of β i) (f i)) i

State before:
case h
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ι) → β i
i : ι
⊢ (DFinsupp.mk s fun i => f ↑i) i = (∑ i ∈ s, (of β i) (f i)) i
Tactic:
simp only [DFinsupp.mk_apply, DFinsupp.finset_sum_apply]
State after:
case h
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ι) → β i
i : ι
⊢ (if h : i ∈ s then f i else 0) = (∑ i ∈ s, (of β i) (f i)) i

State before:
case h
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ι) → β i
i : ι
⊢ (if h : i ∈ s then f i else 0) = (∑ i ∈ s, (of β i) (f i)) i
Tactic:
split_ifs with hi
State after:
case pos
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ι) → β i
i : ι
hi : i ∈ s
⊢ f i = (∑ i ∈ s, (of β i) (f i)) i

case neg
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ι) → β i
i : ι
hi : i ∉ s
⊢ 0 = (∑ i ∈ s, (of β i) (f i)) i

State before:
case pos
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ι) → β i
i : ι
hi : i ∈ s
⊢ f i = (∑ i ∈ s, (of β i) (f i)) i
Tactic:
rw [DFinsupp.finset_sum_apply, Finset.sum_eq_single_of_mem i hi
  (fun j _ hij =>  of_eq_of_ne _ _ _ _ hij), of_eq_same]
State after:
no goals

State before:
case neg
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ι) → β i
i : ι
hi : i ∉ s
⊢ 0 = (∑ i ∈ s, (of β i) (f i)) i
Tactic:
rw [DFinsupp.finset_sum_apply, Finset.sum_eq_zero
  (fun j hj => of_eq_of_ne _ _ _ _ (ne_of_mem_of_not_mem hj hi))]
State after:
no goals