internlm/Lean-Github huggingface dataset:
Theorem: hxSegBallInterSeg
Proof state before:
case h.right.left.right.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : ε / 2 < ε
t : ℝ
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
⊢ ‖(min t (ε / ‖x2 - x1‖) / 2) • (x2 - x1)‖ < ε

case h.right.left.right.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : ε / 2 < ε
t : ℝ
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
⊢ ‖(min (1 - t) (ε / ‖x2 - x1‖) / 2) • (x2 - x1)‖ < ε
Tactic:
all_goals {
  rw [norm_smul, Real.norm_eq_abs, abs_of_pos (by linarith), ← min_div_div_right (by linarith), Monotone.map_min fun _ _ => (mul_le_mul_right (norm_sub_pos_iff.mpr (Ne.symm hx12))).mpr] apply min_lt_of_right_lt ; rw [@div_mul_comm _ _ _ 2, mul_comm, div_mul_div_cancel _ (Ne.symm (ne_of_lt (norm_sub_pos_iff.mpr (Ne.symm hx12))))] ; exact hε
}
Proof state after:
no goals
Theorem: hxSegBallInterSeg
Proof state before:
case h.right.left.right.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : ε / 2 < ε
t : ℝ
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
⊢ ‖(min (1 - t) (ε / ‖x2 - x1‖) / 2) • (x2 - x1)‖ < ε
Tactic:
rw [norm_smul, Real.norm_eq_abs, abs_of_pos (by linarith), ← min_div_div_right (by linarith), Monotone.map_min fun _ _ => (mul_le_mul_right (norm_sub_pos_iff.mpr (Ne.symm hx12))).mpr]
Proof state after:
case h.right.left.right.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : ε / 2 < ε
t : ℝ
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
⊢ min ((1 - t) / 2 * ‖x2 - x1‖) (ε / ‖x2 - x1‖ / 2 * ‖x2 - x1‖) < ε
Theorem: hxSegBallInterSeg
Proof state before:
case h.right.left.right.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : ε / 2 < ε
t : ℝ
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
⊢ min ((1 - t) / 2 * ‖x2 - x1‖) (ε / ‖x2 - x1‖ / 2 * ‖x2 - x1‖) < ε
Tactic:
apply min_lt_of_right_lt
Proof state after:
case h.right.left.right.a.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : ε / 2 < ε
t : ℝ
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
⊢ ε / ‖x2 - x1‖ / 2 * ‖x2 - x1‖ < ε
Theorem: hxSegBallInterSeg
Proof state before:
case h.right.left.right.a.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : ε / 2 < ε
t : ℝ
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
⊢ ε / ‖x2 - x1‖ / 2 * ‖x2 - x1‖ < ε
Tactic:
rw [@div_mul_comm _ _ _ 2, mul_comm, div_mul_div_cancel _ (Ne.symm (ne_of_lt (norm_sub_pos_iff.mpr (Ne.symm hx12))))]
Proof state after:
case h.right.left.right.a.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : ε / 2 < ε
t : ℝ
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
⊢ ε / 2 < ε
Theorem: hxSegBallInterSeg
Proof state before:
case h.right.left.right.a.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : ε / 2 < ε
t : ℝ
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
⊢ ε / 2 < ε
Tactic:
exact hε
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ε : ε / 2 < ε
t : ℝ
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 < min (1 - t) (ε / ‖x2 - x1‖) / 2
Tactic:
linarith
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ε : ε / 2 < ε
t : ℝ
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 ≤ 2
Tactic:
linarith
Proof state after:
no goals
Theorem: hxSegBallInterSeg
Proof state before:
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)
Tactic:
push_neg
Proof state after:
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:
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
Tactic:
intro h1
Proof state after:
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
h1 : t1 • v + x = x
⊢ t2 • v + x ≠ x
Theorem: hxSegBallInterSeg
Proof state before:
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
h1 : t1 • v + x = x
⊢ t2 • v + x ≠ x
Tactic:
rcases (em (x1 = x)) with (rfl | hx1x)
<;> norm_num
<;> intro h
<;> rw [sub_eq_zero] at h
<;> rcases h with h | rfl
Proof state after:
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
Theorem: hxSegBallInterSeg
Proof state before:
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:
simp at hne
Proof state after:
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
Theorem: hxSegBallInterSeg
Proof state before:
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.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
Theorem: hxSegBallInterSeg
Proof state before:
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:
simp at hx12
Proof state after:
no goals
Theorem: Hpolytope.I_mem
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
⊢ ∀ (Hi_ : Halfspace E), Hi_ ∈ I H_ x ↔ Hi_ ∈ H_ ∧ x ∈ frontier ↑Hi_
Tactic:
rintro Hi_
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
Hi_ : Halfspace E
⊢ Hi_ ∈ I H_ x ↔ Hi_ ∈ H_ ∧ x ∈ frontier ↑Hi_
Theorem: Hpolytope.I_mem
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
Hi_ : Halfspace E
⊢ Hi_ ∈ I H_ x ↔ Hi_ ∈ H_ ∧ x ∈ frontier ↑Hi_
Tactic:
unfold I
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
Hi_ : Halfspace E
⊢ Hi_ ∈ {Hi_ | Hi_ ∈ H_ ∧ x ∈ frontier ↑Hi_} ↔ Hi_ ∈ H_ ∧ x ∈ frontier ↑Hi_
Theorem: Hpolytope.I_mem
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
Hi_ : Halfspace E
⊢ Hi_ ∈ {Hi_ | Hi_ ∈ H_ ∧ x ∈ frontier ↑Hi_} ↔ Hi_ ∈ H_ ∧ x ∈ frontier ↑Hi_
Tactic:
rw [Set.mem_setOf]
Proof state after:
no goals
Theorem: Hpolytope.I_sub
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
⊢ I H_ x ⊆ H_
Tactic:
unfold Hpolytope.I
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
⊢ {Hi_ | Hi_ ∈ H_ ∧ x ∈ frontier ↑Hi_} ⊆ H_
Theorem: Hpolytope.I_sub
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x : E
⊢ {Hi_ | Hi_ ∈ H_ ∧ x ∈ frontier ↑Hi_} ⊆ H_
Tactic:
simp only [Set.sep_subset]
Proof state after:
no goals
Theorem: ExtremePointsofHpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
⊢ ∀ x ∈ Hpolytope hH_, x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
Tactic:
rintro x hxH
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
⊢ x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
Theorem: ExtremePointsofHpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
⊢ x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
Tactic:
constructor
Proof state after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
⊢ x ∈ Set.extremePoints ℝ (Hpolytope hH_) → ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}

case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
⊢ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x} → x ∈ Set.extremePoints ℝ (Hpolytope hH_)
Theorem: ExtremePointsofHpolytope
Proof state before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
⊢ x ∈ Set.extremePoints ℝ (Hpolytope hH_) → ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
Tactic:
intro hxEx
Proof state after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hxEx : x ∈ Set.extremePoints ℝ (Hpolytope hH_)
⊢ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
Theorem: ExtremePointsofHpolytope
Proof state before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hxEx : x ∈ Set.extremePoints ℝ (Hpolytope hH_)
⊢ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
Tactic:
rw [Set.eq_singleton_iff_unique_mem]
Proof state after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hxEx : x ∈ Set.extremePoints ℝ (Hpolytope hH_)
⊢ x ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) ∧ ∀ x_1 ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x), x_1 = x
Theorem: ExtremePointsofHpolytope
Proof state before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hxEx : x ∈ Set.extremePoints ℝ (Hpolytope hH_)
⊢ x ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) ∧ ∀ x_1 ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x), x_1 = x
Tactic:
refine ⟨ fun HiS ⟨ Hi_, hHi_, h ⟩ => h ▸ hHi_.2, ?_ ⟩
Proof state after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hxEx : x ∈ Set.extremePoints ℝ (Hpolytope hH_)
⊢ ∀ x_1 ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x), x_1 = x
Theorem: ExtremePointsofHpolytope
Proof state before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hxEx : x ∈ Set.extremePoints ℝ (Hpolytope hH_)
⊢ ∀ x_1 ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x), x_1 = x
Tactic:
contrapose! hxEx
Proof state after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hxEx : ∃ x_1 ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x), x_1 ≠ x
⊢ x ∉ Set.extremePoints ℝ (Hpolytope hH_)
Theorem: ExtremePointsofHpolytope
Proof state before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hxEx : ∃ x_1 ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x), x_1 ≠ x
⊢ x ∉ Set.extremePoints ℝ (Hpolytope hH_)
Tactic:
rcases hxEx with ⟨ y, hy, hyx ⟩
Proof state after:
case mp.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
⊢ x ∉ Set.extremePoints ℝ (Hpolytope hH_)
Theorem: ExtremePointsofHpolytope
Proof state before:
case mp.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
⊢ x ∉ Set.extremePoints ℝ (Hpolytope hH_)
Tactic:
have hxyy : x ∈ openSegment ℝ ((2:ℝ) • x - y) y := by
  clear hyx hy hxH hH_
  rw [openSegment_eq_image, Set.mem_image]
  refine ⟨ 1/2, by norm_num, ?_ ⟩
  rw [(by norm_num : (1:ℝ) - 1 / 2 = 1 / 2), smul_sub, sub_add_cancel, smul_smul,
    div_mul_cancel _ (by linarith), one_smul]
  done
Proof state after:
case mp.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
⊢ x ∉ Set.extremePoints ℝ (Hpolytope hH_)