Theorem: hxSegBallInterSeg
Proof state before:
case h.right.right.inl.inl
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
ε : ℝ
hε : 0 < ε
t : ℝ
ht : t ∈ Set.Ioo 0 1
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
hne : x1 = x1 → x2 ≠ x1
hxseg' : x1 ∈ openSegment ℝ x1 x2
htt : x1 + t • (x2 - x1) = x1
h1 : t1 • v + x1 = x1
h : t2 = 0
⊢ False

case h.right.right.inl.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x2 : E
ε : ℝ
hε : 0 < ε
t : ℝ
ht : t ∈ Set.Ioo 0 1
v : E := x2 - x2
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x2 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x2‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x2‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
hne : x2 = x2 → x2 ≠ x2
hxseg' : x2 ∈ openSegment ℝ x2 x2
htt : x2 + t • (x2 - x2) = x2
h1 : t1 • v + x2 = x2
⊢ False

case h.right.right.inr.inl
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
h1 : t1 • v + x = x
hx1x : ¬x1 = x
h : t2 = 0
⊢ False

case h.right.right.inr.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x2 : E
ε : ℝ
hε : 0 < ε
t : ℝ
ht : t ∈ Set.Ioo 0 1
hne : x2 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x2 x2
htt : x2 + t • (x2 - x2) = x
v : E := x2 - x2
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x2 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x2‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x2‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
h1 : t1 • v + x = x
hx1x : ¬x2 = x
⊢ False
Tactic:
exact (ne_of_lt ht2) h.symm
Proof state after:
case h.right.right.inl.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x2 : E
ε : ℝ
hε : 0 < ε
t : ℝ
ht : t ∈ Set.Ioo 0 1
v : E := x2 - x2
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x2 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x2‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x2‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
hne : x2 = x2 → x2 ≠ x2
hxseg' : x2 ∈ openSegment ℝ x2 x2
htt : x2 + t • (x2 - x2) = x2
h1 : t1 • v + x2 = x2
⊢ False

case h.right.right.inr.inl
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
h1 : t1 • v + x = x
hx1x : ¬x1 = x
h : t2 = 0
⊢ False

case h.right.right.inr.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x2 : E
ε : ℝ
hε : 0 < ε
t : ℝ
ht : t ∈ Set.Ioo 0 1
hne : x2 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x2 x2
htt : x2 + t • (x2 - x2) = x
v : E := x2 - x2
t1 : ℝ := -(min t (ε / ‖v‖) / 2)
t2 : ℝ := min (1 - t) (ε / ‖v‖) / 2
hx12 : x2 ≠ x2
ht1pos : 0 < min t (ε / ‖x2 - x2‖)
ht2pos : 0 < min (1 - t) (ε / ‖x2 - x2‖)
ht1 : t1 < 0
ht2 : 0 < t2
ht12 : 0 < t2 - t1
h1 : t1 • v + x = x
hx1x : ¬x2 = x
⊢ False