internlm/Lean-Github huggingface dataset:
Theorem: hxSegBallInterSeg
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
⊢ x ∈ openSegment ℝ (t1 • v + x) (t2 • v + x) ∧
    segment ℝ (t1 • v + x) (t2 • v + x) ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(t1 • v + x = x ∧ t2 • v + x = x)
Tactic:
have ht2pos: 0 < min (1 - t) (ε / ‖x2 - x1‖) :=
  lt_min (by linarith [ht.2]) <| div_pos hε <| norm_sub_pos_iff.mpr (Ne.symm hx12)
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
⊢ x ∈ openSegment ℝ (t1 • v + x) (t2 • v + x) ∧
    segment ℝ (t1 • v + x) (t2 • v + x) ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(t1 • v + x = x ∧ t2 • v + x = x)
Theorem: hxSegBallInterSeg
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
⊢ x ∈ openSegment ℝ (t1 • v + x) (t2 • v + x) ∧
    segment ℝ (t1 • v + x) (t2 • v + x) ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(t1 • v + x = x ∧ t2 • v + x = x)
Tactic:
have ht1 : t1 < 0 := neg_lt_zero.mpr <| half_pos ht1pos
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
⊢ x ∈ openSegment ℝ (t1 • v + x) (t2 • v + x) ∧
    segment ℝ (t1 • v + x) (t2 • v + x) ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(t1 • v + x = x ∧ t2 • v + x = x)
Theorem: hxSegBallInterSeg
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
⊢ x ∈ openSegment ℝ (t1 • v + x) (t2 • v + x) ∧
    segment ℝ (t1 • v + x) (t2 • v + x) ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(t1 • v + x = x ∧ t2 • v + x = x)
Tactic:
have ht2 : 0 < t2 := half_pos ht2pos
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
⊢ x ∈ openSegment ℝ (t1 • v + x) (t2 • v + x) ∧
    segment ℝ (t1 • v + x) (t2 • v + x) ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(t1 • v + x = x ∧ t2 • v + x = x)
Theorem: hxSegBallInterSeg
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
⊢ x ∈ openSegment ℝ (t1 • v + x) (t2 • v + x) ∧
    segment ℝ (t1 • v + x) (t2 • v + x) ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(t1 • v + x = x ∧ t2 • v + x = x)
Tactic:
have ht12 : 0 < t2 - t1 := sub_pos.mpr <| lt_trans ht1 ht2
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ x ∈ openSegment ℝ (t1 • v + x) (t2 • v + x) ∧
    segment ℝ (t1 • v + x) (t2 • v + x) ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(t1 • v + x = x ∧ t2 • v + x = x)
Theorem: hxSegBallInterSeg
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ x ∈ openSegment ℝ (t1 • v + x) (t2 • v + x) ∧
    segment ℝ (t1 • v + x) (t2 • v + x) ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(t1 • v + x = x ∧ t2 • v + x = x)
Tactic:
constructor
Proof state after:
case h.left
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ x ∈ openSegment ℝ (t1 • v + x) (t2 • v + x)

case h.right
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ segment ℝ (t1 • v + x) (t2 • v + x) ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(t1 • v + x = x ∧ t2 • v + x = x)
Theorem: hxSegBallInterSeg
Proof state before:
case h.right
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ segment ℝ (t1 • v + x) (t2 • v + x) ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(t1 • v + x = x ∧ t2 • v + x = x)
Tactic:
constructor
Proof state after:
case h.right.left
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ segment ℝ (t1 • v + x) (t2 • v + x) ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε

case h.right.right
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ ¬(t1 • v + x = x ∧ t2 • v + x = x)
Theorem: hxSegBallInterSeg
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
⊢ x1 ≠ x2
Tactic:
intro h
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
h : x1 = x2
⊢ False
Theorem: hxSegBallInterSeg
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
h : x1 = x2
⊢ False
Tactic:
rw [←h, openSegment_same] at hxseg'
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ {x1}
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
h : x1 = x2
⊢ False
Theorem: hxSegBallInterSeg
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ {x1}
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
h : x1 = x2
⊢ False
Tactic:
exact (h.symm ▸ hne) (Set.eq_of_mem_singleton hxseg').symm (Set.eq_of_mem_singleton hxseg').symm
Proof state after:
no goals
Theorem: hxSegBallInterSeg
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
⊢ 0 < 1 - t
Tactic:
linarith [ht.2]
Proof state after:
no goals
Theorem: hxSegBallInterSeg
Proof state before:
case h.left
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ x ∈ openSegment ℝ (t1 • v + x) (t2 • v + x)
Tactic:
rw [openSegment_eq_image', Set.mem_image]
Proof state after:
case h.left
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ ∃ x_1 ∈ Set.Ioo 0 1, t1 • v + x + x_1 • (t2 • v + x - (t1 • v + x)) = x
Theorem: hxSegBallInterSeg
Proof state before:
case h.left
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ ∃ x_1 ∈ Set.Ioo 0 1, t1 • v + x + x_1 • (t2 • v + x - (t1 • v + x)) = x
Tactic:
refine ⟨ (-t1/(t2 - t1)), ?_, ?_ ⟩
Proof state after:
case h.left.refine_1
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ -t1 / (t2 - t1) ∈ Set.Ioo 0 1

case h.left.refine_2
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ t1 • v + x + (-t1 / (t2 - t1)) • (t2 • v + x - (t1 • v + x)) = x
Theorem: hxSegBallInterSeg
Proof state before:
case h.left.refine_1
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ -t1 / (t2 - t1) ∈ Set.Ioo 0 1
Tactic:
constructor
Proof state after:
case h.left.refine_1.left
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ 0 < -t1 / (t2 - t1)

case h.left.refine_1.right
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ -t1 / (t2 - t1) < 1
Theorem: hxSegBallInterSeg
Proof state before:
case h.left.refine_1.left
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ 0 < -t1 / (t2 - t1)
Tactic:
rw [div_pos_iff]
Proof state after:
case h.left.refine_1.left
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ 0 < -t1 ∧ 0 < t2 - t1 ∨ -t1 < 0 ∧ t2 - t1 < 0
Theorem: hxSegBallInterSeg
Proof state before:
case h.left.refine_1.left
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ 0 < -t1 ∧ 0 < t2 - t1 ∨ -t1 < 0 ∧ t2 - t1 < 0
Tactic:
left
Proof state after:
case h.left.refine_1.left.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ 0 < -t1 ∧ 0 < t2 - t1
Theorem: hxSegBallInterSeg
Proof state before:
case h.left.refine_1.left.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ 0 < -t1 ∧ 0 < t2 - t1
Tactic:
exact ⟨ neg_pos_of_neg ht1, ht12 ⟩
Proof state after:
no goals
Theorem: hxSegBallInterSeg
Proof state before:
case h.left.refine_1.right
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ -t1 / (t2 - t1) < 1
Tactic:
rw [div_lt_one_iff]
Proof state after:
case h.left.refine_1.right
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ 0 < t2 - t1 ∧ -t1 < t2 - t1 ∨ t2 - t1 = 0 ∨ t2 - t1 < 0 ∧ t2 - t1 < -t1
Theorem: hxSegBallInterSeg
Proof state before:
case h.left.refine_1.right
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ 0 < t2 - t1 ∧ -t1 < t2 - t1 ∨ t2 - t1 = 0 ∨ t2 - t1 < 0 ∧ t2 - t1 < -t1
Tactic:
left
Proof state after:
case h.left.refine_1.right.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ 0 < t2 - t1 ∧ -t1 < t2 - t1
Theorem: hxSegBallInterSeg
Proof state before:
case h.left.refine_1.right.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ 0 < t2 - t1 ∧ -t1 < t2 - t1
Tactic:
exact ⟨ ht12, neg_lt_sub_iff_lt_add.mpr <| lt_add_of_le_of_pos (le_refl _) ht2 ⟩
Proof state after:
no goals
Theorem: hxSegBallInterSeg
Proof state before:
case h.left.refine_2
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ t1 • v + x + (-t1 / (t2 - t1)) • (t2 • v + x - (t1 • v + x)) = x
Tactic:
rw [smul_sub (-t1 / (t2 - t1)), smul_add (-t1 / (t2 - t1)), smul_smul, smul_add, smul_smul,
  add_sub_add_comm, sub_self, add_zero, ←sub_smul, ←mul_sub, div_mul_cancel _ ?_, add_comm,
  ← add_assoc, ← add_smul, neg_add_self, zero_smul, zero_add]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ t2 - t1 ≠ 0
Theorem: hxSegBallInterSeg
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
t : ℝ
ht : t ∈ Set.Ioo 0 1
htt : x1 + t • (x2 - x1) = x
v : E := x2 - x1
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x1 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x1‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x1‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
⊢ t2 - t1 ≠ 0
Tactic:
exact Ne.symm (ne_of_lt ht12)
Proof state after:
no goals