α : Type u_2
ι : Type ?u.481609
γ : Type ?u.481612
A : Type ?u.481615
B : Type ?u.481618
C : Type ?u.481621
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.484751
M : Type u_1
M' : Type ?u.484757
N : Type ?u.484760
P : Type ?u.484763
G : Type ?u.484766
H : Type ?u.484769
R : Type ?u.484772
S : Type ?u.484775
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ (if i ∈ univ then m else 0) = m
α : Type u_2
ι : Type ?u.481609
γ : Type ?u.481612
A : Type ?u.481615
B : Type ?u.481618
C : Type ?u.481621
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.484751
M : Type u_1
M' : Type ?u.484757
N : Type ?u.484760
P : Type ?u.484763
G : Type ?u.484766
H : Type ?u.484769
R : Type ?u.484772
S : Type ?u.484775
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ ∑ j : α, ↑(single i m) j = m
classical rw [single, coe_mk, Finset.sum_pi_single']
no goals
α : Type u_2
ι : Type ?u.481609
γ : Type ?u.481612
A : Type ?u.481615
B : Type ?u.481618
C : Type ?u.481621
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.484751
M : Type u_1
M' : Type ?u.484757
N : Type ?u.484760
P : Type ?u.484763
G : Type ?u.484766
H : Type ?u.484769
R : Type ?u.484772
S : Type ?u.484775
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ (if i ∈ univ then m else 0) = m
simp
α : Type u_2
ι : Type ?u.481609
γ : Type ?u.481612
A : Type ?u.481615
B : Type ?u.481618
C : Type ?u.481621
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.484751
M : Type u_1
M' : Type ?u.484757
N : Type ?u.484760
P : Type ?u.484763
G : Type ?u.484766
H : Type ?u.484769
R : Type ?u.484772
S : Type ?u.484775
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ (if i ∈ univ then m else 0) = m
α : Type u_2
ι : Type ?u.481609
γ : Type ?u.481612
A : Type ?u.481615
B : Type ?u.481618
C : Type ?u.481621
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.484751
M : Type u_1
M' : Type ?u.484757
N : Type ?u.484760
P : Type ?u.484763
G : Type ?u.484766
H : Type ?u.484769
R : Type ?u.484772
S : Type ?u.484775
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ ∑ j : α, ↑(single i m) j = m
rw [single, coe_mk, Finset.sum_pi_single']