Theorem: isPathConnected_aux (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
⊢ IsPathConnected {z | z ≠ 1 ∧ 0 < z.re}
Tactic:
use (2 : ℂ)
State after:
case h

⊢ 2 ∈ {z | z ≠ 1 ∧ 0 < z.re} ∧ ∀ {y : ℂ}, y ∈ {z | z ≠ 1 ∧ 0 < z.re} → JoinedIn {z | z ≠ 1 ∧ 0 < z.re} 2 y

State before:
case h

⊢ 2 ∈ {z | z ≠ 1 ∧ 0 < z.re} ∧ ∀ {y : ℂ}, y ∈ {z | z ≠ 1 ∧ 0 < z.re} → JoinedIn {z | z ≠ 1 ∧ 0 < z.re} 2 y
Tactic:
constructor
State after:
case h.left

⊢ 2 ∈ {z | z ≠ 1 ∧ 0 < z.re}

case h.right

⊢ ∀ {y : ℂ}, y ∈ {z | z ≠ 1 ∧ 0 < z.re} → JoinedIn {z | z ≠ 1 ∧ 0 < z.re} 2 y

State before:
case h.left

⊢ 2 ∈ {z | z ≠ 1 ∧ 0 < z.re}

case h.right

⊢ ∀ {y : ℂ}, y ∈ {z | z ≠ 1 ∧ 0 < z.re} → JoinedIn {z | z ≠ 1 ∧ 0 < z.re} 2 y
Tactic:
simp
State after:
case h.right

⊢ ∀ {y : ℂ}, y ∈ {z | z ≠ 1 ∧ 0 < z.re} → JoinedIn {z | z ≠ 1 ∧ 0 < z.re} 2 y

State before:
case h.right

⊢ ∀ {y : ℂ}, y ∈ {z | z ≠ 1 ∧ 0 < z.re} → JoinedIn {z | z ≠ 1 ∧ 0 < z.re} 2 y
Tactic:
intro w hw
State after:
case h.right
w : ℂ
hw : w ∈ {z | z ≠ 1 ∧ 0 < z.re}
⊢ JoinedIn {z | z ≠ 1 ∧ 0 < z.re} 2 w

State before:
case h.right
w : ℂ
hw : w ∈ {z | z ≠ 1 ∧ 0 < z.re}
⊢ JoinedIn {z | z ≠ 1 ∧ 0 < z.re} 2 w
Tactic:
simp only [ne_eq, mem_setOf_eq] at hw
State after:
case h.right
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
⊢ JoinedIn {z | z ≠ 1 ∧ 0 < z.re} 2 w

State before:
case h.right
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
⊢ JoinedIn {z | z ≠ 1 ∧ 0 < z.re} 2 w
Tactic:
by_cases w_im : w.im = 0
State after:
case pos
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : w.im = 0
⊢ JoinedIn {z | z ≠ 1 ∧ 0 < z.re} 2 w

case neg
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
⊢ JoinedIn {z | z ≠ 1 ∧ 0 < z.re} 2 w

State before:
case pos
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : w.im = 0
⊢ JoinedIn {z | z ≠ 1 ∧ 0 < z.re} 2 w
Tactic:
apply JoinedIn.trans (y := 1 + I)
State after:
case pos.hxy
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : w.im = 0
⊢ JoinedIn {z | z ≠ 1 ∧ 0 < z.re} 2 (1 + I)

case pos.hyz
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : w.im = 0
⊢ JoinedIn {z | z ≠ 1 ∧ 0 < z.re} (1 + I) w

State before:
case pos.hxy
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : w.im = 0
⊢ JoinedIn {z | z ≠ 1 ∧ 0 < z.re} 2 (1 + I)
Tactic:
let f : ℝ → ℂ := fun t ↦ (1 + I) * t + 2 * (1 - t)
State after:
case pos.hxy
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : w.im = 0
f : ℝ → ℂ := fun t => (1 + I) * ↑t + 2 * (1 - ↑t)
⊢ JoinedIn {z | z ≠ 1 ∧ 0 < z.re} 2 (1 + I)

State before:
case pos.hxy
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : w.im = 0
f : ℝ → ℂ := fun t => (1 + I) * ↑t + 2 * (1 - ↑t)
⊢ JoinedIn {z | z ≠ 1 ∧ 0 < z.re} 2 (1 + I)
Tactic:
have cont : Continuous f := by continuity
State after:
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
⊢ JoinedIn {z | z ≠ 1 ∧ 0 < z.re} 2 (1 + I)

State before:
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
⊢ JoinedIn {z | z ≠ 1 ∧ 0 < z.re} 2 (1 + I)
Tactic:
apply JoinedIn.ofLine cont.continuousOn (by simp [f]) (by simp [f])
State after:
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}

State before:
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}
Tactic:
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]
State after:
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)}

State before:
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)}
Tactic:
intro x hx
State after:
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 : x ∈ Icc 0 1
⊢ x ∈ {a | ¬(1 + I) * ↑a + 2 * (1 - ↑a) = 1 ∧ 0 < a + 2 * (1 - a)}

State before:
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 : x ∈ Icc 0 1
⊢ x ∈ {a | ¬(1 + I) * ↑a + 2 * (1 - ↑a) = 1 ∧ 0 < a + 2 * (1 - a)}
Tactic:
simp only [mem_Icc] at hx
State after:
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
⊢ x ∈ {a | ¬(1 + I) * ↑a + 2 * (1 - ↑a) = 1 ∧ 0 < a + 2 * (1 - a)}

State before:
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
⊢ x ∈ {a | ¬(1 + I) * ↑a + 2 * (1 - ↑a) = 1 ∧ 0 < a + 2 * (1 - a)}
Tactic:
refine ⟨?_, by linarith⟩
State after:
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

State before:
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
Tactic:
intro h
State after:
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

State before:
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
Tactic:
rw [Complex.ext_iff] at h
State after:
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)).re = re 1 ∧ ((1 + I) * ↑x + 2 * (1 - ↑x)).im = im 1
⊢ False

State before:
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)).re = re 1 ∧ ((1 + I) * ↑x + 2 * (1 - ↑x)).im = im 1
⊢ False
Tactic:
simp [(by apply And.right; simpa [w_im] using h : x = 0)] at h
State after:
no goals

State before:
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : w.im = 0
f : ℝ → ℂ := fun t => (1 + I) * ↑t + 2 * (1 - ↑t)
⊢ Continuous f
Tactic:
continuity
State after:
no goals

State before:
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 0 = 2
Tactic:
simp [f]
State after:
no goals

State before:
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 1 = 1 + I
Tactic:
simp [f]
State after:
no goals

State before:
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
⊢ 0 < x + 2 * (1 - x)
Tactic:
linarith
State after:
no goals

State before:
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
Tactic:
apply And.right
State after:
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

State before:
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
Tactic:
simpa [w_im] using h
State after:
no goals

State before:
case pos.hyz
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : w.im = 0
⊢ JoinedIn {z | z ≠ 1 ∧ 0 < z.re} (1 + I) w
Tactic:
let f : ℝ → ℂ := fun t ↦ w * t + (1 + I) * (1 - t)
State after:
case pos.hyz
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + (1 + I) * (1 - ↑t)
⊢ JoinedIn {z | z ≠ 1 ∧ 0 < z.re} (1 + I) w

State before:
case pos.hyz
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + (1 + I) * (1 - ↑t)
⊢ JoinedIn {z | z ≠ 1 ∧ 0 < z.re} (1 + I) w
Tactic:
have cont : Continuous f := by continuity
State after:
case pos.hyz
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + (1 + I) * (1 - ↑t)
cont : Continuous f
⊢ JoinedIn {z | z ≠ 1 ∧ 0 < z.re} (1 + I) w

State before:
case pos.hyz
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + (1 + I) * (1 - ↑t)
cont : Continuous f
⊢ JoinedIn {z | z ≠ 1 ∧ 0 < z.re} (1 + I) w
Tactic:
apply JoinedIn.ofLine cont.continuousOn (by simp [f]) (by simp [f])
State after:
case pos.hyz
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + (1 + I) * (1 - ↑t)
cont : Continuous f
⊢ f '' unitInterval ⊆ {z | z ≠ 1 ∧ 0 < z.re}

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

State before:
case pos.hyz
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + (1 + I) * (1 - ↑t)
cont : Continuous f
⊢ Icc 0 1 ⊆ {a | ¬w * ↑a + (1 + I) * (1 - ↑a) = 1 ∧ 0 < w.re * a + (1 - a)}
Tactic:
intro x hx
State after:
case pos.hyz
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 : x ∈ Icc 0 1
⊢ x ∈ {a | ¬w * ↑a + (1 + I) * (1 - ↑a) = 1 ∧ 0 < w.re * a + (1 - a)}

State before:
case pos.hyz
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 : x ∈ Icc 0 1
⊢ x ∈ {a | ¬w * ↑a + (1 + I) * (1 - ↑a) = 1 ∧ 0 < w.re * a + (1 - a)}
Tactic:
simp only [mem_Icc] at hx
State after:
case pos.hyz
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
⊢ x ∈ {a | ¬w * ↑a + (1 + I) * (1 - ↑a) = 1 ∧ 0 < w.re * a + (1 - a)}

State before:
case pos.hyz
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
⊢ x ∈ {a | ¬w * ↑a + (1 + I) * (1 - ↑a) = 1 ∧ 0 < w.re * a + (1 - a)}
Tactic:
simp only [mem_setOf_eq]
State after:
case pos.hyz
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
⊢ ¬w * ↑x + (1 + I) * (1 - ↑x) = 1 ∧ 0 < w.re * x + (1 - x)

State before:
case pos.hyz
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
⊢ ¬w * ↑x + (1 + I) * (1 - ↑x) = 1 ∧ 0 < w.re * x + (1 - x)
Tactic:
constructor
State after:
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
⊢ ¬w * ↑x + (1 + I) * (1 - ↑x) = 1

case pos.hyz.right
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
⊢ 0 < w.re * x + (1 - x)

State before:
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + (1 + I) * (1 - ↑t)
⊢ Continuous f
Tactic:
continuity
State after:
no goals

State before:
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + (1 + I) * (1 - ↑t)
cont : Continuous f
⊢ f 0 = 1 + I
Tactic:
simp [f]
State after:
no goals

State before:
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + (1 + I) * (1 - ↑t)
cont : Continuous f
⊢ f 1 = w
Tactic:
simp [f]
State after:
no goals

State before:
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
⊢ ¬w * ↑x + (1 + I) * (1 - ↑x) = 1
Tactic:
intro h
State after:
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
⊢ False

State before:
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
⊢ False
Tactic:
refine hw.1 ?_
State after:
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

State before:
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
Tactic:
rw [Complex.ext_iff] at h
State after:
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

State before:
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
Tactic:
have : x = 1 := by linarith [(by apply And.right; simpa [w_im] using h : 1 - x = 0)]
State after:
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
this : x = 1
⊢ w = 1

State before:
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
this : x = 1
⊢ w = 1
Tactic:
rw [Complex.ext_iff, one_re, one_im]
State after:
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
this : x = 1
⊢ w.re = 1 ∧ w.im = 0

State before:
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
this : x = 1
⊢ w.re = 1 ∧ w.im = 0
Tactic:
exact ⟨by simpa [this, w_im] using h, w_im⟩
State after:
no goals

State before:
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
⊢ x = 1
Tactic:
linarith [(by apply And.right; simpa [w_im] using h : 1 - x = 0)]
State after:
no goals

State before:
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
⊢ 1 - x = 0
Tactic:
apply And.right
State after:
case self
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
⊢ ?a ∧ 1 - x = 0

case a
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
⊢ Prop

State before:
case self
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
⊢ ?a ∧ 1 - x = 0

case a
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
⊢ Prop
Tactic:
simpa [w_im] using h
State after:
no goals

State before:
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
Tactic:
simpa [this, w_im] using h
State after:
no goals

State before:
case pos.hyz.right
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
⊢ 0 < w.re * x + (1 - x)
Tactic:
by_cases hxx : x = 0
State after:
case pos
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
hxx : x = 0
⊢ 0 < w.re * x + (1 - x)

case neg
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
hxx : ¬x = 0
⊢ 0 < w.re * x + (1 - x)

State before:
case pos
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
hxx : x = 0
⊢ 0 < w.re * x + (1 - x)
Tactic:
simp only [hxx]
State after:
case pos
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
hxx : x = 0
⊢ 0 < w.re * 0 + (1 - 0)

State before:
case pos
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
hxx : x = 0
⊢ 0 < w.re * 0 + (1 - 0)
Tactic:
linarith
State after:
no goals

State before:
case neg
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
hxx : ¬x = 0
⊢ 0 < w.re * x + (1 - x)
Tactic:
have : 0 < x := lt_of_le_of_ne hx.1 (Ne.symm hxx)
State after:
case neg
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
hxx : ¬x = 0
this : 0 < x
⊢ 0 < w.re * x + (1 - x)

State before:
case neg
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
hxx : ¬x = 0
this : 0 < x
⊢ 0 < w.re * x + (1 - x)
Tactic:
have : 0 ≤ 1 - x := by linarith
State after:
case neg
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
hxx : ¬x = 0
this✝ : 0 < x
this : 0 ≤ 1 - x
⊢ 0 < w.re * x + (1 - x)

State before:
case neg
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
hxx : ¬x = 0
this✝ : 0 < x
this : 0 ≤ 1 - x
⊢ 0 < w.re * x + (1 - x)
Tactic:
have := hw.2
State after:
case neg
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
hxx : ¬x = 0
this✝¹ : 0 < x
this✝ : 0 ≤ 1 - x
this : 0 < w.re
⊢ 0 < w.re * x + (1 - x)

State before:
case neg
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
hxx : ¬x = 0
this✝¹ : 0 < x
this✝ : 0 ≤ 1 - x
this : 0 < w.re
⊢ 0 < w.re * x + (1 - x)
Tactic:
positivity
State after:
no goals

State before:
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
hxx : ¬x = 0
this : 0 < x
⊢ 0 ≤ 1 - x
Tactic:
linarith
State after:
no goals

State before:
case neg
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
⊢ JoinedIn {z | z ≠ 1 ∧ 0 < z.re} 2 w
Tactic:
let f : ℝ → ℂ := fun t ↦ w * t + 2 * (1 - t)
State after:
case neg
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
⊢ JoinedIn {z | z ≠ 1 ∧ 0 < z.re} 2 w

State before:
case neg
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
⊢ JoinedIn {z | z ≠ 1 ∧ 0 < z.re} 2 w
Tactic:
have cont : Continuous f := by continuity
State after:
case neg
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
⊢ JoinedIn {z | z ≠ 1 ∧ 0 < z.re} 2 w

State before:
case neg
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
⊢ JoinedIn {z | z ≠ 1 ∧ 0 < z.re} 2 w
Tactic:
apply JoinedIn.ofLine cont.continuousOn (by simp [f]) (by simp [f])
State after:
case neg
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
⊢ f '' unitInterval ⊆ {z | z ≠ 1 ∧ 0 < z.re}

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

State before:
case neg
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
⊢ Icc 0 1 ⊆ {a | ¬w * ↑a + 2 * (1 - ↑a) = 1 ∧ 0 < w.re * a + 2 * (1 - a)}
Tactic:
intro x hx
State after:
case neg
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
x : ℝ
hx : x ∈ Icc 0 1
⊢ x ∈ {a | ¬w * ↑a + 2 * (1 - ↑a) = 1 ∧ 0 < w.re * a + 2 * (1 - a)}

State before:
case neg
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
x : ℝ
hx : x ∈ Icc 0 1
⊢ x ∈ {a | ¬w * ↑a + 2 * (1 - ↑a) = 1 ∧ 0 < w.re * a + 2 * (1 - a)}
Tactic:
simp only [mem_Icc] at hx
State after:
case neg
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
x : ℝ
hx : 0 ≤ x ∧ x ≤ 1
⊢ x ∈ {a | ¬w * ↑a + 2 * (1 - ↑a) = 1 ∧ 0 < w.re * a + 2 * (1 - a)}

State before:
case neg
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
x : ℝ
hx : 0 ≤ x ∧ x ≤ 1
⊢ x ∈ {a | ¬w * ↑a + 2 * (1 - ↑a) = 1 ∧ 0 < w.re * a + 2 * (1 - a)}
Tactic:
constructor
State after:
case neg.left
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
x : ℝ
hx : 0 ≤ x ∧ x ≤ 1
⊢ ¬w * ↑x + 2 * (1 - ↑x) = 1

case neg.right
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
x : ℝ
hx : 0 ≤ x ∧ x ≤ 1
⊢ 0 < w.re * x + 2 * (1 - x)

State before:
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
⊢ Continuous f
Tactic:
continuity
State after:
no goals

State before:
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
⊢ f 0 = 2
Tactic:
simp [f]
State after:
no goals

State before:
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
⊢ f 1 = w
Tactic:
simp [f]
State after:
no goals

State before:
case neg.left
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
x : ℝ
hx : 0 ≤ x ∧ x ≤ 1
⊢ ¬w * ↑x + 2 * (1 - ↑x) = 1
Tactic:
intro h
State after:
case neg.left
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
x : ℝ
hx : 0 ≤ x ∧ x ≤ 1
h : w * ↑x + 2 * (1 - ↑x) = 1
⊢ False

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

State before:
case neg.left
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
x : ℝ
hx : 0 ≤ x ∧ x ≤ 1
h : (w * ↑x + 2 * (1 - ↑x)).re = re 1 ∧ (w * ↑x + 2 * (1 - ↑x)).im = im 1
⊢ False
Tactic:
simp [(by apply And.right; simpa [w_im] using h : x = 0)] at h
State after:
no goals

State before:
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
x : ℝ
hx : 0 ≤ x ∧ x ≤ 1
h : (w * ↑x + 2 * (1 - ↑x)).re = re 1 ∧ (w * ↑x + 2 * (1 - ↑x)).im = im 1
⊢ x = 0
Tactic:
apply And.right
State after:
case self
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
x : ℝ
hx : 0 ≤ x ∧ x ≤ 1
h : (w * ↑x + 2 * (1 - ↑x)).re = re 1 ∧ (w * ↑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 => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
x : ℝ
hx : 0 ≤ x ∧ x ≤ 1
h : (w * ↑x + 2 * (1 - ↑x)).re = re 1 ∧ (w * ↑x + 2 * (1 - ↑x)).im = im 1
⊢ Prop

State before:
case self
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
x : ℝ
hx : 0 ≤ x ∧ x ≤ 1
h : (w * ↑x + 2 * (1 - ↑x)).re = re 1 ∧ (w * ↑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 => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
x : ℝ
hx : 0 ≤ x ∧ x ≤ 1
h : (w * ↑x + 2 * (1 - ↑x)).re = re 1 ∧ (w * ↑x + 2 * (1 - ↑x)).im = im 1
⊢ Prop
Tactic:
simpa [w_im] using h
State after:
no goals

State before:
case neg.right
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
x : ℝ
hx : 0 ≤ x ∧ x ≤ 1
⊢ 0 < w.re * x + 2 * (1 - x)
Tactic:
by_cases hxx : x = 0
State after:
case pos
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
x : ℝ
hx : 0 ≤ x ∧ x ≤ 1
hxx : x = 0
⊢ 0 < w.re * x + 2 * (1 - x)

case neg
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
x : ℝ
hx : 0 ≤ x ∧ x ≤ 1
hxx : ¬x = 0
⊢ 0 < w.re * x + 2 * (1 - x)

State before:
case pos
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
x : ℝ
hx : 0 ≤ x ∧ x ≤ 1
hxx : x = 0
⊢ 0 < w.re * x + 2 * (1 - x)
Tactic:
simp only [hxx]
State after:
case pos
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
x : ℝ
hx : 0 ≤ x ∧ x ≤ 1
hxx : x = 0
⊢ 0 < w.re * 0 + 2 * (1 - 0)

State before:
case pos
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
x : ℝ
hx : 0 ≤ x ∧ x ≤ 1
hxx : x = 0
⊢ 0 < w.re * 0 + 2 * (1 - 0)
Tactic:
linarith
State after:
no goals

State before:
case neg
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
x : ℝ
hx : 0 ≤ x ∧ x ≤ 1
hxx : ¬x = 0
⊢ 0 < w.re * x + 2 * (1 - x)
Tactic:
have : 0 < x := lt_of_le_of_ne hx.1 (Ne.symm hxx)
State after:
case neg
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
x : ℝ
hx : 0 ≤ x ∧ x ≤ 1
hxx : ¬x = 0
this : 0 < x
⊢ 0 < w.re * x + 2 * (1 - x)

State before:
case neg
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
x : ℝ
hx : 0 ≤ x ∧ x ≤ 1
hxx : ¬x = 0
this : 0 < x
⊢ 0 < w.re * x + 2 * (1 - x)
Tactic:
have : 0 ≤ 1 - x := by linarith
State after:
case neg
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
x : ℝ
hx : 0 ≤ x ∧ x ≤ 1
hxx : ¬x = 0
this✝ : 0 < x
this : 0 ≤ 1 - x
⊢ 0 < w.re * x + 2 * (1 - x)

State before:
case neg
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
x : ℝ
hx : 0 ≤ x ∧ x ≤ 1
hxx : ¬x = 0
this✝ : 0 < x
this : 0 ≤ 1 - x
⊢ 0 < w.re * x + 2 * (1 - x)
Tactic:
have := hw.2
State after:
case neg
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
x : ℝ
hx : 0 ≤ x ∧ x ≤ 1
hxx : ¬x = 0
this✝¹ : 0 < x
this✝ : 0 ≤ 1 - x
this : 0 < w.re
⊢ 0 < w.re * x + 2 * (1 - x)

State before:
case neg
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
x : ℝ
hx : 0 ≤ x ∧ x ≤ 1
hxx : ¬x = 0
this✝¹ : 0 < x
this✝ : 0 ≤ 1 - x
this : 0 < w.re
⊢ 0 < w.re * x + 2 * (1 - x)
Tactic:
positivity
State after:
no goals

State before:
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
w_im : ¬w.im = 0
f : ℝ → ℂ := fun t => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
x : ℝ
hx : 0 ≤ x ∧ x ≤ 1
hxx : ¬x = 0
this : 0 < x
⊢ 0 ≤ 1 - x
Tactic:
linarith
State after:
no goals