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

State before:
G : Type ?u.78830
inst✝ : AddCommGroup G
f✝ : G → ℤ
bound✝ : ℕ
h✝ : AlmostAdditive f✝ bound✝
m n✝ : ℤ
g : G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
⊢ |f n| ≤ (bound + |f 1|) * |n| + bound
Tactic:
lax_exact h.linear_growth_upper_bound n 1
State after:
case e_a.e_m.e_a
G : Type ?u.78830
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.78830
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