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 ι
x : (i : { x // x ∈ s }) → β ↑i
⊢ (mk β s) x = ∑ i ∈ s, (of β i) (if h : i ∈ s then x ⟨i, h⟩ else 0)
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 ι
x : (i : { x // x ∈ s }) → β ↑i
⊢ ∀ (i : ι), ((mk β s) x) i = (∑ i ∈ s, (of β i) (if h : i ∈ s then x ⟨i, h⟩ else 0)) 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 ι
x : (i : { x // x ∈ s }) → β ↑i
⊢ ∀ (i : ι), ((mk β s) x) i = (∑ i ∈ s, (of β i) (if h : i ∈ s then x ⟨i, h⟩ else 0)) 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 ι
x : (i : { x // x ∈ s }) → β ↑i
i : ι
⊢ ((mk β s) x) i = (∑ i ∈ s, (of β i) (if h : i ∈ s then x ⟨i, h⟩ else 0)) 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 ι
x : (i : { x // x ∈ s }) → β ↑i
i : ι
⊢ ((mk β s) x) i = (∑ i ∈ s, (of β i) (if h : i ∈ s then x ⟨i, h⟩ else 0)) i
Tactic:
rw [mk_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 ι
x : (i : { x // x ∈ s }) → β ↑i
i : ι
⊢ (if h : i ∈ s then x ⟨i, h⟩ else 0) = (∑ i ∈ s, (of β i) (if h : i ∈ s then x ⟨i, h⟩ else 0)) 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 ι
x : (i : { x // x ∈ s }) → β ↑i
i : ι
⊢ (if h : i ∈ s then x ⟨i, h⟩ else 0) = (∑ i ∈ s, (of β i) (if h : i ∈ s then x ⟨i, h⟩ else 0)) 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 ι
x : (i : { x // x ∈ s }) → β ↑i
i : ι
hi : i ∈ s
⊢ x ⟨i, hi⟩ = (∑ i ∈ s, (of β i) (if h : i ∈ s then x ⟨i, h⟩ else 0)) i

case neg
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
x : (i : { x // x ∈ s }) → β ↑i
i : ι
hi : i ∉ s
⊢ 0 = (∑ i ∈ s, (of β i) (if h : i ∈ s then x ⟨i, h⟩ else 0)) 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 ι
x : (i : { x // x ∈ s }) → β ↑i
i : ι
hi : i ∈ s
⊢ x ⟨i, hi⟩ = (∑ i ∈ s, (of β i) (if h : i ∈ s then x ⟨i, h⟩ else 0)) i
Tactic:
rw [DFinsupp.finset_sum_apply, Finset.sum_eq_single i (fun j _ hji => of_eq_of_ne _ _ _ _ hji),
  of_eq_same, dif_pos 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 ι
x : (i : { x // x ∈ s }) → β ↑i
i : ι
hi : i ∈ s
⊢ i ∉ s → ((of β i) (if h : i ∈ s then x ⟨i, h⟩ else 0)) 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 ι
x : (i : { x // x ∈ s }) → β ↑i
i : ι
hi : i ∈ s
⊢ i ∉ s → ((of β i) (if h : i ∈ s then x ⟨i, h⟩ else 0)) i = 0
Tactic:
intro his
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 ι
x : (i : { x // x ∈ s }) → β ↑i
i : ι
hi : i ∈ s
his : i ∉ s
⊢ ((of β i) (if h : i ∈ s then x ⟨i, h⟩ else 0)) 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 ι
x : (i : { x // x ∈ s }) → β ↑i
i : ι
hi : i ∈ s
his : i ∉ s
⊢ ((of β i) (if h : i ∈ s then x ⟨i, h⟩ else 0)) i = 0
Tactic:
rw [of_eq_same, dif_neg his]
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 ι
x : (i : { x // x ∈ s }) → β ↑i
i : ι
hi : i ∉ s
⊢ 0 = (∑ i ∈ s, (of β i) (if h : i ∈ s then x ⟨i, h⟩ else 0)) 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