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

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |f (n • g)| ≤ |f (n • g) - n * f g| + |n * f g|
Tactic:
lax_exact Int.natAbs_add_le (f (n • g) - n * f g) (n * f g)
State after:
case e_a.e_m
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ f (n • g) = f (n • g) - n * f g + n * f g

State before:
case e_a.e_m
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ f (n • g) = f (n • g) - n * f g + n * f g
Tactic:
linarith
State after:
no goals

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |f (n • g) - n * f g| + |n * f g| ≤ (bound + |f g|) * |n| + bound
Tactic:
linarith [h.almost_smul n g, Int.natAbs_mul n (f g)]
State after:
no goals