apply And.right
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)).re = re 1 ∧ ((1 + I) * ↑x + 2 * (1 - ↑x)).im = im 1
⊢ x = 0
case self
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)).re = re 1 ∧ ((1 + I) * ↑x + 2 * (1 - ↑x)).im = im 1
⊢ ?a ∧ x = 0

case a
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)).re = re 1 ∧ ((1 + I) * ↑x + 2 * (1 - ↑x)).im = im 1
⊢ Prop