z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ arg z = -arccos (z.re / ↑abs z)
z : ℂ
hz : z.im < 0
⊢ arg z = -arccos (z.re / ↑abs z)
have h₀ : z ≠ 0 := mt (congr_arg im) hz.ne
case hx₁
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ 0 ≤ -arg z

case hx₂
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ -arg z ≤ π
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ arg z = -arccos (z.re / ↑abs z)
rw [← cos_arg h₀, ← Real.cos_neg, Real.arccos_cos, neg_neg]
no goals
case hx₁
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ 0 ≤ -arg z

case hx₂
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ -arg z ≤ π
exacts [neg_nonneg.2 (arg_neg_iff.2 hz).le, neg_le.2 (neg_pi_lt_arg z).le]