case pos
z : ℂ
h₀ : z = 0
⊢ arg z = -(π / 2) ↔ z.re = 0 ∧ z.im < 0

case neg
z : ℂ
h₀ : ¬z = 0
⊢ arg z = -(π / 2) ↔ z.re = 0 ∧ z.im < 0
z : ℂ
⊢ arg z = -(π / 2) ↔ z.re = 0 ∧ z.im < 0
by_cases h₀ : z = 0
case neg.mp
z : ℂ
h₀ : ¬z = 0
⊢ arg z = -(π / 2) → z.re = 0 ∧ z.im < 0

case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re = 0 ∧ z.im < 0 → arg z = -(π / 2)
case neg
z : ℂ
h₀ : ¬z = 0
⊢ arg z = -(π / 2) ↔ z.re = 0 ∧ z.im < 0
constructor
no goals
case pos
z : ℂ
h₀ : z = 0
⊢ arg z = -(π / 2) ↔ z.re = 0 ∧ z.im < 0
simp [h₀, lt_irrefl, Real.pi_ne_zero]
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : arg z = -(π / 2)
⊢ z.re = 0 ∧ z.im < 0
case neg.mp
z : ℂ
h₀ : ¬z = 0
⊢ arg z = -(π / 2) → z.re = 0 ∧ z.im < 0
intro h
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : arg z = -(π / 2)
⊢ (↑(↑abs z) * (cos ↑(-(π / 2)) + sin ↑(-(π / 2)) * I)).re = 0 ∧
    (↑(↑abs z) * (cos ↑(-(π / 2)) + sin ↑(-(π / 2)) * I)).im < 0
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : arg z = -(π / 2)
⊢ z.re = 0 ∧ z.im < 0
rw [← abs_mul_cos_add_sin_mul_I z, h]
no goals
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : arg z = -(π / 2)
⊢ (↑(↑abs z) * (cos ↑(-(π / 2)) + sin ↑(-(π / 2)) * I)).re = 0 ∧
    (↑(↑abs z) * (cos ↑(-(π / 2)) + sin ↑(-(π / 2)) * I)).im < 0
simp [h₀]
case neg.mpr.mk
x y : ℝ
h₀ : ¬{ re := x, im := y } = 0
⊢ { re := x, im := y }.re = 0 ∧ { re := x, im := y }.im < 0 → arg { re := x, im := y } = -(π / 2)
case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re = 0 ∧ z.im < 0 → arg z = -(π / 2)
cases' z with x y
case neg.mpr.mk.intro
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : y < 0
⊢ arg { re := 0, im := y } = -(π / 2)
case neg.mpr.mk
x y : ℝ
h₀ : ¬{ re := x, im := y } = 0
⊢ { re := x, im := y }.re = 0 ∧ { re := x, im := y }.im < 0 → arg { re := x, im := y } = -(π / 2)
rintro ⟨rfl : x = 0, hy : y < 0⟩
case neg.mpr.mk.intro
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : y < 0
⊢ arg (↑0 + ↑y * I) = arg (↑(-y) * -I)
case neg.mpr.mk.intro
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : y < 0
⊢ arg { re := 0, im := y } = -(π / 2)
rw [← arg_neg_I, ← arg_real_mul (-I) (neg_pos.2 hy), mk_eq_add_mul_I]
no goals
case neg.mpr.mk.intro
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : y < 0
⊢ arg (↑0 + ↑y * I) = arg (↑(-y) * -I)
simp