Theorem: DirectSum.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
⊢ ((mk β s) fun i => f ↑i) = ∑ i ∈ s, (of β i) (f i)
Tactic:
apply DFinsupp.ext
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 : ι), ((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 : ι), ((mk β s) fun i => f ↑i) i = (∑ i ∈ s, (of β i) (f i)) i
Tactic:
intro 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 : ι
⊢ ((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 : ι
⊢ ((mk β s) fun i => f ↑i) i = (∑ i ∈ s, (of β i) (f i)) i
Tactic:
convert mk_apply s _ i
State after:
case h.e'_3
ι : 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 : ι
⊢ (∑ i ∈ s, (of β i) (f i)) i = if h : i ∈ s then f ↑⟨i, h⟩ else 0

State before:
case h.e'_3
ι : 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 : ι
⊢ (∑ i ∈ s, (of β i) (f i)) i = if h : i ∈ s then f ↑⟨i, h⟩ else 0
Tactic:
rw [DFinsupp.finset_sum_apply]
State after:
case h.e'_3
ι : 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 : ι
⊢ ∑ a ∈ s, ((of β a) (f a)) i = if h : i ∈ s then f ↑⟨i, h⟩ else 0

State before:
case h.e'_3
ι : 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 : ι
⊢ ∑ a ∈ s, ((of β a) (f a)) i = if h : i ∈ s then f ↑⟨i, h⟩ else 0
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
⊢ ∑ a ∈ s, ((of β a) (f a)) i = f ↑⟨i, hi⟩

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
⊢ ∑ a ∈ s, ((of β a) (f a)) i = 0

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
⊢ ∑ a ∈ s, ((of β a) (f a)) i = f ↑⟨i, hi⟩
Tactic:
rw [Finset.sum_eq_single_of_mem i hi (fun j _ hij => of_eq_of_ne _ _ _ _ hij),
  ← lof_eq_of ℕ, lof_apply]
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
⊢ ∑ a ∈ s, ((of β a) (f a)) i = 0
Tactic:
exact Finset.sum_eq_zero (fun j hj => of_eq_of_ne _ _ _ _ (ne_of_mem_of_not_mem hj hi))
State after:
no goals