case h
α : Type u_1
β : Type ?u.295412
γ : Type ?u.295415
ι : Type ?u.295418
M : Type u_2
M' : Type ?u.295424
N : Type ?u.295427
P : Type ?u.295430
G : Type ?u.295433
H : Type ?u.295436
R : Type ?u.295439
S : Type ?u.295442
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
j : α
⊢ ↑(update f a b) j = ↑(single a b + erase a f) j
α : Type u_1
β : Type ?u.295412
γ : Type ?u.295415
ι : Type ?u.295418
M : Type u_2
M' : Type ?u.295424
N : Type ?u.295427
P : Type ?u.295430
G : Type ?u.295433
H : Type ?u.295436
R : Type ?u.295439
S : Type ?u.295442
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
⊢ update f a b = single a b + erase a f
ext j
case h.inl
α : Type u_1
β : Type ?u.295412
γ : Type ?u.295415
ι : Type ?u.295418
M : Type u_2
M' : Type ?u.295424
N : Type ?u.295427
P : Type ?u.295430
G : Type ?u.295433
H : Type ?u.295436
R : Type ?u.295439
S : Type ?u.295442
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
⊢ ↑(update f a b) a = ↑(single a b + erase a f) a

case h.inr
α : Type u_1
β : Type ?u.295412
γ : Type ?u.295415
ι : Type ?u.295418
M : Type u_2
M' : Type ?u.295424
N : Type ?u.295427
P : Type ?u.295430
G : Type ?u.295433
H : Type ?u.295436
R : Type ?u.295439
S : Type ?u.295442
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
j : α
h : a ≠ j
⊢ ↑(update f a b) j = ↑(single a b + erase a f) j
case h
α : Type u_1
β : Type ?u.295412
γ : Type ?u.295415
ι : Type ?u.295418
M : Type u_2
M' : Type ?u.295424
N : Type ?u.295427
P : Type ?u.295430
G : Type ?u.295433
H : Type ?u.295436
R : Type ?u.295439
S : Type ?u.295442
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
j : α
⊢ ↑(update f a b) j = ↑(single a b + erase a f) j
rcases eq_or_ne a j with (rfl | h)
no goals
case h.inl
α : Type u_1
β : Type ?u.295412
γ : Type ?u.295415
ι : Type ?u.295418
M : Type u_2
M' : Type ?u.295424
N : Type ?u.295427
P : Type ?u.295430
G : Type ?u.295433
H : Type ?u.295436
R : Type ?u.295439
S : Type ?u.295442
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
⊢ ↑(update f a b) a = ↑(single a b + erase a f) a
simp
no goals
case h.inr
α : Type u_1
β : Type ?u.295412
γ : Type ?u.295415
ι : Type ?u.295418
M : Type u_2
M' : Type ?u.295424
N : Type ?u.295427
P : Type ?u.295430
G : Type ?u.295433
H : Type ?u.295436
R : Type ?u.295439
S : Type ?u.295442
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
j : α
h : a ≠ j
⊢ ↑(update f a b) j = ↑(single a b + erase a f) j
simp [Function.update_noteq h.symm, single_apply, h, erase_ne, h.symm]