no goals
α : Type u_1
ι : Type ?u.74791
γ : Type ?u.74794
A : Type ?u.74797
B : Type ?u.74800
C : Type ?u.74803
inst✝⁷ : AddCommMonoid A
inst✝⁶ : AddCommMonoid B
inst✝⁵ : AddCommMonoid C
t : ι → A → C
h0 : ∀ (i : ι), t i 0 = 0
h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y
s : Finset α
f✝ : α → ι →₀ A
i : ι
g : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type ?u.77933
M : Type ?u.77936
M' : Type ?u.77939
N✝ : Type ?u.77942
P : Type ?u.77945
G : Type ?u.77948
H : Type ?u.77951
R : Type ?u.77954
S : Type ?u.77957
inst✝⁴ : Zero M
inst✝³ : Zero M'
inst✝² : CommMonoid N✝
inst✝¹ : DecidableEq α
N : Type u_2
inst✝ : AddCommMonoid N
f : α →₀ N
a : α
⊢ (sum f fun x v => if x = a then v else 0) = ↑f a
classical
  convert f.sum_ite_eq' a fun _ => id
  simp [ite_eq_right_iff.2 Eq.symm]
case h.e'_3
α : Type u_1
ι : Type ?u.74791
γ : Type ?u.74794
A : Type ?u.74797
B : Type ?u.74800
C : Type ?u.74803
inst✝⁷ : AddCommMonoid A
inst✝⁶ : AddCommMonoid B
inst✝⁵ : AddCommMonoid C
t : ι → A → C
h0 : ∀ (i : ι), t i 0 = 0
h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y
s : Finset α
f✝ : α → ι →₀ A
i : ι
g : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type ?u.77933
M : Type ?u.77936
M' : Type ?u.77939
N✝ : Type ?u.77942
P : Type ?u.77945
G : Type ?u.77948
H : Type ?u.77951
R : Type ?u.77954
S : Type ?u.77957
inst✝⁴ : Zero M
inst✝³ : Zero M'
inst✝² : CommMonoid N✝
inst✝¹ : DecidableEq α
N : Type u_2
inst✝ : AddCommMonoid N
f : α →₀ N
a : α
⊢ ↑f a = if a ∈ f.support then id (↑f a) else 0
α : Type u_1
ι : Type ?u.74791
γ : Type ?u.74794
A : Type ?u.74797
B : Type ?u.74800
C : Type ?u.74803
inst✝⁷ : AddCommMonoid A
inst✝⁶ : AddCommMonoid B
inst✝⁵ : AddCommMonoid C
t : ι → A → C
h0 : ∀ (i : ι), t i 0 = 0
h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y
s : Finset α
f✝ : α → ι →₀ A
i : ι
g : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type ?u.77933
M : Type ?u.77936
M' : Type ?u.77939
N✝ : Type ?u.77942
P : Type ?u.77945
G : Type ?u.77948
H : Type ?u.77951
R : Type ?u.77954
S : Type ?u.77957
inst✝⁴ : Zero M
inst✝³ : Zero M'
inst✝² : CommMonoid N✝
inst✝¹ : DecidableEq α
N : Type u_2
inst✝ : AddCommMonoid N
f : α →₀ N
a : α
⊢ (sum f fun x v => if x = a then v else 0) = ↑f a
convert f.sum_ite_eq' a fun _ => id
no goals
case h.e'_3
α : Type u_1
ι : Type ?u.74791
γ : Type ?u.74794
A : Type ?u.74797
B : Type ?u.74800
C : Type ?u.74803
inst✝⁷ : AddCommMonoid A
inst✝⁶ : AddCommMonoid B
inst✝⁵ : AddCommMonoid C
t : ι → A → C
h0 : ∀ (i : ι), t i 0 = 0
h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y
s : Finset α
f✝ : α → ι →₀ A
i : ι
g : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type ?u.77933
M : Type ?u.77936
M' : Type ?u.77939
N✝ : Type ?u.77942
P : Type ?u.77945
G : Type ?u.77948
H : Type ?u.77951
R : Type ?u.77954
S : Type ?u.77957
inst✝⁴ : Zero M
inst✝³ : Zero M'
inst✝² : CommMonoid N✝
inst✝¹ : DecidableEq α
N : Type u_2
inst✝ : AddCommMonoid N
f : α →₀ N
a : α
⊢ ↑f a = if a ∈ f.support then id (↑f a) else 0
simp [ite_eq_right_iff.2 Eq.symm]