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

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

case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re = 0 ∧ 0 < z.im → arg z = π / 2
case neg
z : ℂ
h₀ : ¬z = 0
⊢ arg z = π / 2 ↔ z.re = 0 ∧ 0 < z.im
constructor
no goals
case pos
z : ℂ
h₀ : z = 0
⊢ arg z = π / 2 ↔ z.re = 0 ∧ 0 < z.im
simp [h₀, lt_irrefl, Real.pi_div_two_pos.ne]
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : arg z = π / 2
⊢ z.re = 0 ∧ 0 < z.im
case neg.mp
z : ℂ
h₀ : ¬z = 0
⊢ arg z = π / 2 → z.re = 0 ∧ 0 < z.im
intro h
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : arg z = π / 2
⊢ (↑(↑abs z) * (cos ↑(π / 2) + sin ↑(π / 2) * I)).re = 0 ∧ 0 < (↑(↑abs z) * (cos ↑(π / 2) + sin ↑(π / 2) * I)).im
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : arg z = π / 2
⊢ z.re = 0 ∧ 0 < z.im
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 ∧ 0 < (↑(↑abs z) * (cos ↑(π / 2) + sin ↑(π / 2) * I)).im
simp [h₀]
case neg.mpr.mk
x y : ℝ
h₀ : ¬{ re := x, im := y } = 0
⊢ { re := x, im := y }.re = 0 ∧ 0 < { re := x, im := y }.im → arg { re := x, im := y } = π / 2
case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re = 0 ∧ 0 < z.im → arg z = π / 2
cases' z with x y
case neg.mpr.mk.intro
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : 0 < y
⊢ arg { re := 0, im := y } = π / 2
case neg.mpr.mk
x y : ℝ
h₀ : ¬{ re := x, im := y } = 0
⊢ { re := x, im := y }.re = 0 ∧ 0 < { re := x, im := y }.im → arg { re := x, im := y } = π / 2
rintro ⟨rfl : x = 0, hy : 0 < y⟩
no goals
case neg.mpr.mk.intro
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : 0 < y
⊢ arg { re := 0, im := y } = π / 2
rw [← arg_I, ← arg_real_mul I hy, ofReal_mul', I_re, I_im, MulZeroClass.mul_zero, mul_one]