no goals
α : Type u_1
β : Type ?u.13590
γ : Type ?u.13593
ι : Type ?u.13596
M : Type u_2
M' : Type ?u.13602
N : Type ?u.13605
P : Type ?u.13608
G : Type ?u.13611
H : Type ?u.13614
R : Type ?u.13617
S : Type ?u.13620
inst✝ : Zero M
f : α →₀ M
⊢ ↑f = 0 ↔ f = 0
rw [← coe_zero, FunLike.coe_fn_eq]