θ : Angle
⊢ cos (θ + ↑π) = -cos θ
⊢ Function.Antiperiodic cos ↑π
intro θ
case h
x✝ : ℝ
⊢ cos (↑x✝ + ↑π) = -cos ↑x✝
θ : Angle
⊢ cos (θ + ↑π) = -cos θ
induction θ using Real.Angle.induction_on
no goals
case h
x✝ : ℝ
⊢ cos (↑x✝ + ↑π) = -cos ↑x✝
exact Real.cos_antiperiodic _