no goals
α : Type u_4
β : Type ?u.49269
γ : Type ?u.49272
ι : Type ?u.49275
M : Type u_3
M' : Type ?u.49281
N : Type u_1
P : Type u_2
G : Type ?u.49290
H : Type ?u.49293
R : Type ?u.49296
S : Type ?u.49299
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid P
f : N →+ P
f₂ : M →+ N
⊢ (↑f ∘ ↑f₂) 0 = 0
simp only [comp_apply, map_zero]