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

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

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ : G → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ |f₁ (x + y) - f₁ x - f₁ y + (f₂ (x + y) - f₂ x - f₂ y)| ≤ bound₁ + bound₂
Tactic:
transitivity
State after:
case a
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ : G → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ |f₁ (x + y) - f₁ x - f₁ y + (f₂ (x + y) - f₂ x - f₂ y)| ≤ ?m

case a
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ : G → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ ?m ≤ bound₁ + bound₂

case m
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ : G → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ ℕ