case ofNat.succ m hᵢ =>
  rewrite [Int.ofNat_eq_coe, ofNat_zsmul] at hᵢ ⊢
  
  rewrite [show m.succ • g = g + m • g from AddMonoid.nsmul_succ ..,
           show ↑(m.succ) * f g = f g + m * f g
             by rewrite [Nat.succ_eq_add_one, Nat.cast_succ]; linarith]
  calc |f (g + m • g) - (f g + m * f g)|
      = |(f (g + m • g) - f g - f (m • g)) + (f (m • g) - m * f g)|
          := congrArg Int.natAbs <| by linarith
    _ ≤ |f (g + m • g) - f g - f (m • g)| + |f (m • g) - m * f g|
          := Int.natAbs_add_le ..
    _ ≤ bound + bound * (m + 1)
          := Nat.add_le_add (h.almost_additive ..) hᵢ
    _ = bound * (m.succ + 1)
          := by linarith
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.ofNat m • g) - Int.ofNat m * f g| ≤ bound * (|Int.ofNat m| + 1)
⊢ |f (Int.ofNat (Nat.succ m) • g) - Int.ofNat (Nat.succ m) * f g| ≤ bound * (|Int.ofNat (Nat.succ m)| + 1)
no goals