θ ψ : Angle
h : θ = ψ ∨ θ = ψ + ↑π
⊢ abs (sin θ) = abs (sin ψ)
θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ abs (sin θ) = abs (sin ψ)
rw [two_nsmul_eq_iff] at h
case inl
θ : Angle
⊢ abs (sin θ) = abs (sin θ)

case inr
ψ : Angle
⊢ abs (sin (ψ + ↑π)) = abs (sin ψ)
θ ψ : Angle
h : θ = ψ ∨ θ = ψ + ↑π
⊢ abs (sin θ) = abs (sin ψ)
rcases h with (rfl | rfl)
no goals
case inl
θ : Angle
⊢ abs (sin θ) = abs (sin θ)
rfl
no goals
case inr
ψ : Angle
⊢ abs (sin (ψ + ↑π)) = abs (sin ψ)
rw [sin_add_pi, abs_neg]