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

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ f₂ : G → ℤ
bound' : ℕ
h' : Bounded (-f₁ + f₂) bound'
g : G
⊢ -f (f₁ g) + f (f₂ g) = f (f₁ g + (f₂ g - f₁ g)) - f (f₁ g) - f (f₂ g - f₁ g) + f (f₂ g - f₁ g)
Tactic:
rw [Int.add_sub_cancel_right (f₁ g) (f₂ g),
    ←Int.sub_eq_neg_add, Int.sub_add_cancel]
State after:
no goals

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ f₂ : G → ℤ
bound' : ℕ
h' : Bounded (-f₁ + f₂) bound'
g : G
⊢ bound + ((bound + |f 1|) * bound' + bound) = (bound + |f 1|) * bound' + bound * 2
Tactic:
rw [Nat.add_comm, Nat.add_assoc, Nat.mul_two]
State after:
no goals