case inl
z : ℂ
hre : 0 ≤ z.re
⊢ -(π / 2) ≤ arg z ↔ 0 ≤ z.re ∨ 0 ≤ z.im

case inr
z : ℂ
hre : z.re < 0
⊢ -(π / 2) ≤ arg z ↔ 0 ≤ z.re ∨ 0 ≤ z.im
z : ℂ
⊢ -(π / 2) ≤ arg z ↔ 0 ≤ z.re ∨ 0 ≤ z.im
cases' le_or_lt 0 (re z) with hre hre
case inr
z : ℂ
hre : z.re < 0
⊢ -(π / 2) ≤ arg z ↔ 0 ≤ z.im
case inr
z : ℂ
hre : z.re < 0
⊢ -(π / 2) ≤ arg z ↔ 0 ≤ z.re ∨ 0 ≤ z.im
simp only [hre.not_le, false_or_iff]
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ -(π / 2) ≤ arg z ↔ 0 ≤ z.im

case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ -(π / 2) ≤ arg z ↔ 0 ≤ z.im
case inr
z : ℂ
hre : z.re < 0
⊢ -(π / 2) ≤ arg z ↔ 0 ≤ z.im
cases' le_or_lt 0 (im z) with him him
no goals
case inl
z : ℂ
hre : 0 ≤ z.re
⊢ -(π / 2) ≤ arg z ↔ 0 ≤ z.re ∨ 0 ≤ z.im
simp only [hre, arg_of_re_nonneg hre, Real.neg_pi_div_two_le_arcsin, true_or_iff]
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ -(π / 2) ≤ arg z ↔ True
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ -(π / 2) ≤ arg z ↔ 0 ≤ z.im
simp only [him]
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ -(π / 2) ≤ arcsin ((-z).im / ↑abs z) + π
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ -(π / 2) ≤ arg z ↔ True
rw [iff_true_iff, arg_of_re_neg_of_im_nonneg hre him]
no goals
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ -(π / 2) ≤ arcsin ((-z).im / ↑abs z) + π
exact (Real.neg_pi_div_two_le_arcsin _).trans (le_add_of_nonneg_right Real.pi_pos.le)
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ -(π / 2) ≤ arg z ↔ False
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ -(π / 2) ≤ arg z ↔ 0 ≤ z.im
simp only [him.not_le]
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ z.re ≠ 0

case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ 0 < ↑abs z
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ -(π / 2) ≤ arg z ↔ False
rw [iff_false_iff, not_le, arg_of_re_neg_of_im_neg hre him, sub_lt_iff_lt_add', ←
  sub_eq_add_neg, sub_half, Real.arcsin_lt_pi_div_two, div_lt_one, neg_im, ← abs_of_neg him,
  abs_im_lt_abs]
no goals
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ z.re ≠ 0

case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ 0 < ↑abs z
exacts [hre.ne, abs.pos <| ne_of_apply_ne re hre.ne]