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

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

case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ arg z ≤ π / 2 ↔ z.im < 0
case inr
z : ℂ
hre : z.re < 0
⊢ arg z ≤ π / 2 ↔ z.im < 0
cases' le_or_lt 0 (im z) with him him
no goals
case inl
z : ℂ
hre : 0 ≤ z.re
⊢ arg z ≤ π / 2 ↔ 0 ≤ z.re ∨ z.im < 0
simp only [hre, arg_of_re_nonneg hre, Real.arcsin_le_pi_div_two, true_or_iff]
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ arg z ≤ π / 2 ↔ False
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ arg z ≤ π / 2 ↔ z.im < 0
simp only [him.not_lt]
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ z.re ≠ 0

case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ 0 < ↑abs z
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ arg z ≤ π / 2 ↔ False
rw [iff_false_iff, not_le, arg_of_re_neg_of_im_nonneg hre him, ← sub_lt_iff_lt_add, half_sub,
  Real.neg_pi_div_two_lt_arcsin, neg_im, neg_div, neg_lt_neg_iff, div_lt_one, ←
  _root_.abs_of_nonneg him, abs_im_lt_abs]
no goals
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ z.re ≠ 0

case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ 0 < ↑abs z
exacts [hre.ne, abs.pos <| ne_of_apply_ne re hre.ne]
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ arg z ≤ π / 2 ↔ True
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ arg z ≤ π / 2 ↔ z.im < 0
simp only [him]
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ arcsin ((-z).im / ↑abs z) - π ≤ π / 2
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ arg z ≤ π / 2 ↔ True
rw [iff_true_iff, arg_of_re_neg_of_im_neg hre him]
no goals
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ arcsin ((-z).im / ↑abs z) - π ≤ π / 2
exact (sub_le_self _ Real.pi_pos.le).trans (Real.arcsin_le_pi_div_two _)