no goals
α : Type u_1
β : Type u_2
γ : Type ?u.84885
f g : α → β
c c₁ c₂ x✝ : α
inst✝ : AddCommSemigroup α
h : Periodic f c
a x : α
⊢ (fun x => f (x + a)) (x + c) = (fun x => f (x + a)) x
simpa only [add_right_comm] using h (x + a)