internlm/Lean-Github huggingface dataset:
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
⊢ 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 => 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
Theorem: isPathConnected_aux
Proof 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
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
this : x = 1
⊢ w.re = 1
Tactic:
simpa [this, w_im] using h
Proof state after:
no goals
Theorem: isPathConnected_aux
Proof 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
Proof 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)
Theorem: isPathConnected_aux
Proof 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]
Proof 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)
Theorem: isPathConnected_aux
Proof 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
Proof state after:
no goals
Theorem: isPathConnected_aux
Proof 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)
Proof 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)
Theorem: isPathConnected_aux
Proof 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
Proof 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)
Theorem: isPathConnected_aux
Proof 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
Proof 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)
Theorem: isPathConnected_aux
Proof 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
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
hxx : ¬x = 0
this : 0 < x
⊢ 0 ≤ 1 - x
Tactic:
linarith
Proof state after:
no goals
Theorem: isPathConnected_aux
Proof 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)
Proof 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
Theorem: isPathConnected_aux
Proof 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
Proof 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
Theorem: isPathConnected_aux
Proof 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])
Proof 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}
Theorem: isPathConnected_aux
Proof 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]
Proof 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)}
Theorem: isPathConnected_aux
Proof 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
Proof 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)}
Theorem: isPathConnected_aux
Proof 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
Proof 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)}
Theorem: isPathConnected_aux
Proof 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
Proof 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)
Theorem: isPathConnected_aux
Proof 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
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 + 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 => w * ↑t + 2 * (1 - ↑t)
cont : Continuous f
⊢ f 1 = w
Tactic:
simp [f]
Proof state after:
no goals
Theorem: isPathConnected_aux
Proof 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
Proof 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
Theorem: isPathConnected_aux
Proof 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
Proof 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
Theorem: isPathConnected_aux
Proof 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
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 + 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
Proof 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
Theorem: isPathConnected_aux
Proof 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
Proof state after:
no goals
Theorem: isPathConnected_aux
Proof 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
Proof 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)
Theorem: isPathConnected_aux
Proof 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]
Proof 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)
Theorem: isPathConnected_aux
Proof 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
Proof state after:
no goals
Theorem: isPathConnected_aux
Proof 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)
Proof 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)
Theorem: isPathConnected_aux
Proof 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
Proof 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)
Theorem: isPathConnected_aux
Proof 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
Proof 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)
Theorem: isPathConnected_aux
Proof 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
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 + 2 * (1 - ↑t)
cont : Continuous f
x : ℝ
hx : 0 ≤ x ∧ x ≤ 1
hxx : ¬x = 0
this : 0 < x
⊢ 0 ≤ 1 - x
Tactic:
linarith
Proof state after:
no goals
Theorem: Zeta0EqZeta
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ ζ₀ N s = ζ s
Tactic:
let f := riemannZeta
Proof state after:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
⊢ ζ₀ N s = ζ s
Theorem: Zeta0EqZeta
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
⊢ ζ₀ N s = ζ s
Tactic:
let g := ζ₀ N
Proof state after:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
⊢ ζ₀ N s = ζ s
Theorem: Zeta0EqZeta
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
⊢ ζ₀ N s = ζ s
Tactic:
let U := {z : ℂ | z ≠ 1 ∧ 0 < z.re}
Proof state after:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
⊢ ζ₀ N s = ζ s
Theorem: Zeta0EqZeta
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
⊢ ζ₀ N s = ζ s
Tactic:
have f_an : AnalyticOn ℂ f U := by
  apply (HolomophicOn_riemannZeta.analyticOn isOpen_ne).mono
  simp only [ne_eq, setOf_subset_setOf, and_imp, U]
  exact fun a ha _ ↦ ha
Proof state after:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
⊢ ζ₀ N s = ζ s
Theorem: Zeta0EqZeta
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
⊢ ζ₀ N s = ζ s
Tactic:
have g_an : AnalyticOn ℂ g U := (HolomorphicOn_riemannZeta0 N_pos).analyticOn isOpen_aux
Proof state after:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
⊢ ζ₀ N s = ζ s
Theorem: Zeta0EqZeta
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
⊢ ζ₀ N s = ζ s
Tactic:
have preconU : IsPreconnected U := by
  apply IsConnected.isPreconnected
  apply (IsOpen.isConnected_iff_isPathConnected isOpen_aux).mp isPathConnected_aux
Proof state after:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
preconU : IsPreconnected U
⊢ ζ₀ N s = ζ s
Theorem: Zeta0EqZeta
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
preconU : IsPreconnected U
⊢ ζ₀ N s = ζ s
Tactic:
have h2 : (2 : ℂ) ∈ U := by simp [U]
Proof state after:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
preconU : IsPreconnected U
h2 : 2 ∈ U
⊢ ζ₀ N s = ζ s
Theorem: Zeta0EqZeta
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
preconU : IsPreconnected U
h2 : 2 ∈ U
⊢ ζ₀ N s = ζ s
Tactic:
have s_mem : s ∈ U := by simp [U, reS_pos, s_ne_one]
Proof state after:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
preconU : IsPreconnected U
h2 : 2 ∈ U
s_mem : s ∈ U
⊢ ζ₀ N s = ζ s
Theorem: Zeta0EqZeta
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
preconU : IsPreconnected U
h2 : 2 ∈ U
s_mem : s ∈ U
⊢ ζ₀ N s = ζ s
Tactic:
convert (AnalyticOn.eqOn_of_preconnected_of_eventuallyEq f_an g_an preconU h2 ?_ s_mem).symm
Proof state after:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
preconU : IsPreconnected U
h2 : 2 ∈ U
s_mem : s ∈ U
⊢ f =ᶠ[𝓝 2] g
Theorem: Zeta0EqZeta
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
preconU : IsPreconnected U
h2 : 2 ∈ U
s_mem : s ∈ U
⊢ f =ᶠ[𝓝 2] g
Tactic:
have u_mem : {z : ℂ | 1 < z.re} ∈ 𝓝 (2 : ℂ) := by
  apply mem_nhds_iff.mpr
  use {z : ℂ | 1 < z.re}
  simp only [setOf_subset_setOf, imp_self, forall_const, mem_setOf_eq, re_ofNat,
    Nat.one_lt_ofNat, and_true, true_and]
  exact isOpen_lt (by continuity) (by continuity)
Proof state after:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
preconU : IsPreconnected U
h2 : 2 ∈ U
s_mem : s ∈ U
u_mem : {z | 1 < z.re} ∈ 𝓝 2
⊢ f =ᶠ[𝓝 2] g
Theorem: Zeta0EqZeta
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
preconU : IsPreconnected U
h2 : 2 ∈ U
s_mem : s ∈ U
u_mem : {z | 1 < z.re} ∈ 𝓝 2
⊢ f =ᶠ[𝓝 2] g
Tactic:
filter_upwards [u_mem]
Proof state after:
case h
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
preconU : IsPreconnected U
h2 : 2 ∈ U
s_mem : s ∈ U
u_mem : {z | 1 < z.re} ∈ 𝓝 2
⊢ ∀ (a : ℂ), 1 < a.re → f a = g a
Theorem: Zeta0EqZeta
Proof state before:
case h
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
preconU : IsPreconnected U
h2 : 2 ∈ U
s_mem : s ∈ U
u_mem : {z | 1 < z.re} ∈ 𝓝 2
⊢ ∀ (a : ℂ), 1 < a.re → f a = g a
Tactic:
intro z hz
Proof state after:
case h
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
preconU : IsPreconnected U
h2 : 2 ∈ U
s_mem : s ∈ U
u_mem : {z | 1 < z.re} ∈ 𝓝 2
z : ℂ
hz : 1 < z.re
⊢ f z = g z
Theorem: Zeta0EqZeta
Proof state before:
case h
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
preconU : IsPreconnected U
h2 : 2 ∈ U
s_mem : s ∈ U
u_mem : {z | 1 < z.re} ∈ 𝓝 2
z : ℂ
hz : 1 < z.re
⊢ f z = g z
Tactic:
simp only [f,g, zeta_eq_tsum_one_div_nat_cpow hz, riemannZeta0_apply]
Proof state after:
case h
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
preconU : IsPreconnected U
h2 : 2 ∈ U
s_mem : s ∈ U
u_mem : {z | 1 < z.re} ∈ 𝓝 2
z : ℂ
hz : 1 < z.re
⊢ ∑' (n : ℕ), 1 / ↑n ^ z =
    ∑ n ∈ Finset.range (N + 1), 1 / ↑n ^ z +
      (-↑N ^ (1 - z) / (1 - z) + -↑N ^ (-z) / 2 + z * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(z + 1)))
Theorem: Zeta0EqZeta
Proof state before:
case h
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
preconU : IsPreconnected U
h2 : 2 ∈ U
s_mem : s ∈ U
u_mem : {z | 1 < z.re} ∈ 𝓝 2
z : ℂ
hz : 1 < z.re
⊢ ∑' (n : ℕ), 1 / ↑n ^ z =
    ∑ n ∈ Finset.range (N + 1), 1 / ↑n ^ z +
      (-↑N ^ (1 - z) / (1 - z) + -↑N ^ (-z) / 2 + z * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(z + 1)))
Tactic:
nth_rewrite 2 [neg_div]
Proof state after:
case h
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
preconU : IsPreconnected U
h2 : 2 ∈ U
s_mem : s ∈ U
u_mem : {z | 1 < z.re} ∈ 𝓝 2
z : ℂ
hz : 1 < z.re
⊢ ∑' (n : ℕ), 1 / ↑n ^ z =
    ∑ n ∈ Finset.range (N + 1), 1 / ↑n ^ z +
      (-↑N ^ (1 - z) / (1 - z) + -(↑N ^ (-z) / 2) + z * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(z + 1)))