exact ⟨_, by
  intro n
  rewrite [show (-f₁.comp f₂ + f₂.comp f₁) n = (-f₁.comp f₂ n + f₂.comp f₁ n) from rfl,
           ←Int.natAbs_neg,
           show -(-f₁.comp f₂ n + f₂.comp f₁ n) = f₁.comp f₂ n - f₂.comp f₁ n by
             rw [neg_add_rev, neg_neg, sub_eq_neg_add]]
  have triag := Int.natAbs_add_le (n * (f₁.comp f₂ n) - f₂ n * f₁ n) (f₂ n * f₁ n - n * (f₂.comp f₁ n))
  simp only [sub_add_sub_cancel, Int.diff_eq] at triag
  if c: n = 0
  then
    simp only [c, zero_mul, zero_sub, Int.natAbs_neg, ge_iff_le] at hf₁ hf₂ |-
    exact self_le_add_right |(f₁.comp f₂ - f₂.comp f₁) 0| (2*(k₁ + k₂))
  else
  have goal_mul_n :=
    calc |n| * |f₁.comp f₂ n - f₂.comp f₁ n|
      = |n*f₁.comp f₂ n - n*f₂.comp f₁ n| := by rw [←Int.natAbs_mul, mul_sub_left_distrib]
    _ ≤ |n*f₁.comp f₂ n - f₂ n * f₁ n| + |f₂ n * f₁ n - n*f₂.comp f₁ n| := triag
    _ ≤ |n*f₁.comp f₂ n - f₂ n * f₁ n| + (|n|+1)*k₂  :=
        by
          rw [mul_comm (f₂ n), ←Int.natAbs_neg (f₁ n * f₂ n - n * f₂.comp f₁ n)]
          apply Nat.add_le_add_left;
          simp only [neg_sub, Int.diff_eq]; exact hf₂ ..
    _ ≤ (|n|+1)*k₁ + (|n|+1)*k₂ := Nat.add_le_add_right (hf₁ ..) ..
    _ = (|n|+1)*(k₁ + k₂) := by ring
    _ ≤ |n| * (2*(k₁ + k₂)) :=
        by
          rw [←mul_assoc, mul_comm |n|]
          exact Nat.mul_le_mul_of_nonneg_right <|
                succ_le_two_mul |n| <|
                Int.natAbs_ne_zero.2 c
  calc |f₁.comp f₂ n - f₂.comp f₁ n|
    ≤ 2*(k₁ + k₂) := le_of_mul_le_mul_left goal_mul_n
      <| Or.resolve_left (Nat.eq_zero_or_pos ..) (Int.natAbs_ne_zero.2 c)
  _ ≤ _ := self_le_add_left  (2*(k₁ + k₂)) |(f₁.comp f₂ - f₂.comp f₁) 0|⟩
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
⊢ ∃ bound, ∀ (g : ℤ), |toFun (-AlmostHom.comp f₁ f₂ + AlmostHom.comp f₂ f₁) g| ≤ bound
no goals