simp only [ne_eq, mem_setOf_eq] at hw
case h.right
w : ℂ
hw : w ∈ {z | z ≠ 1 ∧ 0 < z.re}
⊢ JoinedIn {z | z ≠ 1 ∧ 0 < z.re} 2 w
case h.right
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
⊢ JoinedIn {z | z ≠ 1 ∧ 0 < z.re} 2 w