internlm/Lean-Github huggingface dataset:
Theorem: HasDerivAtZeta0
Proof state before:
case h.e'_7
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
n : ℕ
a✝ : n ∈ Finset.range (N + 1)
⊢ -((↑n ^ s)⁻¹ * ↑(↑n).log) = -(↑n ^ (-s) * (↑n).log)
Tactic:
simp [cpow_neg]
Proof state after:
no goals
Theorem: HasDerivAtZeta0
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun x => -↑N ^ (1 - x) / (1 - x)) (-↑N ^ (1 - s) / (1 - s) ^ 2 + ↑(↑N).log * ↑N ^ (1 - s) / (1 - s)) s
Tactic:
convert HasDerivAt.comp (h₂ := fun z ↦ -(N : ℂ) ^ z / z) (h := fun z ↦ 1 - z) (h' := -1)
  (h₂' := ((N : ℂ) ^ (1 - s) / (1 - s) ^ 2 - Real.log (N : ℝ) * (N : ℂ) ^ (1 - s) / (1 - s)))
  (x := s) ?_ ?_ using 1
Proof state after:
case h.e'_7
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ -↑N ^ (1 - s) / (1 - s) ^ 2 + ↑(↑N).log * ↑N ^ (1 - s) / (1 - s) =
    (↑N ^ (1 - s) / (1 - s) ^ 2 - ↑(↑N).log * ↑N ^ (1 - s) / (1 - s)) * -1

case convert_1
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun z => -↑N ^ z / z) (↑N ^ (1 - s) / (1 - s) ^ 2 - ↑(↑N).log * ↑N ^ (1 - s) / (1 - s))
    ((fun z => 1 - z) s)

case convert_2
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun z => 1 - z) (-1) s
Theorem: HasDerivAtZeta0
Proof state before:
case h.e'_7
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ -↑N ^ (1 - s) / (1 - s) ^ 2 + ↑(↑N).log * ↑N ^ (1 - s) / (1 - s) =
    (↑N ^ (1 - s) / (1 - s) ^ 2 - ↑(↑N).log * ↑N ^ (1 - s) / (1 - s)) * -1

case convert_1
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun z => -↑N ^ z / z) (↑N ^ (1 - s) / (1 - s) ^ 2 - ↑(↑N).log * ↑N ^ (1 - s) / (1 - s))
    ((fun z => 1 - z) s)

case convert_2
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun z => 1 - z) (-1) s
Tactic:
ring_nf
Proof state after:
case convert_1
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun z => -↑N ^ z / z) (↑N ^ (1 - s) / (1 - s) ^ 2 - ↑(↑N).log * ↑N ^ (1 - s) / (1 - s))
    ((fun z => 1 - z) s)

case convert_2
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun z => 1 - z) (-1) s
Theorem: HasDerivAtZeta0
Proof state before:
case convert_1
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun z => -↑N ^ z / z) (↑N ^ (1 - s) / (1 - s) ^ 2 - ↑(↑N).log * ↑N ^ (1 - s) / (1 - s))
    ((fun z => 1 - z) s)
Tactic:
exact HasDerivAt_cpow_over_var N (by rw [sub_ne_zero]; exact s_ne_one.symm)
Proof state after:
no goals
Theorem: HasDerivAtZeta0
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ 1 - s ≠ 0
Tactic:
rw [sub_ne_zero]
Proof state after:
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ 1 ≠ s
Theorem: HasDerivAtZeta0
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ 1 ≠ s
Tactic:
exact s_ne_one.symm
Proof state after:
no goals
Theorem: HasDerivAtZeta0
Proof state before:
case convert_2
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun z => 1 - z) (-1) s
Tactic:
convert hasDerivAt_const s _ |>.sub (hasDerivAt_id _) using 1
Proof state after:
case h.e'_7
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ -1 = 0 - 1
Theorem: HasDerivAtZeta0
Proof state before:
case h.e'_7
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ -1 = 0 - 1
Tactic:
simp
Proof state after:
no goals
Theorem: HasDerivAtZeta0
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun x => -↑N ^ (-x) / 2) (↑(↑N).log * ↑N ^ (-s) / 2) s
Tactic:
convert HasDerivAt_neg_cpow_over2 Npos s using 1
Proof state after:
case h.e'_7
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ ↑(↑N).log * ↑N ^ (-s) / 2 = -(-↑(↑N).log * ↑N ^ (-s)) / 2
Theorem: HasDerivAtZeta0
Proof state before:
case h.e'_7
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ ↑(↑N).log * ↑N ^ (-s) / 2 = -(-↑(↑N).log * ↑N ^ (-s)) / 2
Tactic:
simp only [natCast_log, neg_mul, neg_neg]
Proof state after:
no goals
Theorem: HasDerivAtZeta0
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun x => x * ∫ (x_1 : ℝ) in Ioi ↑N, (↑⌊x_1⌋ + 1 / 2 - ↑x_1) / ↑x_1 ^ (x + 1))
    ((1 * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1)) +
      s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑x.log)
    s
Tactic:
simp_rw [div_cpow_eq_cpow_neg, neg_add, ← sub_eq_add_neg]
Proof state after:
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun x => x * ∫ (x_1 : ℝ) in Ioi ↑N, (↑⌊x_1⌋ + 1 / 2 - ↑x_1) * ↑x_1 ^ (-x - 1))
    ((1 * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1)) +
      s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑x.log)
    s
Theorem: HasDerivAtZeta0
Proof state before:
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun x => x * ∫ (x_1 : ℝ) in Ioi ↑N, (↑⌊x_1⌋ + 1 / 2 - ↑x_1) * ↑x_1 ^ (-x - 1))
    ((1 * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1)) +
      s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑x.log)
    s
Tactic:
convert hasDerivAt_id s |>.mul <| hasDerivAt_Zeta0Integral Npos reS_pos using 1
Proof state after:
no goals
Theorem: HolomophicOn_riemannZeta
Proof state before:
⊢ HolomorphicOn ζ {s | s ≠ 1}
Tactic:
intro z hz
Proof state after:
z : ℂ
hz : z ∈ {s | s ≠ 1}
⊢ DifferentiableWithinAt ℂ ζ {s | s ≠ 1} z
Theorem: HolomophicOn_riemannZeta
Proof state before:
z : ℂ
hz : z ∈ {s | s ≠ 1}
⊢ DifferentiableWithinAt ℂ ζ {s | s ≠ 1} z
Tactic:
simp only [mem_setOf_eq] at hz
Proof state after:
z : ℂ
hz : z ≠ 1
⊢ DifferentiableWithinAt ℂ ζ {s | s ≠ 1} z
Theorem: HolomophicOn_riemannZeta
Proof state before:
z : ℂ
hz : z ≠ 1
⊢ DifferentiableWithinAt ℂ ζ {s | s ≠ 1} z
Tactic:
exact (differentiableAt_riemannZeta hz).differentiableWithinAt
Proof state after:
no goals
Theorem: isPathConnected_aux
Proof state before:
⊢ IsPathConnected {z | z ≠ 1 ∧ 0 < z.re}
Tactic:
use (2 : ℂ)
Proof 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
Theorem: isPathConnected_aux
Proof 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
Proof 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
Theorem: isPathConnected_aux
Proof 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
Proof state after:
case h.right

⊢ ∀ {y : ℂ}, y ∈ {z | z ≠ 1 ∧ 0 < z.re} → JoinedIn {z | z ≠ 1 ∧ 0 < z.re} 2 y
Theorem: isPathConnected_aux
Proof 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
Proof state after:
case h.right
w : ℂ
hw : w ∈ {z | z ≠ 1 ∧ 0 < z.re}
⊢ JoinedIn {z | z ≠ 1 ∧ 0 < z.re} 2 w
Theorem: isPathConnected_aux
Proof 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
Proof state after:
case h.right
w : ℂ
hw : ¬w = 1 ∧ 0 < w.re
⊢ JoinedIn {z | z ≠ 1 ∧ 0 < z.re} 2 w
Theorem: isPathConnected_aux
Proof 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
Proof 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
Theorem: isPathConnected_aux
Proof 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)
Proof 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
Theorem: isPathConnected_aux
Proof 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)
Proof 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)
Theorem: isPathConnected_aux
Proof 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
Proof 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)
Theorem: isPathConnected_aux
Proof 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])
Proof 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}
Theorem: isPathConnected_aux
Proof 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]
Proof 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)}
Theorem: isPathConnected_aux
Proof 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
Proof 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)}
Theorem: isPathConnected_aux
Proof 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
Proof 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)}
Theorem: isPathConnected_aux
Proof 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⟩
Proof 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
Theorem: isPathConnected_aux
Proof 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
Proof 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
Theorem: isPathConnected_aux
Proof 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
Proof 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
Theorem: isPathConnected_aux
Proof 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
Proof state after:
no goals
Theorem: isPathConnected_aux
Proof 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
Proof state after:
no goals
Theorem: isPathConnected_aux
Proof 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]
Proof state after:
no goals
Theorem: isPathConnected_aux
Proof 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]
Proof state after:
no goals
Theorem: isPathConnected_aux
Proof 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
Proof state after:
no goals
Theorem: isPathConnected_aux
Proof 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
Proof 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
Theorem: isPathConnected_aux
Proof 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
Proof state after:
no goals
Theorem: isPathConnected_aux
Proof 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)
Proof 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
Theorem: isPathConnected_aux
Proof 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
Proof 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
Theorem: isPathConnected_aux
Proof 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])
Proof 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}
Theorem: isPathConnected_aux
Proof 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]
Proof 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)}
Theorem: isPathConnected_aux
Proof 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
Proof 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)}
Theorem: isPathConnected_aux
Proof 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
Proof 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)}
Theorem: isPathConnected_aux
Proof 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]
Proof 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)
Theorem: isPathConnected_aux
Proof 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
Proof 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)
Theorem: isPathConnected_aux
Proof 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
Proof state after:
no goals
Theorem: isPathConnected_aux
Proof 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]
Proof state after:
no goals
Theorem: isPathConnected_aux
Proof 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]
Proof state after:
no goals
Theorem: isPathConnected_aux
Proof 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
Proof 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
Theorem: isPathConnected_aux
Proof 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 ?_
Proof 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
Theorem: isPathConnected_aux
Proof 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
Proof 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
Theorem: isPathConnected_aux
Proof 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)]
Proof 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
Theorem: isPathConnected_aux
Proof 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]
Proof 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
Theorem: isPathConnected_aux
Proof 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⟩
Proof state after:
no goals
Theorem: isPathConnected_aux
Proof 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)]
Proof state after:
no goals