case pos
z : ℂ
h₀ : z = 0
⊢ arg z = π ↔ z.re < 0 ∧ z.im = 0

case neg
z : ℂ
h₀ : ¬z = 0
⊢ arg z = π ↔ z.re < 0 ∧ z.im = 0
z : ℂ
⊢ arg z = π ↔ z.re < 0 ∧ z.im = 0
by_cases h₀ : z = 0
case neg
z : ℂ
h₀ : ¬z = 0
⊢ arg z = π ↔ z.re < 0 ∧ z.im = 0
case pos
z : ℂ
h₀ : z = 0
⊢ arg z = π ↔ z.re < 0 ∧ z.im = 0

case neg
z : ℂ
h₀ : ¬z = 0
⊢ arg z = π ↔ z.re < 0 ∧ z.im = 0
simp [h₀, lt_irrefl, Real.pi_ne_zero.symm]
case neg.mp
z : ℂ
h₀ : ¬z = 0
⊢ arg z = π → z.re < 0 ∧ z.im = 0

case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re < 0 ∧ z.im = 0 → arg z = π
case neg
z : ℂ
h₀ : ¬z = 0
⊢ arg z = π ↔ z.re < 0 ∧ z.im = 0
constructor
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : arg z = π
⊢ z.re < 0 ∧ z.im = 0
case neg.mp
z : ℂ
h₀ : ¬z = 0
⊢ arg z = π → z.re < 0 ∧ z.im = 0
intro h
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : arg z = π
⊢ (↑(↑abs z) * (cos ↑π + sin ↑π * I)).re < 0 ∧ (↑(↑abs z) * (cos ↑π + sin ↑π * I)).im = 0
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : arg z = π
⊢ 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 = π
⊢ (↑(↑abs z) * (cos ↑π + sin ↑π * I)).re < 0 ∧ (↑(↑abs z) * (cos ↑π + sin ↑π * 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 } = π
case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re < 0 ∧ z.im = 0 → arg z = π
cases' z with x y
case neg.mpr.mk.intro
x : ℝ
h : x < 0
h₀ : ¬{ re := x, im := 0 } = 0
⊢ arg { re := x, im := 0 } = π
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 } = π
rintro ⟨h : x < 0, rfl : y = 0⟩
case neg.mpr.mk.intro
x : ℝ
h : x < 0
h₀ : ¬{ re := x, im := 0 } = 0
⊢ arg { re := x, im := 0 } = arg (↑(-x) * -1)
case neg.mpr.mk.intro
x : ℝ
h : x < 0
h₀ : ¬{ re := x, im := 0 } = 0
⊢ arg { re := x, im := 0 } = π
rw [← arg_neg_one, ← arg_real_mul (-1) (neg_pos.2 h)]
no goals
case neg.mpr.mk.intro
x : ℝ
h : x < 0
h₀ : ¬{ re := x, im := 0 } = 0
⊢ arg { re := x, im := 0 } = arg (↑(-x) * -1)
simp [← ofReal_def]