case h
α : Type u_1
β : Type ?u.300562
γ : Type ?u.300565
ι : Type ?u.300568
M : Type u_2
M' : Type ?u.300574
N : Type ?u.300577
P : Type ?u.300580
G : Type ?u.300583
H : Type ?u.300586
R : Type ?u.300589
S : Type ?u.300592
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
j : α
⊢ ↑(update f a b) j = ↑(erase a f + single a b) j
α : Type u_1
β : Type ?u.300562
γ : Type ?u.300565
ι : Type ?u.300568
M : Type u_2
M' : Type ?u.300574
N : Type ?u.300577
P : Type ?u.300580
G : Type ?u.300583
H : Type ?u.300586
R : Type ?u.300589
S : Type ?u.300592
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
⊢ update f a b = erase a f + single a b
ext j
case h.inl
α : Type u_1
β : Type ?u.300562
γ : Type ?u.300565
ι : Type ?u.300568
M : Type u_2
M' : Type ?u.300574
N : Type ?u.300577
P : Type ?u.300580
G : Type ?u.300583
H : Type ?u.300586
R : Type ?u.300589
S : Type ?u.300592
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
⊢ ↑(update f a b) a = ↑(erase a f + single a b) a

case h.inr
α : Type u_1
β : Type ?u.300562
γ : Type ?u.300565
ι : Type ?u.300568
M : Type u_2
M' : Type ?u.300574
N : Type ?u.300577
P : Type ?u.300580
G : Type ?u.300583
H : Type ?u.300586
R : Type ?u.300589
S : Type ?u.300592
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
j : α
h : a ≠ j
⊢ ↑(update f a b) j = ↑(erase a f + single a b) j
case h
α : Type u_1
β : Type ?u.300562
γ : Type ?u.300565
ι : Type ?u.300568
M : Type u_2
M' : Type ?u.300574
N : Type ?u.300577
P : Type ?u.300580
G : Type ?u.300583
H : Type ?u.300586
R : Type ?u.300589
S : Type ?u.300592
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
j : α
⊢ ↑(update f a b) j = ↑(erase a f + single a b) j
rcases eq_or_ne a j with (rfl | h)
no goals
case h.inl
α : Type u_1
β : Type ?u.300562
γ : Type ?u.300565
ι : Type ?u.300568
M : Type u_2
M' : Type ?u.300574
N : Type ?u.300577
P : Type ?u.300580
G : Type ?u.300583
H : Type ?u.300586
R : Type ?u.300589
S : Type ?u.300592
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
⊢ ↑(update f a b) a = ↑(erase a f + single a b) a
simp
no goals
case h.inr
α : Type u_1
β : Type ?u.300562
γ : Type ?u.300565
ι : Type ?u.300568
M : Type u_2
M' : Type ?u.300574
N : Type ?u.300577
P : Type ?u.300580
G : Type ?u.300583
H : Type ?u.300586
R : Type ?u.300589
S : Type ?u.300592
inst✝ : AddZeroClass M
f : α →₀ M
a : α
b : M
j : α
h : a ≠ j
⊢ ↑(update f a b) j = ↑(erase a f + single a b) j
simp [Function.update_noteq h.symm, single_apply, h, erase_ne, h.symm]