[GOAL]
x y : ℂ
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ arg x = arg y
[PROOFSTEP]
rcases eq_or_ne x 0 with (rfl | hx)
[GOAL]
case inl
y : ℂ
⊢ SameRay ℝ 0 y ↔ 0 = 0 ∨ y = 0 ∨ arg 0 = arg y
[PROOFSTEP]
simp
[GOAL]
case inr
x y : ℂ
hx : x ≠ 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ arg x = arg y
[PROOFSTEP]
rcases eq_or_ne y 0 with (rfl | hy)
[GOAL]
case inr.inl
x : ℂ
hx : x ≠ 0
⊢ SameRay ℝ x 0 ↔ x = 0 ∨ 0 = 0 ∨ arg x = arg 0
[PROOFSTEP]
simp
[GOAL]
case inr.inr
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ arg x = arg y
[PROOFSTEP]
simp only [hx, hy, false_or_iff, sameRay_iff_norm_smul_eq, arg_eq_arg_iff hx hy]
[GOAL]
case inr.inr
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ ‖x‖ • y = ‖y‖ • x ↔ ↑(↑abs y) / ↑(↑abs x) * x = y
[PROOFSTEP]
field_simp [hx, hy]
[GOAL]
case inr.inr
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑(↑abs x) * y = ↑(↑abs y) * x ↔ ↑(↑abs y) * x = y * ↑(↑abs x)
[PROOFSTEP]
rw [mul_comm, eq_comm]
[GOAL]
x y : ℂ
⊢ SameRay ℝ x y ↔ arg (x / y) = 0
[PROOFSTEP]
rw [← Real.Angle.toReal_zero, ← arg_coe_angle_eq_iff_eq_toReal, sameRay_iff]
[GOAL]
x y : ℂ
⊢ x = 0 ∨ y = 0 ∨ arg x = arg y ↔ ↑(arg (x / y)) = 0
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
x y : ℂ
hx : x = 0
⊢ x = 0 ∨ y = 0 ∨ arg x = arg y ↔ ↑(arg (x / y)) = 0
[PROOFSTEP]
simp [hx]
[GOAL]
case neg
x y : ℂ
hx : ¬x = 0
⊢ x = 0 ∨ y = 0 ∨ arg x = arg y ↔ ↑(arg (x / y)) = 0
[PROOFSTEP]
by_cases hy : y = 0
[GOAL]
case pos
x y : ℂ
hx : ¬x = 0
hy : y = 0
⊢ x = 0 ∨ y = 0 ∨ arg x = arg y ↔ ↑(arg (x / y)) = 0
[PROOFSTEP]
simp [hy]
[GOAL]
case neg
x y : ℂ
hx : ¬x = 0
hy : ¬y = 0
⊢ x = 0 ∨ y = 0 ∨ arg x = arg y ↔ ↑(arg (x / y)) = 0
[PROOFSTEP]
simp [hx, hy, arg_div_coe_angle, sub_eq_zero]
