intro h
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
x : ℝ
hx : 0 ≤ x ∧ x ≤ 1
⊢ ¬(1 + I) * ↑x + 2 * (1 - ↑x) = 1
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
x : ℝ
hx : 0 ≤ x ∧ x ≤ 1
h : (1 + I) * ↑x + 2 * (1 - ↑x) = 1
⊢ False