case h
ψ x✝ : ℝ
⊢ sin ↑x✝ = Real.sin ψ ↔ ↑x✝ = ↑ψ ∨ ↑x✝ + ↑ψ = ↑π
θ : Angle
ψ : ℝ
⊢ sin θ = Real.sin ψ ↔ θ = ↑ψ ∨ θ + ↑ψ = ↑π
induction θ using Real.Angle.induction_on
no goals
case h
ψ x✝ : ℝ
⊢ sin ↑x✝ = Real.sin ψ ↔ ↑x✝ = ↑ψ ∨ ↑x✝ + ↑ψ = ↑π
exact sin_eq_iff_coe_eq_or_add_eq_pi