Theorem: hxSegBallInterSeg (src/MainTheorem.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
⊢ ∀ (x1 x2 : E) (ε : ℝ),
    x ∈ openSegment ℝ x1 x2 ∧ ¬(x1 = x ∧ x2 = x) →
      0 < ε →
        ∃ x1' x2',
          x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)
Tactic:
rintro x1 x2 ε ⟨ hxseg, hne ⟩ hε
State after:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hxseg : x ∈ openSegment ℝ x1 x2
hne : ¬(x1 = x ∧ x2 = x)
hε : 0 < ε
⊢ ∃ x1' x2',
    x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)

State before:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hxseg : x ∈ openSegment ℝ x1 x2
hne : ¬(x1 = x ∧ x2 = x)
hε : 0 < ε
⊢ ∃ x1' x2',
    x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)
Tactic:
push_neg at hne
State after:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hxseg : x ∈ openSegment ℝ x1 x2
hε : 0 < ε
hne : x1 = x → x2 ≠ x
⊢ ∃ x1' x2',
    x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)

State before:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hxseg : x ∈ openSegment ℝ x1 x2
hε : 0 < ε
hne : x1 = x → x2 ≠ x
⊢ ∃ x1' x2',
    x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)
Tactic:
have hxseg' := hxseg
State after:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hxseg : x ∈ openSegment ℝ x1 x2
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
⊢ ∃ x1' x2',
    x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)

State before:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hxseg : x ∈ openSegment ℝ x1 x2
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
⊢ ∃ x1' x2',
    x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)
Tactic:
rw [openSegment_eq_image', Set.mem_image] at hxseg
State after:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hxseg : ∃ x_1 ∈ Set.Ioo 0 1, x1 + x_1 • (x2 - x1) = x
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
⊢ ∃ x1' x2',
    x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)

State before:
case intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hxseg : ∃ x_1 ∈ Set.Ioo 0 1, x1 + x_1 • (x2 - x1) = x
hε : 0 < ε
hne : x1 = x → x2 ≠ x
hxseg' : x ∈ openSegment ℝ x1 x2
⊢ ∃ x1' x2',
    x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)
Tactic:
rcases hxseg with ⟨ t, ht, htt ⟩
State after:
case intro.intro.intro
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
⊢ ∃ x1' x2',
    x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)

State before:
case intro.intro.intro
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
⊢ ∃ x1' x2',
    x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)
Tactic:
let v := x2 - x1
State after:
case intro.intro.intro
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
⊢ ∃ x1' x2',
    x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)

State before:
case intro.intro.intro
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
⊢ ∃ x1' x2',
    x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)
Tactic:
let t1 := (-(min t (ε/norm v)/2))
State after:
case intro.intro.intro
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)
⊢ ∃ x1' x2',
    x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)

State before:
case intro.intro.intro
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)
⊢ ∃ x1' x2',
    x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)
Tactic:
let t2 := ((min (1-t) (ε/norm v))/2)
State after:
case intro.intro.intro
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',
    x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)

State before:
case intro.intro.intro
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',
    x ∈ openSegment ℝ x1' x2' ∧ segment ℝ x1' x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(x1' = x ∧ x2' = x)
Tactic:
use t1 • v + x
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
⊢ ∃ x2',
    x ∈ openSegment ℝ (t1 • v + x) x2' ∧
      segment ℝ (t1 • v + x) x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(t1 • v + x = x ∧ x2' = x)

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
⊢ ∃ x2',
    x ∈ openSegment ℝ (t1 • v + x) x2' ∧
      segment ℝ (t1 • v + x) x2' ⊆ openSegment ℝ x1 x2 ∩ Metric.ball x ε ∧ ¬(t1 • v + x = x ∧ x2' = x)
Tactic:
use t2 • v + x
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
⊢ 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)

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
⊢ 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 hx12 : x1 ≠ x2 := by
  intro h
  rw [←h, openSegment_same] at hxseg'
  exact (h.symm ▸ hne) (Set.eq_of_mem_singleton hxseg').symm (Set.eq_of_mem_singleton hxseg').symm
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
⊢ 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)

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
⊢ 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 ht1pos: 0 < min t (ε / ‖x2 - x1‖) := lt_min ht.1 <| div_pos hε <| norm_sub_pos_iff.mpr (Ne.symm hx12)
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‖)
⊢ 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)

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)
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)

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
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)

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
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)

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
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)

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
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)

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
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)

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
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

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'
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

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
State after:
no goals

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]
State after:
no goals

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]
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

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)), ?_, ?_ ⟩
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

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
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

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]
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

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
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

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 ⟩
State after:
no goals

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]
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

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
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

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 ⟩
State after:
no goals

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]
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

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)
State after:
no goals

State before:
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 ε
Tactic:
rw [Set.subset_inter_iff]
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 ∧ segment ℝ (t1 • v + x) (t2 • v + x) ⊆ Metric.ball x ε

State before:
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 ∧ segment ℝ (t1 • v + x) (t2 • v + x) ⊆ Metric.ball x ε
Tactic:
constructor
State after:
case h.right.left.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

case h.right.left.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) ⊆ Metric.ball x ε

State before:
case h.right.left.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
Tactic:
have := @convex_openSegment ℝ _ _ _ _ x1 x2
State after:
case h.right.left.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
this : Convex ℝ (openSegment ℝ x1 x2)
⊢ segment ℝ (t1 • v + x) (t2 • v + x) ⊆ openSegment ℝ x1 x2

State before:
case h.right.left.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
this : Convex ℝ (openSegment ℝ x1 x2)
⊢ segment ℝ (t1 • v + x) (t2 • v + x) ⊆ openSegment ℝ x1 x2
Tactic:
rw [convex_iff_segment_subset] at this
State after:
case h.right.left.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
this : ∀ ⦃x : E⦄, x ∈ openSegment ℝ x1 x2 → ∀ ⦃y : E⦄, y ∈ openSegment ℝ x1 x2 → segment ℝ x y ⊆ openSegment ℝ x1 x2
⊢ segment ℝ (t1 • v + x) (t2 • v + x) ⊆ openSegment ℝ x1 x2

State before:
case h.right.left.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
this : ∀ ⦃x : E⦄, x ∈ openSegment ℝ x1 x2 → ∀ ⦃y : E⦄, y ∈ openSegment ℝ x1 x2 → segment ℝ x y ⊆ openSegment ℝ x1 x2
⊢ segment ℝ (t1 • v + x) (t2 • v + x) ⊆ openSegment ℝ x1 x2
Tactic:
apply this <;> clear this <;> rw [←htt] <;>
rw [@add_comm _ _ x1, ←add_assoc, ← add_smul, @add_comm _ _ _ t, openSegment_eq_image']
State after:
case h.right.left.left.a
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
⊢ (t + t1) • v + x1 ∈ (fun θ => x1 + θ • (x2 - x1)) '' Set.Ioo 0 1

case h.right.left.left.a
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
⊢ (t + t2) • v + x1 ∈ (fun θ => x1 + θ • (x2 - x1)) '' Set.Ioo 0 1

State before:
case h.right.left.left.a
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
⊢ (t + t1) • v + x1 ∈ (fun θ => x1 + θ • (x2 - x1)) '' Set.Ioo 0 1
Tactic:
exact ⟨ t + t1,
  ⟨ lt_of_le_of_lt' (by linarith [min_le_left t (ε/norm v)] : t -t/2 ≤ t -(min t (ε /norm v)/2))
    (by linarith [ht.1]), lt_trans (add_lt_of_neg_right t ht1) ht.2 ⟩,
  by unfold_let v; simp only [ge_iff_le]; rw [add_comm, @add_comm _ _ t t1, sub_eq_neg_add] ⟩
State after:
no goals

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
⊢ t - t / 2 ≤ t - min t (ε / ‖v‖) / 2
Tactic:
linarith [min_le_left t (ε/norm v)]
State after:
no goals

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
⊢ 0 < t - t / 2
Tactic:
linarith [ht.1]
State after:
no goals

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
⊢ (fun θ => x1 + θ • (x2 - x1)) (t + t1) = (t + t1) • v + x1
Tactic:
unfold_let v
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
⊢ (fun θ => x1 + θ • (x2 - x1)) (t + t1) = (t + t1) • (x2 - x1) + x1

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
⊢ (fun θ => x1 + θ • (x2 - x1)) (t + t1) = (t + t1) • (x2 - x1) + x1
Tactic:
simp only [ge_iff_le]
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
⊢ x1 + (t + t1) • (x2 - x1) = (t + t1) • (x2 - x1) + x1

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
⊢ x1 + (t + t1) • (x2 - x1) = (t + t1) • (x2 - x1) + x1
Tactic:
rw [add_comm, @add_comm _ _ t t1, sub_eq_neg_add]
State after:
no goals

State before:
case h.right.left.left.a
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
⊢ (t + t2) • v + x1 ∈ (fun θ => x1 + θ • (x2 - x1)) '' Set.Ioo 0 1
Tactic:
refine ⟨ t + t2,
  ⟨ lt_trans ht.1 (by linarith [ht2pos] : t < t + (min (1 - t) (ε / ‖x2 - x1‖) / 2)), ?_ ⟩,
  by simp only [ge_iff_le] ;rw [add_comm] ⟩
State after:
case h.right.left.left.a
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
⊢ t + t2 < 1

State before:
case h.right.left.left.a
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
⊢ t + t2 < 1
Tactic:
exact lt_of_lt_of_le' (by linarith [ht.2]) (by linarith [min_le_left (1 - t) ((ε / ‖x2 - x1‖))]
  : t + min (1 - t) (ε / ‖x2 - x1‖) / 2 ≤ t + ((1 - t) / 2))
State after:
no goals

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
⊢ t < t + min (1 - t) (ε / ‖x2 - x1‖) / 2
Tactic:
linarith [ht2pos]
State after:
no goals

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
⊢ (fun θ => x1 + θ • (x2 - x1)) (t + t2) = (t + t2) • v + x1
Tactic:
simp only [ge_iff_le]
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
⊢ x1 + (t + t2) • (x2 - x1) = (t + t2) • v + x1

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
⊢ x1 + (t + t2) • (x2 - x1) = (t + t2) • v + x1
Tactic:
rw [add_comm]
State after:
no goals

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
⊢ t + (1 - t) / 2 < 1
Tactic:
linarith [ht.2]
State after:
no goals

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
⊢ t + min (1 - t) (ε / ‖x2 - x1‖) / 2 ≤ t + (1 - t) / 2
Tactic:
linarith [min_le_left (1 - t) ((ε / ‖x2 - x1‖))]
State after:
no goals

State before:
case h.right.left.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) ⊆ Metric.ball x ε
Tactic:
clear ht hxseg' hne
State after:
case h.right.left.right
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
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
⊢ segment ℝ (t1 • v + x) (t2 • v + x) ⊆ Metric.ball x ε

State before:
case h.right.left.right
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
ε : ℝ
hε : 0 < ε
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
⊢ segment ℝ (t1 • v + x) (t2 • v + x) ⊆ Metric.ball x ε
Tactic:
rw [← half_lt_self_iff] at hε
State after:
case h.right.left.right
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
⊢ segment ℝ (t1 • v + x) (t2 • v + x) ⊆ Metric.ball x ε

State before:
case h.right.left.right
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
⊢ segment ℝ (t1 • v + x) (t2 • v + x) ⊆ Metric.ball x ε
Tactic:
apply (convex_iff_segment_subset.mp <| convex_ball x ε ) <;> rw [Metric.mem_ball] <;> norm_num <;> unfold_let
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 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)‖ < ε

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:
simp
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 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)‖ < ε

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ε
}
State after:
no goals

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]
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‖) < ε

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
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‖ < ε

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))))]
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 < ε

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ε
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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

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
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

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
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

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
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

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
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

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
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

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
State after:
no goals