[GOAL]
α : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
f : α → α
g : α → M
m n : ℕ
x : α
⊢ birkhoffSum f g (m + n) x = birkhoffSum f g m x + birkhoffSum f g n (f^[m] x)
[PROOFSTEP]
simp_rw [birkhoffSum, sum_range_add, add_comm m, iterate_add_apply]
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
f : α → α
x : α
h : IsFixedPt f x
g : α → M
n : ℕ
⊢ birkhoffSum f g n x = n • g x
[PROOFSTEP]
simp [birkhoffSum, (h.iterate _).eq]
[GOAL]
α : Type u_1
G : Type u_2
inst✝ : AddCommGroup G
f : α → α
g : α → G
n : ℕ
x : α
⊢ birkhoffSum f g n (f x) - birkhoffSum f g n x = g (f^[n] x) - g x
[PROOFSTEP]
rw [← sub_eq_iff_eq_add.2 (birkhoffSum_succ f g n x), ← sub_eq_iff_eq_add.2 (birkhoffSum_succ' f g n x), ← sub_add, ←
  sub_add, sub_add_comm]
