case inl
y : ℂ
⊢ SameRay ℝ 0 y ↔ 0 = 0 ∨ y = 0 ∨ arg 0 = arg y

case inr
x y : ℂ
hx : x ≠ 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ arg x = arg y
x y : ℂ
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ arg x = arg y
rcases eq_or_ne x 0 with (rfl | hx)
case inr.inl
x : ℂ
hx : x ≠ 0
⊢ SameRay ℝ x 0 ↔ x = 0 ∨ 0 = 0 ∨ arg x = arg 0

case inr.inr
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ arg x = arg y
case inr
x y : ℂ
hx : x ≠ 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ arg x = arg y
rcases eq_or_ne y 0 with (rfl | hy)
case inr.inr
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ ‖x‖ • y = ‖y‖ • x ↔ ↑(↑abs y) / ↑(↑abs x) * x = y
case inr.inr
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ arg x = arg y
simp only [hx, hy, false_or_iff, sameRay_iff_norm_smul_eq, arg_eq_arg_iff hx hy]
case inr.inr
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑(↑abs x) * y = ↑(↑abs y) * x ↔ ↑(↑abs y) * x = y * ↑(↑abs x)
case inr.inr
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ ‖x‖ • y = ‖y‖ • x ↔ ↑(↑abs y) / ↑(↑abs x) * x = y
field_simp [hx, hy]
no goals
case inr.inr
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑(↑abs x) * y = ↑(↑abs y) * x ↔ ↑(↑abs y) * x = y * ↑(↑abs x)
rw [mul_comm, eq_comm]
no goals
case inl
y : ℂ
⊢ SameRay ℝ 0 y ↔ 0 = 0 ∨ y = 0 ∨ arg 0 = arg y
simp
no goals
case inr.inl
x : ℂ
hx : x ≠ 0
⊢ SameRay ℝ x 0 ↔ x = 0 ∨ 0 = 0 ∨ arg x = arg 0
simp