case refine'_1
R : Type u_1
V : Type u_2
V' : Type ?u.490916
P : Type u_3
P' : Type ?u.490922
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
h : Sbtw R x y z
⊢ z ∈ ↑(lineMap x y) '' Set.Ioi 1

case refine'_2
R : Type u_1
V : Type u_2
V' : Type ?u.490916
P : Type u_3
P' : Type ?u.490922
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
h : x ≠ y ∧ z ∈ ↑(lineMap x y) '' Set.Ioi 1
⊢ Sbtw R x y z
R : Type u_1
V : Type u_2
V' : Type ?u.490916
P : Type u_3
P' : Type ?u.490922
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
⊢ Sbtw R x y z ↔ x ≠ y ∧ z ∈ ↑(lineMap x y) '' Set.Ioi 1
refine' ⟨fun h => ⟨h.left_ne, _⟩, fun h => _⟩
case refine'_1.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.490916
P : Type u_3
P' : Type ?u.490922
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
r : R
hr : r ∈ Set.Ici 1
h : Sbtw R x y (↑(lineMap x y) r)
⊢ ↑(lineMap x y) r ∈ ↑(lineMap x y) '' Set.Ioi 1
case refine'_1
R : Type u_1
V : Type u_2
V' : Type ?u.490916
P : Type u_3
P' : Type ?u.490922
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
h : Sbtw R x y z
⊢ z ∈ ↑(lineMap x y) '' Set.Ioi 1
obtain ⟨r, ⟨hr, rfl⟩⟩ := h.wbtw.right_mem_image_Ici_of_left_ne h.left_ne
case refine'_1.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.490916
P : Type u_3
P' : Type ?u.490922
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
r : R
hr : 1 ≤ r
h : Sbtw R x y (↑(lineMap x y) r)
⊢ ↑(lineMap x y) r ∈ ↑(lineMap x y) '' Set.Ioi 1
case refine'_1.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.490916
P : Type u_3
P' : Type ?u.490922
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
r : R
hr : r ∈ Set.Ici 1
h : Sbtw R x y (↑(lineMap x y) r)
⊢ ↑(lineMap x y) r ∈ ↑(lineMap x y) '' Set.Ioi 1
rw [Set.mem_Ici] at hr
case refine'_1.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.490916
P : Type u_3
P' : Type ?u.490922
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
r : R
hr : 1 ≤ r
h : Sbtw R x y (↑(lineMap x y) r)
hrlt : 1 < r
⊢ ↑(lineMap x y) r ∈ ↑(lineMap x y) '' Set.Ioi 1

case refine'_1.intro.intro.inr
R : Type u_1
V : Type u_2
V' : Type ?u.490916
P : Type u_3
P' : Type ?u.490922
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
hr : 1 ≤ 1
h : Sbtw R x y (↑(lineMap x y) 1)
⊢ ↑(lineMap x y) 1 ∈ ↑(lineMap x y) '' Set.Ioi 1
case refine'_1.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.490916
P : Type u_3
P' : Type ?u.490922
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
r : R
hr : 1 ≤ r
h : Sbtw R x y (↑(lineMap x y) r)
⊢ ↑(lineMap x y) r ∈ ↑(lineMap x y) '' Set.Ioi 1
rcases hr.lt_or_eq with (hrlt | rfl)
no goals
case refine'_1.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.490916
P : Type u_3
P' : Type ?u.490922
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
r : R
hr : 1 ≤ r
h : Sbtw R x y (↑(lineMap x y) r)
hrlt : 1 < r
⊢ ↑(lineMap x y) r ∈ ↑(lineMap x y) '' Set.Ioi 1
exact Set.mem_image_of_mem _ hrlt
case refine'_1.intro.intro.inr.h
R : Type u_1
V : Type u_2
V' : Type ?u.490916
P : Type u_3
P' : Type ?u.490922
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
hr : 1 ≤ 1
h : Sbtw R x y (↑(lineMap x y) 1)
⊢ False
case refine'_1.intro.intro.inr
R : Type u_1
V : Type u_2
V' : Type ?u.490916
P : Type u_3
P' : Type ?u.490922
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
hr : 1 ≤ 1
h : Sbtw R x y (↑(lineMap x y) 1)
⊢ ↑(lineMap x y) 1 ∈ ↑(lineMap x y) '' Set.Ioi 1
exfalso
no goals
case refine'_1.intro.intro.inr.h
R : Type u_1
V : Type u_2
V' : Type ?u.490916
P : Type u_3
P' : Type ?u.490922
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
hr : 1 ≤ 1
h : Sbtw R x y (↑(lineMap x y) 1)
⊢ False
simp at h
case refine'_2.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.490916
P : Type u_3
P' : Type ?u.490922
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
hne : x ≠ y
r : R
hr : r ∈ Set.Ioi 1
⊢ Sbtw R x y (↑(lineMap x y) r)
case refine'_2
R : Type u_1
V : Type u_2
V' : Type ?u.490916
P : Type u_3
P' : Type ?u.490922
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
h : x ≠ y ∧ z ∈ ↑(lineMap x y) '' Set.Ioi 1
⊢ Sbtw R x y z
rcases h with ⟨hne, r, hr, rfl⟩
case refine'_2.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.490916
P : Type u_3
P' : Type ?u.490922
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
hne : x ≠ y
r : R
hr : 1 < r
⊢ Sbtw R x y (↑(lineMap x y) r)
case refine'_2.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.490916
P : Type u_3
P' : Type ?u.490922
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
hne : x ≠ y
r : R
hr : r ∈ Set.Ioi 1
⊢ Sbtw R x y (↑(lineMap x y) r)
rw [Set.mem_Ioi] at hr
case refine'_2.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.490916
P : Type u_3
P' : Type ?u.490922
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
hne : x ≠ y
r : R
hr : 1 < r
⊢ y ≠ ↑(lineMap x y) r
case refine'_2.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.490916
P : Type u_3
P' : Type ?u.490922
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
hne : x ≠ y
r : R
hr : 1 < r
⊢ Sbtw R x y (↑(lineMap x y) r)
refine'
  ⟨wbtw_iff_left_eq_or_right_mem_image_Ici.2
      (Or.inr (Set.mem_image_of_mem _ (Set.mem_of_mem_of_subset hr Set.Ioi_subset_Ici_self))),
    hne.symm, _⟩
case refine'_2.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.490916
P : Type u_3
P' : Type ?u.490922
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
hne : x ≠ y
r : R
hr : 1 < r
⊢ y -ᵥ x - r • (y -ᵥ x) ≠ 0
case refine'_2.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.490916
P : Type u_3
P' : Type ?u.490922
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
hne : x ≠ y
r : R
hr : 1 < r
⊢ y ≠ ↑(lineMap x y) r
rw [lineMap_apply, ← @vsub_ne_zero V, vsub_vadd_eq_vsub_sub]
case refine'_2.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.490916
P : Type u_3
P' : Type ?u.490922
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
hne : x ≠ y
r : R
hr : 1 < r
⊢ 1 • (y -ᵥ x) - r • (y -ᵥ x) ≠ 0
case refine'_2.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.490916
P : Type u_3
P' : Type ?u.490922
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
hne : x ≠ y
r : R
hr : 1 < r
⊢ y -ᵥ x - r • (y -ᵥ x) ≠ 0
nth_rw 1 [← one_smul R (y -ᵥ x)]
case refine'_2.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.490916
P : Type u_3
P' : Type ?u.490922
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
hne : x ≠ y
r : R
hr : 1 < r
⊢ 1 ≠ r ∧ y ≠ x
case refine'_2.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.490916
P : Type u_3
P' : Type ?u.490922
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
hne : x ≠ y
r : R
hr : 1 < r
⊢ 1 • (y -ᵥ x) - r • (y -ᵥ x) ≠ 0
rw [← sub_smul, smul_ne_zero_iff, vsub_ne_zero, sub_ne_zero]
no goals
case refine'_2.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.490916
P : Type u_3
P' : Type ?u.490922
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
hne : x ≠ y
r : R
hr : 1 < r
⊢ 1 ≠ r ∧ y ≠ x
exact ⟨hr.ne, hne.symm⟩