α : Type u_2
ι : Type ?u.487120
γ : Type ?u.487123
A : Type ?u.487126
B : Type ?u.487129
C : Type ?u.487132
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.490262
M : Type u_1
M' : Type ?u.490268
N : Type ?u.490271
P : Type ?u.490274
G : Type ?u.490277
H : Type ?u.490280
R : Type ?u.490283
S : Type ?u.490286
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ ∑ x : α, Pi.single x m i = m
α : Type u_2
ι : Type ?u.487120
γ : Type ?u.487123
A : Type ?u.487126
B : Type ?u.487129
C : Type ?u.487132
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.490262
M : Type u_1
M' : Type ?u.490268
N : Type ?u.490271
P : Type ?u.490274
G : Type ?u.490277
H : Type ?u.490280
R : Type ?u.490283
S : Type ?u.490286
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ ∑ j : α, ↑(single j m) i = m
simp_rw [single, coe_mk]
α : Type u_2
ι : Type ?u.487120
γ : Type ?u.487123
A : Type ?u.487126
B : Type ?u.487129
C : Type ?u.487132
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.490262
M : Type u_1
M' : Type ?u.490268
N : Type ?u.490271
P : Type ?u.490274
G : Type ?u.490277
H : Type ?u.490280
R : Type ?u.490283
S : Type ?u.490286
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ (if i ∈ univ then m else 0) = m
α : Type u_2
ι : Type ?u.487120
γ : Type ?u.487123
A : Type ?u.487126
B : Type ?u.487129
C : Type ?u.487132
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.490262
M : Type u_1
M' : Type ?u.490268
N : Type ?u.490271
P : Type ?u.490274
G : Type ?u.490277
H : Type ?u.490280
R : Type ?u.490283
S : Type ?u.490286
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ ∑ x : α, Pi.single x m i = m
classical rw [Finset.sum_pi_single]
no goals
α : Type u_2
ι : Type ?u.487120
γ : Type ?u.487123
A : Type ?u.487126
B : Type ?u.487129
C : Type ?u.487132
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.490262
M : Type u_1
M' : Type ?u.490268
N : Type ?u.490271
P : Type ?u.490274
G : Type ?u.490277
H : Type ?u.490280
R : Type ?u.490283
S : Type ?u.490286
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ (if i ∈ univ then m else 0) = m
simp
α : Type u_2
ι : Type ?u.487120
γ : Type ?u.487123
A : Type ?u.487126
B : Type ?u.487129
C : Type ?u.487132
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.490262
M : Type u_1
M' : Type ?u.490268
N : Type ?u.490271
P : Type ?u.490274
G : Type ?u.490277
H : Type ?u.490280
R : Type ?u.490283
S : Type ?u.490286
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ (if i ∈ univ then m else 0) = m
α : Type u_2
ι : Type ?u.487120
γ : Type ?u.487123
A : Type ?u.487126
B : Type ?u.487129
C : Type ?u.487132
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.490262
M : Type u_1
M' : Type ?u.490268
N : Type ?u.490271
P : Type ?u.490274
G : Type ?u.490277
H : Type ?u.490280
R : Type ?u.490283
S : Type ?u.490286
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ ∑ x : α, Pi.single x m i = m
rw [Finset.sum_pi_single]