θ : Angle
⊢ sin θ = sin 0 ↔ θ = 0 ∨ θ = ↑π
θ : Angle
⊢ sin θ = 0 ↔ θ = 0 ∨ θ = ↑π
nth_rw 1 [← sin_zero]
θ : Angle
⊢ θ = 0 ∨ θ + 0 = ↑π ↔ θ = 0 ∨ θ = ↑π
θ : Angle
⊢ sin θ = sin 0 ↔ θ = 0 ∨ θ = ↑π
rw [sin_eq_iff_eq_or_add_eq_pi]
no goals
θ : Angle
⊢ θ = 0 ∨ θ + 0 = ↑π ↔ θ = 0 ∨ θ = ↑π
simp