simp only [unitInterval, ne_eq, image_subset_iff, preimage_setOf_eq, add_re, mul_re, one_re,
  I_re, add_zero, ofReal_re, one_mul, add_im, one_im, I_im, zero_add, ofReal_im, mul_zero,
  sub_zero, re_ofNat, sub_re, im_ofNat, sub_im, sub_self, f, mem_setOf_eq]
case pos.hxy
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : w.im = 0
f : ℝ → ℂ := fun t => (1 + I) * ↑t + 2 * (1 - ↑t)
cont : Continuous f
⊢ f '' unitInterval ⊆ {z | z ≠ 1 ∧ 0 < z.re}
case pos.hxy
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : w.im = 0
f : ℝ → ℂ := fun t => (1 + I) * ↑t + 2 * (1 - ↑t)
cont : Continuous f
⊢ Icc 0 1 ⊆ {a | ¬(1 + I) * ↑a + 2 * (1 - ↑a) = 1 ∧ 0 < a + 2 * (1 - a)}