calc |n * (f₁.comp f₂ n) - f₂ n * f₁ n|
    ≤ b₁*(|f₂ n| + |n| + 2) := hypcomm
  _ ≤ b₁*(a'*|n| + b' + |n| + 2) :=
      by apply mul_le_mul_of_nonneg_left
          (by simp only [add_le_add_iff_right, hlin]) (zero_le _)
  _ = b₁*(|n| * (a' + 1) + (b'+ 2)) := by ring
  _ ≤ b₁*(|n| * (a' + 1) + (b'+ 2)) + b₁*(a'+1) :=
      by simp only [le_add_iff_nonneg_right, zero_le]
  _ ≤ b₁*(|n| * (a' + 1) + (b'+ 2)) + b₁*(a'+1) + b₁*(|n|)*(b'+2) :=
      by simp only [le_add_iff_nonneg_right, zero_le]
  _ = (|n|+1)*(b₁*(a'+1 + b'+2)) := by ring
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 : ℤ
hlin : |toFun f₂ n| ≤ a' * |n| + b'
hypcomm : |n * toFun f₁ (toFun f₂ n) - toFun f₂ n * toFun f₁ n| ≤ b₁ * (|toFun f₂ n| + |n| + 2)
⊢ |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * ?m.41850
no goals