apply JoinedIn.trans (y := 1 + I)
case pos
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : w.im = 0
⊢ JoinedIn {z | z ≠ 1 ∧ 0 < z.re} 2 w
case pos.hxy
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : w.im = 0
⊢ JoinedIn {z | z ≠ 1 ∧ 0 < z.re} 2 (1 + I)

case pos.hyz
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : w.im = 0
⊢ JoinedIn {z | z ≠ 1 ∧ 0 < z.re} (1 + I) w