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₂
n : ℤ
triag :
  |n * toFun (AlmostHom.comp f₁ f₂) n - n * toFun (AlmostHom.comp f₂ f₁) n| ≤
    |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| +
      |toFun f₂ n * toFun f₁ n - n * toFun (AlmostHom.comp f₂ f₁) n|
⊢ |toFun (AlmostHom.comp f₁ f₂) n - toFun (AlmostHom.comp f₂ f₁) n| ≤ ?m.49722

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₂
⊢ ℕ

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₂
⊢ ℕ

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₂
⊢ ℕ
no goals