no goals
α : Type u_1
β : Type ?u.26168
γ : Type ?u.26171
ι : Type ?u.26174
M : Type u_2
M' : Type ?u.26180
N : Type ?u.26183
P : Type ?u.26186
G : Type ?u.26189
H : Type ?u.26192
R : Type ?u.26195
S : Type ?u.26198
inst✝¹ : Zero M
inst✝ : Unique α
f g : α →₀ M
h : ↑f default = ↑g default
a : α
⊢ ↑f a = ↑g a
rwa [Unique.eq_default a]