case h
θ : Angle
x✝ : ℝ
⊢ cos θ = cos ↑x✝ ↔ θ = ↑x✝ ∨ θ = -↑x✝
θ ψ : Angle
⊢ cos θ = cos ψ ↔ θ = ψ ∨ θ = -ψ
induction ψ using Real.Angle.induction_on
no goals
case h
θ : Angle
x✝ : ℝ
⊢ cos θ = cos ↑x✝ ↔ θ = ↑x✝ ∨ θ = -↑x✝
exact cos_eq_real_cos_iff_eq_or_eq_neg