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

State before:
G : Type ?u.87514
inst✝ : AddCommGroup G
f✝ : G → ℤ
bound✝ : ℕ
h✝ : AlmostAdditive f✝ bound✝
m n✝ : ℤ
g : G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
⊢ (|f 1| - bound) * |n| - bound ≤ |f n|
Tactic:
lax_exact h.linear_growth_lower_bound n 1
State after:
case e_a.e_m.e_a
G : Type ?u.87514
inst✝ : AddCommGroup G
f✝ : G → ℤ
bound✝ : ℕ
h✝ : AlmostAdditive f✝ bound✝
m n✝ : ℤ
g : G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
⊢ n = n • 1

State before:
case e_a.e_m.e_a
G : Type ?u.87514
inst✝ : AddCommGroup G
f✝ : G → ℤ
bound✝ : ℕ
h✝ : AlmostAdditive f✝ bound✝
m n✝ : ℤ
g : G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
⊢ n = n • 1
Tactic:
rw [zsmul_int_one]
State after:
no goals