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

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |f (-g) - -f g| ≤ |f (-g) + f g - f 0| + |f 0|
Tactic:
lax_exact Int.natAbs_add_le (f (-g) + f g - f 0) (f 0)
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 (-g) - -f g = f (-g) + f g - f 0 + f 0

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 (-g) - -f g = f (-g) + f g - f 0 + f 0
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 (-g) + f g - f 0| + |f 0| = |f (-g + g) - f (-g) - f g| + |f 0|
Tactic:
congr 1
State after:
case e_a
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |f (-g) + f g - f 0| = |f (-g + g) - f (-g) - f g|

State before:
case e_a
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |f (-g) + f g - f 0| = |f (-g + g) - f (-g) - f g|
Tactic:
rewrite [←Int.natAbs_neg, ←add_left_neg g]
State after:
case e_a
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |-(f (-g) + f g - f (-g + g))| = |f (-g + g) - f (-g) - f g|

State before:
case e_a
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |-(f (-g) + f g - f (-g + g))| = |f (-g + g) - f (-g) - f g|
Tactic:
congr
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 (-g) + f g - f (-g + g)) = f (-g + g) - f (-g) - 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 (-g) + f g - f (-g + g)) = f (-g + g) - f (-g) - 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 (-g + g) - f (-g) - f g| + |f 0| ≤ bound * 2
Tactic:
linarith [h.almost_additive (-g) g, h.almost_zero]
State after:
no goals