no goals
α : Type u_4
β : Type ?u.118278
γ : Type ?u.118281
ι : Type ?u.118284
M : Type u_1
M' : Type ?u.118290
N : Type u_2
P : Type u_3
G : Type ?u.118299
H : Type ?u.118302
R : Type ?u.118305
S : Type ?u.118308
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid P
f : M ≃+ N
f₂ : N ≃+ P
⊢ (↑f₂ ∘ ↑f) 0 = 0
simp