no goals
α : Type u_1
β : Type u_2
γ : Type ?u.81127
f g : α → β
c c₁ c₂ x✝ : α
inst✝ : AddGroup α
h1 : Periodic f c₁
h2 : Periodic f c₂
x : α
⊢ f (x + (c₁ - c₂)) = f x
rw [sub_eq_add_neg, ← add_assoc, h2.neg, h1]