no goals
α : Type u_1
β : Type u_2
γ : Type ?u.87566
f g : α → β
c c₁ c₂ x✝ : α
inst✝ : AddCommGroup α
h : Periodic f c
a x : α
⊢ (fun x => f (a - x)) (x + c) = (fun x => f (a - x)) x
simp only [← sub_sub, h.sub_eq]