no goals
α : Type u_1
β : Type u_2
γ : Type ?u.153445
f g : α → β
c c₁ c₂ x✝ : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
x : α
⊢ f (x - c) = -f x
simp only [← neg_eq_iff_eq_neg, ← h (x - c), sub_add_cancel]