simpa [this, w_im] using h
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
this : x = 1
⊢ w.re = 1
no goals