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

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

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

State before:
G : Type u_1
inst✝ : AddCommGroup G
f₁ : ℤ → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ |f₁ (f₂ (x + y)) - f₁ (f₂ (x + y) - f₂ x - f₂ y) - f₁ (f₂ x + f₂ y)| + |f₁ (f₂ (x + y) - f₂ x - f₂ y)| +
      |f₁ (f₂ x + f₂ y) - f₁ (f₂ x) - f₁ (f₂ y)| ≤
    bound₁ + ((bound₁ + |f₁ 1|) * |f₂ (x + y) - f₂ x - f₂ y| + bound₁) + bound₁
Tactic:
conv in f₁ (f₂ (x + y)) =>
  
  rw [show f₂ (x + y) = (f₂ (x + y) - f₂ x - f₂ y) + (f₂ x + f₂ y)
      by linarith]
State after:
G : Type u_1
inst✝ : AddCommGroup G
f₁ : ℤ → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ |f₁ (f₂ (x + y) - f₂ x - f₂ y + (f₂ x + f₂ y)) - f₁ (f₂ (x + y) - f₂ x - f₂ y) - f₁ (f₂ x + f₂ y)| +
        |f₁ (f₂ (x + y) - f₂ x - f₂ y)| +
      |f₁ (f₂ x + f₂ y) - f₁ (f₂ x) - f₁ (f₂ y)| ≤
    bound₁ + ((bound₁ + |f₁ 1|) * |f₂ (x + y) - f₂ x - f₂ y| + bound₁) + bound₁

State before:
G : Type u_1
inst✝ : AddCommGroup G
f₁ : ℤ → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ |f₁ (f₂ (x + y) - f₂ x - f₂ y + (f₂ x + f₂ y)) - f₁ (f₂ (x + y) - f₂ x - f₂ y) - f₁ (f₂ x + f₂ y)| +
        |f₁ (f₂ (x + y) - f₂ x - f₂ y)| +
      |f₁ (f₂ x + f₂ y) - f₁ (f₂ x) - f₁ (f₂ y)| ≤
    bound₁ + ((bound₁ + |f₁ 1|) * |f₂ (x + y) - f₂ x - f₂ y| + bound₁) + bound₁
Tactic:
refine Nat.add_le_add₃ ?_ ?using_lemma ?_
State after:
case refine_1
G : Type u_1
inst✝ : AddCommGroup G
f₁ : ℤ → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ |f₁ (f₂ (x + y) - f₂ x - f₂ y + (f₂ x + f₂ y)) - f₁ (f₂ (x + y) - f₂ x - f₂ y) - f₁ (f₂ x + f₂ y)| ≤ bound₁

case using_lemma
G : Type u_1
inst✝ : AddCommGroup G
f₁ : ℤ → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ |f₁ (f₂ (x + y) - f₂ x - f₂ y)| ≤ (bound₁ + |f₁ 1|) * |f₂ (x + y) - f₂ x - f₂ y| + bound₁

case refine_2
G : Type u_1
inst✝ : AddCommGroup G
f₁ : ℤ → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ |f₁ (f₂ x + f₂ y) - f₁ (f₂ x) - f₁ (f₂ y)| ≤ bound₁

State before:
G : Type u_1
inst✝ : AddCommGroup G
f₁ : ℤ → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ |f₁ (f₂ (x + y) - f₂ x - f₂ y)| ≤ (bound₁ + |f₁ 1|) * |f₂ (x + y) - f₂ x - f₂ y| + bound₁
Tactic:
case using_lemma => apply h₁.linear_growth_upper_bound_int
State after:
no goals

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

case refine_2
G : Type u_1
inst✝ : AddCommGroup G
f₁ : ℤ → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ |f₁ (f₂ x + f₂ y) - f₁ (f₂ x) - f₁ (f₂ y)| ≤ bound₁
Tactic:
all_goals apply h₁.almost_additive
State after:
no goals

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

State before:
G : Type u_1
inst✝ : AddCommGroup G
f₁ : ℤ → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ |f₁ (f₂ (x + y) - f₂ x - f₂ y)| ≤ (bound₁ + |f₁ 1|) * |f₂ (x + y) - f₂ x - f₂ y| + bound₁
Tactic:
apply h₁.linear_growth_upper_bound_int
State after:
no goals

State before:
case refine_2
G : Type u_1
inst✝ : AddCommGroup G
f₁ : ℤ → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ |f₁ (f₂ x + f₂ y) - f₁ (f₂ x) - f₁ (f₂ y)| ≤ bound₁
Tactic:
apply h₁.almost_additive
State after:
no goals

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