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