ext
G : Type u_1
inst✝ : AddCommGroup G
g : AlmostHom G
f₁ f₂ : AlmostHom ℤ
⊢ AlmostHom.comp (f₁ + f₂) g = AlmostHom.comp f₁ g + AlmostHom.comp f₂ g
case a.h
G : Type u_1
inst✝ : AddCommGroup G
g : AlmostHom G
f₁ f₂ : AlmostHom ℤ
x✝ : G
⊢ toFun (AlmostHom.comp (f₁ + f₂) g) x✝ = toFun (AlmostHom.comp f₁ g + AlmostHom.comp f₂ g) x✝