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

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |f ((m * n) • g) - n * f (m • g)| + |f ((m * n) • g) - m * f (n • g)| =
    |f (n • m • g) - n * f (m • g)| + |f (m • n • g) - m * f (n • g)|
Tactic:
congr 3
State after:
case e_a.e_m.e_a
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ f ((m * n) • g) = f (n • m • g)

case e_a.e_m.e_a
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ f ((m * n) • g) = f (m • n • g)

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |f (n • m • g) - n * f (m • g)| + |f (m • n • g) - m * f (n • g)| ≤ bound * (|n| + 1) + bound * (|m| + 1)
Tactic:
apply Nat.add_le_add <;> apply h.almost_smul
State after:
no goals

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ bound * (|n| + 1) + bound * (|m| + 1) = bound * (|m| + |n| + 2)
Tactic:
linarith
State after:
no goals