no goals
α : Type u_1
β : Type ?u.43277
γ : Type ?u.43280
ι : Type ?u.43283
M : Type u_2
M' : Type ?u.43289
N : Type ?u.43292
P : Type ?u.43295
G : Type ?u.43298
H : Type ?u.43301
R : Type ?u.43304
S : Type ?u.43307
inst✝ : Zero M
a✝ a' : α
b : M
a : α
⊢ (fun f => ↑f) (single a 0) = (fun f => ↑f) 0
classical simpa only [single_eq_update, coe_zero] using Function.update_eq_self a (0 : α → M)
no goals
α : Type u_1
β : Type ?u.43277
γ : Type ?u.43280
ι : Type ?u.43283
M : Type u_2
M' : Type ?u.43289
N : Type ?u.43292
P : Type ?u.43295
G : Type ?u.43298
H : Type ?u.43301
R : Type ?u.43304
S : Type ?u.43307
inst✝ : Zero M
a✝ a' : α
b : M
a : α
⊢ (fun f => ↑f) (single a 0) = (fun f => ↑f) 0
simpa only [single_eq_update, coe_zero] using Function.update_eq_self a (0 : α → M)