case inl

⊢ 0 ≤ arg 0 ↔ 0 ≤ 0.im

case inr
z : ℂ
h₀ : z ≠ 0
⊢ 0 ≤ arg z ↔ 0 ≤ z.im
z : ℂ
⊢ 0 ≤ arg z ↔ 0 ≤ z.im
rcases eq_or_ne z 0 with (rfl | h₀)
no goals
case inr
z : ℂ
h₀ : z ≠ 0
⊢ 0 ≤ arg z ↔ 0 ≤ z.im
calc
  0 ≤ arg z ↔ 0 ≤ Real.sin (arg z) :=
    ⟨fun h => Real.sin_nonneg_of_mem_Icc ⟨h, arg_le_pi z⟩, by
      contrapose!
      intro h
      exact Real.sin_neg_of_neg_of_neg_pi_lt h (neg_pi_lt_arg _)⟩
  _ ↔ _ := by rw [sin_arg, le_div_iff (abs.pos h₀), MulZeroClass.zero_mul]
no goals
case inl

⊢ 0 ≤ arg 0 ↔ 0 ≤ 0.im
simp
z : ℂ
h₀ : z ≠ 0
⊢ arg z < 0 → Real.sin (arg z) < 0
z : ℂ
h₀ : z ≠ 0
⊢ 0 ≤ Real.sin (arg z) → 0 ≤ arg z
contrapose!
z : ℂ
h₀ : z ≠ 0
h : arg z < 0
⊢ Real.sin (arg z) < 0
z : ℂ
h₀ : z ≠ 0
⊢ arg z < 0 → Real.sin (arg z) < 0
intro h
no goals
z : ℂ
h₀ : z ≠ 0
h : arg z < 0
⊢ Real.sin (arg z) < 0
exact Real.sin_neg_of_neg_of_neg_pi_lt h (neg_pi_lt_arg _)
no goals
z : ℂ
h₀ : z ≠ 0
⊢ 0 ≤ Real.sin (arg z) ↔ 0 ≤ z.im
rw [sin_arg, le_div_iff (abs.pos h₀), MulZeroClass.zero_mul]