x : ℂ
⊢ ∃ a, sin a = x
⊢ Function.Surjective sin
intro x
case intro
z : ℂ
⊢ ∃ a, sin a = cos z
x : ℂ
⊢ ∃ a, sin a = x
rcases cos_surjective x with ⟨z, rfl⟩
no goals
case intro
z : ℂ
⊢ ∃ a, sin a = cos z
exact ⟨z + π / 2, sin_add_pi_div_two z⟩