no goals
α : Type u_1
β : Type u_2
γ : Type ?u.165187
f g : α → β
c c₁ c₂ x✝ : α
inst✝¹ : AddSemigroup α
inst✝ : Neg β
h : Antiperiodic f c
a x : α
⊢ (fun x => f (a + x)) (x + c) = -(fun x => f (a + x)) x
simpa [add_assoc] using h (a + x)