Theorem: AlmostAdditive.almost_smul (RealsQuasiMorphisms/Basic.lean)

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |f (m • g) - m * f g| ≤ bound * (|m| + 1)
Tactic:
cases m <;> (rename_i m; induction m)
State after:
case ofNat.zero
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
⊢ |f (Int.ofNat Nat.zero • g) - Int.ofNat Nat.zero * f g| ≤ bound * (|Int.ofNat Nat.zero| + 1)

case ofNat.succ
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
n✝ : ℕ
n_ih✝ : |f (Int.ofNat n✝ • g) - Int.ofNat n✝ * f g| ≤ bound * (|Int.ofNat n✝| + 1)
⊢ |f (Int.ofNat (Nat.succ n✝) • g) - Int.ofNat (Nat.succ n✝) * f g| ≤ bound * (|Int.ofNat (Nat.succ n✝)| + 1)

case negSucc.zero
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
⊢ |f (Int.negSucc Nat.zero • g) - Int.negSucc Nat.zero * f g| ≤ bound * (|Int.negSucc Nat.zero| + 1)

case negSucc.succ
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
n✝ : ℕ
n_ih✝ : |f (Int.negSucc n✝ • g) - Int.negSucc n✝ * f g| ≤ bound * (|Int.negSucc n✝| + 1)
⊢ |f (Int.negSucc (Nat.succ n✝) • g) - Int.negSucc (Nat.succ n✝) * f g| ≤ bound * (|Int.negSucc (Nat.succ n✝)| + 1)

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
⊢ |f (Int.ofNat Nat.zero • g) - Int.ofNat Nat.zero * f g| ≤ bound * (|Int.ofNat Nat.zero| + 1)
Tactic:
case ofNat.zero => simp; exact h.almost_zero
State after:
no goals

State before:
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)
Tactic:
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
State after:
no goals

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
⊢ |f (Int.negSucc Nat.zero • g) - Int.negSucc Nat.zero * f g| ≤ bound * (|Int.negSucc Nat.zero| + 1)
Tactic:
case negSucc.zero =>
  rewrite [show Int.negSucc Nat.zero = -1 by rfl]; simpa using h.almost_neg g
State after:
no goals

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ |f (Int.negSucc (Nat.succ m) • g) - Int.negSucc (Nat.succ m) * f g| ≤ bound * (|Int.negSucc (Nat.succ m)| + 1)
Tactic:
case negSucc.succ m hᵢ =>
  conv => lhs; rewrite [←Int.negSucc_sub_one]
  rewrite [sub_zsmul, one_zsmul, sub_mul, one_mul]
  calc |f (Int.negSucc m • g + -g) - (Int.negSucc m * f g - f g)|
      = |(-(f (Int.negSucc m • g) - f (Int.negSucc m • g + -g) - f g))
         + (f (Int.negSucc m • g) - Int.negSucc m * f g)|
          := congrArg Int.natAbs <| by linarith
    _ ≤ |f (Int.negSucc m • g) - f (Int.negSucc m • g + -g) - f g|
        + |f (Int.negSucc m • g) - Int.negSucc m * f g|
          := by conv => rhs; arg 1; rewrite [←Int.natAbs_neg]
                apply Int.natAbs_add_le
    _ ≤ bound + bound * (|Int.negSucc m| + 1)
          := Nat.add_le_add (by rewrite [←congrArg f <| neg_add_cancel_right ..]
                                apply h.almost_additive _ g)
                            hᵢ
    _ = bound * (|Int.negSucc m.succ| + 1)
          := by simp only [Int.natAbs_negSucc]; linarith
State after:
no goals

State before:
case negSucc
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
a✝ : ℕ
⊢ |f (Int.negSucc a✝ • g) - Int.negSucc a✝ * f g| ≤ bound * (|Int.negSucc a✝| + 1)
Tactic:
rename_i m
State after:
case negSucc
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
⊢ |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)

State before:
case negSucc
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
⊢ |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
Tactic:
induction m
State after:
case negSucc.zero
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
⊢ |f (Int.negSucc Nat.zero • g) - Int.negSucc Nat.zero * f g| ≤ bound * (|Int.negSucc Nat.zero| + 1)

case negSucc.succ
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
n✝ : ℕ
n_ih✝ : |f (Int.negSucc n✝ • g) - Int.negSucc n✝ * f g| ≤ bound * (|Int.negSucc n✝| + 1)
⊢ |f (Int.negSucc (Nat.succ n✝) • g) - Int.negSucc (Nat.succ n✝) * f g| ≤ bound * (|Int.negSucc (Nat.succ n✝)| + 1)

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
⊢ |f (Int.ofNat Nat.zero • g) - Int.ofNat Nat.zero * f g| ≤ bound * (|Int.ofNat Nat.zero| + 1)
Tactic:
simp
State after:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
⊢ |f 0| ≤ bound

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
⊢ |f 0| ≤ bound
Tactic:
exact h.almost_zero
State after:
no goals

State before:
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)
Tactic:
rewrite [Int.ofNat_eq_coe, ofNat_zsmul] at hᵢ ⊢
State after:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (m • g) - ↑m * f g| ≤ bound * (|↑m| + 1)
⊢ |f (Nat.succ m • g) - ↑(Nat.succ m) * f g| ≤ bound * (|↑(Nat.succ m)| + 1)

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (m • g) - ↑m * f g| ≤ bound * (|↑m| + 1)
⊢ |f (Nat.succ m • g) - ↑(Nat.succ m) * f g| ≤ bound * (|↑(Nat.succ m)| + 1)
Tactic:
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]
State after:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (m • g) - ↑m * f g| ≤ bound * (|↑m| + 1)
⊢ |f (g + m • g) - (f g + ↑m * f g)| ≤ bound * (|↑(Nat.succ m)| + 1)

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (m • g) - ↑m * f g| ≤ bound * (|↑m| + 1)
⊢ |f (g + m • g) - (f g + ↑m * f g)| ≤ bound * (|↑(Nat.succ m)| + 1)
Tactic:
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
State after:
no goals

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (m • g) - ↑m * f g| ≤ bound * (|↑m| + 1)
⊢ ↑(Nat.succ m) * f g = f g + ↑m * f g
Tactic:
rewrite [Nat.succ_eq_add_one, Nat.cast_succ]
State after:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (m • g) - ↑m * f g| ≤ bound * (|↑m| + 1)
⊢ (↑m + 1) * f g = f g + ↑m * f g

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (m • g) - ↑m * f g| ≤ bound * (|↑m| + 1)
⊢ (↑m + 1) * f g = f g + ↑m * f g
Tactic:
linarith
State after:
no goals

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (m • g) - ↑m * f g| ≤ bound * (|↑m| + 1)
⊢ f (g + m • g) - (f g + ↑m * f g) = f (g + m • g) - f g - f (m • g) + (f (m • g) - ↑m * f g)
Tactic:
linarith
State after:
no goals

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (m • g) - ↑m * f g| ≤ bound * (|↑m| + 1)
⊢ bound + bound * (m + 1) = bound * (Nat.succ m + 1)
Tactic:
linarith
State after:
no goals

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
⊢ |f (Int.negSucc Nat.zero • g) - Int.negSucc Nat.zero * f g| ≤ bound * (|Int.negSucc Nat.zero| + 1)
Tactic:
rewrite [show Int.negSucc Nat.zero = -1 by rfl]
State after:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
⊢ |f (-1 • g) - -1 * f g| ≤ bound * (|-1| + 1)

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
⊢ |f (-1 • g) - -1 * f g| ≤ bound * (|-1| + 1)
Tactic:
simpa using h.almost_neg g
State after:
no goals

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
⊢ Int.negSucc Nat.zero = -1
Tactic:
rfl
State after:
no goals

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ |f (Int.negSucc (Nat.succ m) • g) - Int.negSucc (Nat.succ m) * f g| ≤ bound * (|Int.negSucc (Nat.succ m)| + 1)
Tactic:
conv => lhs; rewrite [←Int.negSucc_sub_one]
State after:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ |f ((Int.negSucc m - 1) • g) - (Int.negSucc m - 1) * f g| ≤ bound * (|Int.negSucc (Nat.succ m)| + 1)

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ |f ((Int.negSucc m - 1) • g) - (Int.negSucc m - 1) * f g| ≤ bound * (|Int.negSucc (Nat.succ m)| + 1)
Tactic:
rewrite [sub_zsmul, one_zsmul, sub_mul, one_mul]
State after:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ |f (Int.negSucc m • g + -g) - (Int.negSucc m * f g - f g)| ≤ bound * (|Int.negSucc (Nat.succ m)| + 1)

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ |f (Int.negSucc m • g + -g) - (Int.negSucc m * f g - f g)| ≤ bound * (|Int.negSucc (Nat.succ m)| + 1)
Tactic:
calc |f (Int.negSucc m • g + -g) - (Int.negSucc m * f g - f g)|
    = |(-(f (Int.negSucc m • g) - f (Int.negSucc m • g + -g) - f g))
       + (f (Int.negSucc m • g) - Int.negSucc m * f g)|
        := congrArg Int.natAbs <| by linarith
  _ ≤ |f (Int.negSucc m • g) - f (Int.negSucc m • g + -g) - f g|
      + |f (Int.negSucc m • g) - Int.negSucc m * f g|
        := by conv => rhs; arg 1; rewrite [←Int.natAbs_neg]
              apply Int.natAbs_add_le
  _ ≤ bound + bound * (|Int.negSucc m| + 1)
        := Nat.add_le_add (by rewrite [←congrArg f <| neg_add_cancel_right ..]
                              apply h.almost_additive _ g)
                          hᵢ
  _ = bound * (|Int.negSucc m.succ| + 1)
        := by simp only [Int.natAbs_negSucc]; linarith
State after:
no goals

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ f (Int.negSucc m • g + -g) - (Int.negSucc m * f g - f g) =
    -(f (Int.negSucc m • g) - f (Int.negSucc m • g + -g) - f g) + (f (Int.negSucc m • g) - Int.negSucc m * f g)
Tactic:
linarith
State after:
no goals

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ |-(f (Int.negSucc m • g) - f (Int.negSucc m • g + -g) - f g) + (f (Int.negSucc m • g) - Int.negSucc m * f g)| ≤
    |f (Int.negSucc m • g) - f (Int.negSucc m • g + -g) - f g| + |f (Int.negSucc m • g) - Int.negSucc m * f g|
Tactic:
conv => rhs; arg 1; rewrite [←Int.natAbs_neg]
State after:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ |-(f (Int.negSucc m • g) - f (Int.negSucc m • g + -g) - f g) + (f (Int.negSucc m • g) - Int.negSucc m * f g)| ≤
    |-(f (Int.negSucc m • g) - f (Int.negSucc m • g + -g) - f g)| + |f (Int.negSucc m • g) - Int.negSucc m * f g|

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ |-(f (Int.negSucc m • g) - f (Int.negSucc m • g + -g) - f g) + (f (Int.negSucc m • g) - Int.negSucc m * f g)| ≤
    |-(f (Int.negSucc m • g) - f (Int.negSucc m • g + -g) - f g)| + |f (Int.negSucc m • g) - Int.negSucc m * f g|
Tactic:
apply Int.natAbs_add_le
State after:
no goals

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ |f (Int.negSucc m • g) - f (Int.negSucc m • g + -g) - f g| ≤ bound
Tactic:
rewrite [←congrArg f <| neg_add_cancel_right ..]
State after:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ |f (Int.negSucc m • g + -?m.60523 + ?m.60523) - f (Int.negSucc m • g + -g) - f g| ≤ bound

G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ G

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ |f (Int.negSucc m • g + -?m.60523 + ?m.60523) - f (Int.negSucc m • g + -g) - f g| ≤ bound

G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ G
Tactic:
apply h.almost_additive _ g
State after:
no goals

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ bound + bound * (|Int.negSucc m| + 1) = bound * (|Int.negSucc (Nat.succ m)| + 1)
Tactic:
simp only [Int.natAbs_negSucc]
State after:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ bound + bound * (Nat.succ m + 1) = bound * (Nat.succ (Nat.succ m) + 1)

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ bound + bound * (Nat.succ m + 1) = bound * (Nat.succ (Nat.succ m) + 1)
Tactic:
linarith
State after:
no goals