Theorem: AlmostAdditive.almost_comp_add (RealsQuasiMorphisms/Ring.lean)

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ f₂ : G → ℤ
g : G
⊢ |HAdd.hAdd (-f ∘ (f₁ + f₂)) (f ∘ f₁ + f ∘ f₂) g| ≤ bound
Tactic:
show |(-f (f₁ g + f₂ g)) + (f (f₁ g) + f (f₂ g))| ≤ bound
State after:
G : Type u_1
inst✝ : AddCommGroup G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ f₂ : G → ℤ
g : G
⊢ |-f (f₁ g + f₂ g) + (f (f₁ g) + f (f₂ g))| ≤ bound

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ f₂ : G → ℤ
g : G
⊢ |-f (f₁ g + f₂ g) + (f (f₁ g) + f (f₂ g))| ≤ bound
Tactic:
rewrite [←Int.natAbs_neg]
State after:
G : Type u_1
inst✝ : AddCommGroup G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ f₂ : G → ℤ
g : G
⊢ |-(-f (f₁ g + f₂ g) + (f (f₁ g) + f (f₂ g)))| ≤ bound

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ f₂ : G → ℤ
g : G
⊢ |-(-f (f₁ g + f₂ g) + (f (f₁ g) + f (f₂ g)))| ≤ bound
Tactic:
lax_exact h.almost_additive (f₁ g) (f₂ g)
State after:
case e_a.e_m
G : Type u_1
inst✝ : AddCommGroup G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ f₂ : G → ℤ
g : G
⊢ -(-f (f₁ g + f₂ g) + (f (f₁ g) + f (f₂ g))) = f (f₁ g + f₂ g) - f (f₁ g) - f (f₂ g)

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