case refine'_1
R : Type u_1
V : Type u_2
V' : Type ?u.468028
P : Type u_3
P' : Type ?u.468034
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
h : Wbtw R x y z
⊢ x = y ∨ z ∈ ↑(lineMap x y) '' Set.Ici 1

case refine'_2
R : Type u_1
V : Type u_2
V' : Type ?u.468028
P : Type u_3
P' : Type ?u.468034
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.Ici 1
⊢ Wbtw R x y z
R : Type u_1
V : Type u_2
V' : Type ?u.468028
P : Type u_3
P' : Type ?u.468034
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
⊢ Wbtw R x y z ↔ x = y ∨ z ∈ ↑(lineMap x y) '' Set.Ici 1
refine' ⟨fun h => _, fun h => _⟩
case refine'_1.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.468028
P : Type u_3
P' : Type ?u.468034
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
⊢ x = ↑(lineMap x z) r ∨ z ∈ ↑(lineMap x (↑(lineMap x z) r)) '' Set.Ici 1
case refine'_1
R : Type u_1
V : Type u_2
V' : Type ?u.468028
P : Type u_3
P' : Type ?u.468034
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
h : Wbtw R x y z
⊢ x = y ∨ z ∈ ↑(lineMap x y) '' Set.Ici 1
rcases h with ⟨r, ⟨hr0, hr1⟩, rfl⟩
case refine'_1.intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.468028
P : Type u_3
P' : Type ?u.468034
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hr0' : 0 < r
⊢ x = ↑(lineMap x z) r ∨ z ∈ ↑(lineMap x (↑(lineMap x z) r)) '' Set.Ici 1

case refine'_1.intro.intro.intro.inr
R : Type u_1
V : Type u_2
V' : Type ?u.468028
P : Type u_3
P' : Type ?u.468034
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
hr0 : 0 ≤ 0
hr1 : 0 ≤ 1
⊢ x = ↑(lineMap x z) 0 ∨ z ∈ ↑(lineMap x (↑(lineMap x z) 0)) '' Set.Ici 1
case refine'_1.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.468028
P : Type u_3
P' : Type ?u.468034
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
⊢ x = ↑(lineMap x z) r ∨ z ∈ ↑(lineMap x (↑(lineMap x z) r)) '' Set.Ici 1
rcases hr0.lt_or_eq with (hr0' | rfl)
case refine'_1.intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.468028
P : Type u_3
P' : Type ?u.468034
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hr0' : 0 < r
⊢ x = ↑(lineMap x z) r ∨ ∃ x_1, x_1 ∈ Set.Ici 1 ∧ ↑(lineMap x (↑(lineMap x z) r)) x_1 = z
case refine'_1.intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.468028
P : Type u_3
P' : Type ?u.468034
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hr0' : 0 < r
⊢ x = ↑(lineMap x z) r ∨ z ∈ ↑(lineMap x (↑(lineMap x z) r)) '' Set.Ici 1
rw [Set.mem_image]
case refine'_1.intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.468028
P : Type u_3
P' : Type ?u.468034
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hr0' : 0 < r
⊢ ↑(lineMap x (↑(lineMap x z) r)) r⁻¹ = z
case refine'_1.intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.468028
P : Type u_3
P' : Type ?u.468034
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hr0' : 0 < r
⊢ x = ↑(lineMap x z) r ∨ ∃ x_1, x_1 ∈ Set.Ici 1 ∧ ↑(lineMap x (↑(lineMap x z) r)) x_1 = z
refine' Or.inr ⟨r⁻¹, one_le_inv hr0' hr1, _⟩
case refine'_1.intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.468028
P : Type u_3
P' : Type ?u.468034
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hr0' : 0 < r
⊢ (r⁻¹ * r) • (z -ᵥ x) +ᵥ x = z
case refine'_1.intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.468028
P : Type u_3
P' : Type ?u.468034
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hr0' : 0 < r
⊢ ↑(lineMap x (↑(lineMap x z) r)) r⁻¹ = z
simp only [lineMap_apply, smul_smul, vadd_vsub]
no goals
case refine'_1.intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.468028
P : Type u_3
P' : Type ?u.468034
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hr0' : 0 < r
⊢ (r⁻¹ * r) • (z -ᵥ x) +ᵥ x = z
rw [inv_mul_cancel hr0'.ne', one_smul, vsub_vadd]
no goals
case refine'_1.intro.intro.intro.inr
R : Type u_1
V : Type u_2
V' : Type ?u.468028
P : Type u_3
P' : Type ?u.468034
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
hr0 : 0 ≤ 0
hr1 : 0 ≤ 1
⊢ x = ↑(lineMap x z) 0 ∨ z ∈ ↑(lineMap x (↑(lineMap x z) 0)) '' Set.Ici 1
simp
case refine'_2.inl
R : Type u_1
V : Type u_2
V' : Type ?u.468028
P : Type u_3
P' : Type ?u.468034
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
⊢ Wbtw R x x z

case refine'_2.inr.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.468028
P : Type u_3
P' : Type ?u.468034
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
r : R
hr : r ∈ Set.Ici 1
⊢ Wbtw R x y (↑(lineMap x y) r)
case refine'_2
R : Type u_1
V : Type u_2
V' : Type ?u.468028
P : Type u_3
P' : Type ?u.468034
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.Ici 1
⊢ Wbtw R x y z
rcases h with (rfl | ⟨r, ⟨hr, rfl⟩⟩)
no goals
case refine'_2.inl
R : Type u_1
V : Type u_2
V' : Type ?u.468028
P : Type u_3
P' : Type ?u.468034
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
⊢ Wbtw R x x z
exact wbtw_self_left _ _ _
case refine'_2.inr.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.468028
P : Type u_3
P' : Type ?u.468034
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
r : R
hr : 1 ≤ r
⊢ Wbtw R x y (↑(lineMap x y) r)
case refine'_2.inr.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.468028
P : Type u_3
P' : Type ?u.468034
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
r : R
hr : r ∈ Set.Ici 1
⊢ Wbtw R x y (↑(lineMap x y) r)
rw [Set.mem_Ici] at hr
case refine'_2.inr.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.468028
P : Type u_3
P' : Type ?u.468034
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
r : R
hr : 1 ≤ r
⊢ ↑(lineMap x (↑(lineMap x y) r)) r⁻¹ = y
case refine'_2.inr.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.468028
P : Type u_3
P' : Type ?u.468034
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
r : R
hr : 1 ≤ r
⊢ Wbtw R x y (↑(lineMap x y) r)
refine' ⟨r⁻¹, ⟨inv_nonneg.2 (zero_le_one.trans hr), inv_le_one hr⟩, _⟩
case refine'_2.inr.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.468028
P : Type u_3
P' : Type ?u.468034
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
r : R
hr : 1 ≤ r
⊢ (r⁻¹ * r) • (y -ᵥ x) +ᵥ x = y
case refine'_2.inr.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.468028
P : Type u_3
P' : Type ?u.468034
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
r : R
hr : 1 ≤ r
⊢ ↑(lineMap x (↑(lineMap x y) r)) r⁻¹ = y
simp only [lineMap_apply, smul_smul, vadd_vsub]
no goals
case refine'_2.inr.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.468028
P : Type u_3
P' : Type ?u.468034
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
r : R
hr : 1 ≤ r
⊢ (r⁻¹ * r) • (y -ᵥ x) +ᵥ x = y
rw [inv_mul_cancel (one_pos.trans_le hr).ne', one_smul, vsub_vadd]