case h
R✝ : Type ?u.40332
R₁ : Type ?u.40335
R₂ : Type ?u.40338
R₃ : Type ?u.40341
R₄ : Type ?u.40344
S : Type ?u.40347
K : Type ?u.40350
K₂ : Type ?u.40353
M : Type ?u.40356
M' : Type ?u.40359
M₁ : Type ?u.40362
M₂ : Type ?u.40365
M₃ : Type ?u.40368
M₄ : Type ?u.40371
N : Type ?u.40374
N₂ : Type ?u.40377
ι✝ : Type ?u.40380
V : Type ?u.40383
V₂ : Type ?u.40386
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
R : Type u_2
inst✝ : Semiring R
x : ι → R
x✝ : ι
⊢ x x✝ = Finset.sum Finset.univ (fun i => x i • fun j => if i = j then 1 else 0) x✝
R✝ : Type ?u.40332
R₁ : Type ?u.40335
R₂ : Type ?u.40338
R₃ : Type ?u.40341
R₄ : Type ?u.40344
S : Type ?u.40347
K : Type ?u.40350
K₂ : Type ?u.40353
M : Type ?u.40356
M' : Type ?u.40359
M₁ : Type ?u.40362
M₂ : Type ?u.40365
M₃ : Type ?u.40368
M₄ : Type ?u.40371
N : Type ?u.40374
N₂ : Type ?u.40377
ι✝ : Type ?u.40380
V : Type ?u.40383
V₂ : Type ?u.40386
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
R : Type u_2
inst✝ : Semiring R
x : ι → R
⊢ x = ∑ i : ι, x i • fun j => if i = j then 1 else 0
ext
no goals
case h
R✝ : Type ?u.40332
R₁ : Type ?u.40335
R₂ : Type ?u.40338
R₃ : Type ?u.40341
R₄ : Type ?u.40344
S : Type ?u.40347
K : Type ?u.40350
K₂ : Type ?u.40353
M : Type ?u.40356
M' : Type ?u.40359
M₁ : Type ?u.40362
M₂ : Type ?u.40365
M₃ : Type ?u.40368
M₄ : Type ?u.40371
N : Type ?u.40374
N₂ : Type ?u.40377
ι✝ : Type ?u.40380
V : Type ?u.40383
V₂ : Type ?u.40386
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
R : Type u_2
inst✝ : Semiring R
x : ι → R
x✝ : ι
⊢ x x✝ = Finset.sum Finset.univ (fun i => x i • fun j => if i = j then 1 else 0) x✝
simp