specialize hlin n
G : Type ?u.41105
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
a' b' : ℕ
hlin : ∀ (n : ℤ), |toFun f₂ n| ≤ a' * |n| + b'
b₁ : ℕ
hf₁ : AlmostAdditive f₁.toFun b₁
n : ℤ
hypcomm : |n * toFun f₁ (toFun f₂ n • 1) - toFun f₂ n * toFun f₁ (n • 1)| ≤ b₁ * (|toFun f₂ n| + |n| + 2)
⊢ |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * ?m.41850
G : Type ?u.41105
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
a' b' : ℕ
hlin✝ : ∀ (n : ℤ), |toFun f₂ n| ≤ a' * |n| + b'
b₁ : ℕ
hf₁ : AlmostAdditive f₁.toFun b₁
n : ℤ
hypcomm : |n * toFun f₁ (toFun f₂ n • 1) - toFun f₂ n * toFun f₁ (n • 1)| ≤ b₁ * (|toFun f₂ n| + |n| + 2)
hlin : |toFun f₂ n| ≤ a' * |n| + b'
⊢ |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * ?m.41850