case refine'_1
z : ℂ
h : arg z = 0
⊢ 0 ≤ z.re ∧ z.im = 0

case refine'_2
z : ℂ
⊢ 0 ≤ z.re ∧ z.im = 0 → arg z = 0
z : ℂ
⊢ arg z = 0 ↔ 0 ≤ z.re ∧ z.im = 0
refine' ⟨fun h => _, _⟩
case refine'_1
z : ℂ
h : arg z = 0
⊢ 0 ≤ (↑(↑abs z) * (cos ↑0 + sin ↑0 * I)).re ∧ (↑(↑abs z) * (cos ↑0 + sin ↑0 * I)).im = 0
case refine'_1
z : ℂ
h : arg z = 0
⊢ 0 ≤ z.re ∧ z.im = 0
rw [← abs_mul_cos_add_sin_mul_I z, h]
no goals
case refine'_1
z : ℂ
h : arg z = 0
⊢ 0 ≤ (↑(↑abs z) * (cos ↑0 + sin ↑0 * I)).re ∧ (↑(↑abs z) * (cos ↑0 + sin ↑0 * I)).im = 0
simp [abs.nonneg]
case refine'_2.mk
x y : ℝ
⊢ 0 ≤ { re := x, im := y }.re ∧ { re := x, im := y }.im = 0 → arg { re := x, im := y } = 0
case refine'_2
z : ℂ
⊢ 0 ≤ z.re ∧ z.im = 0 → arg z = 0
cases' z with x y
case refine'_2.mk.intro
x : ℝ
h : 0 ≤ { re := x, im := 0 }.re
⊢ arg { re := x, im := 0 } = 0
case refine'_2.mk
x y : ℝ
⊢ 0 ≤ { re := x, im := y }.re ∧ { re := x, im := y }.im = 0 → arg { re := x, im := y } = 0
rintro ⟨h, rfl : y = 0⟩
no goals
case refine'_2.mk.intro
x : ℝ
h : 0 ≤ { re := x, im := 0 }.re
⊢ arg { re := x, im := 0 } = 0
exact arg_ofReal_of_nonneg h