Injectivity/surjectivity of latitude-longitude chart in Lean via Complex.arg

For (u,v) ↦ (cos u cos v, sin u cos v, sin v) on Ioc (-π) π ×ˢ Ioo (-(π/2)) (π/2): latitude is injective by Real.injOn_sin (on Icc, use Ioo_subset_Icc_self); after cancelling cos v > 0 (cos_pos_of_mem_Ioo, mul_right_cancel₀) get cos u = cos u', sin u = sin u', then Complex.arg_cos_add_sin_mul_I hu — but its cos/sin are Complex.cos ↑u, so first rw [← Complex.ofReal_cos, ← Complex.ofReal_sin, hcu, hsu, Complex.ofReal_cos, Complex.ofReal_sin, Complex.arg_cos_add_sin_mul_I hu']. Surjectivity onto a zone: take v = arcsin z, u = Complex.arg ⟨x, y⟩, and use Complex.cos_arg hz0, Complex.sin_arg, Real.cos_arcsin, with ‖⟨x,y⟩‖ = √(1 - z²) from Complex.norm_def + Complex.normSq_apply; finish coordinatewise with ext i; fin_cases i <;> simp <;> field_simp. With an area formula this gives Archimedes' zone area 2π(b-a) in ~60 lines.