rw [Complex.ext_iff] at h
case pos.hyz.left
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + (1 + I) * (1 - ↑t)
cont : Continuous f
x : ℝ
hx : 0 ≤ x ∧ x ≤ 1
h : w * ↑x + (1 + I) * (1 - ↑x) = 1
⊢ w = 1
case pos.hyz.left
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + (1 + I) * (1 - ↑t)
cont : Continuous f
x : ℝ
hx : 0 ≤ x ∧ x ≤ 1
h : (w * ↑x + (1 + I) * (1 - ↑x)).re = re 1 ∧ (w * ↑x + (1 + I) * (1 - ↑x)).im = im 1
⊢ w = 1