case intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.351137
P : Type u_3
P' : Type ?u.351143
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
⊢ SameRay R (↑(lineMap x z) t -ᵥ x) (z -ᵥ ↑(lineMap x z) t)
R : Type u_1
V : Type u_2
V' : Type ?u.351137
P : Type u_3
P' : Type ?u.351143
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
h : Wbtw R x y z
⊢ SameRay R (y -ᵥ x) (z -ᵥ y)
rcases h with ⟨t, ⟨ht0, ht1⟩, rfl⟩
case intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.351137
P : Type u_3
P' : Type ?u.351143
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
⊢ SameRay R (t • (z -ᵥ x) +ᵥ x -ᵥ x) (z -ᵥ (t • (z -ᵥ x) +ᵥ x))
case intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.351137
P : Type u_3
P' : Type ?u.351143
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
⊢ SameRay R (↑(lineMap x z) t -ᵥ x) (z -ᵥ ↑(lineMap x z) t)
simp_rw [lineMap_apply]
case intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.351137
P : Type u_3
P' : Type ?u.351143
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
ht0' : 0 < t
⊢ SameRay R (t • (z -ᵥ x) +ᵥ x -ᵥ x) (z -ᵥ (t • (z -ᵥ x) +ᵥ x))

case intro.intro.intro.inr
R : Type u_1
V : Type u_2
V' : Type ?u.351137
P : Type u_3
P' : Type ?u.351143
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
ht0 : 0 ≤ 0
ht1 : 0 ≤ 1
⊢ SameRay R (0 • (z -ᵥ x) +ᵥ x -ᵥ x) (z -ᵥ (0 • (z -ᵥ x) +ᵥ x))
case intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.351137
P : Type u_3
P' : Type ?u.351143
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
⊢ SameRay R (t • (z -ᵥ x) +ᵥ x -ᵥ x) (z -ᵥ (t • (z -ᵥ x) +ᵥ x))
rcases ht0.lt_or_eq with (ht0' | rfl)
case intro.intro.intro.inr
R : Type u_1
V : Type u_2
V' : Type ?u.351137
P : Type u_3
P' : Type ?u.351143
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
ht0 : 0 ≤ 0
ht1 : 0 ≤ 1
⊢ SameRay R (0 • (z -ᵥ x) +ᵥ x -ᵥ x) (z -ᵥ (0 • (z -ᵥ x) +ᵥ x))

case intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.351137
P : Type u_3
P' : Type ?u.351143
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
ht0' : 0 < t
⊢ SameRay R (t • (z -ᵥ x) +ᵥ x -ᵥ x) (z -ᵥ (t • (z -ᵥ x) +ᵥ x))
case intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.351137
P : Type u_3
P' : Type ?u.351143
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
ht0' : 0 < t
⊢ SameRay R (t • (z -ᵥ x) +ᵥ x -ᵥ x) (z -ᵥ (t • (z -ᵥ x) +ᵥ x))

case intro.intro.intro.inr
R : Type u_1
V : Type u_2
V' : Type ?u.351137
P : Type u_3
P' : Type ?u.351143
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
ht0 : 0 ≤ 0
ht1 : 0 ≤ 1
⊢ SameRay R (0 • (z -ᵥ x) +ᵥ x -ᵥ x) (z -ᵥ (0 • (z -ᵥ x) +ᵥ x))
swap
case intro.intro.intro.inl.inl
R : Type u_1
V : Type u_2
V' : Type ?u.351137
P : Type u_3
P' : Type ?u.351143
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
ht0' : 0 < t
ht1' : t < 1
⊢ SameRay R (t • (z -ᵥ x) +ᵥ x -ᵥ x) (z -ᵥ (t • (z -ᵥ x) +ᵥ x))

case intro.intro.intro.inl.inr
R : Type u_1
V : Type u_2
V' : Type ?u.351137
P : Type u_3
P' : Type ?u.351143
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
ht0 : 0 ≤ 1
ht1 : 1 ≤ 1
ht0' : 0 < 1
⊢ SameRay R (1 • (z -ᵥ x) +ᵥ x -ᵥ x) (z -ᵥ (1 • (z -ᵥ x) +ᵥ x))
case intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.351137
P : Type u_3
P' : Type ?u.351143
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
ht0' : 0 < t
⊢ SameRay R (t • (z -ᵥ x) +ᵥ x -ᵥ x) (z -ᵥ (t • (z -ᵥ x) +ᵥ x))
rcases ht1.lt_or_eq with (ht1' | rfl)
case intro.intro.intro.inl.inr
R : Type u_1
V : Type u_2
V' : Type ?u.351137
P : Type u_3
P' : Type ?u.351143
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
ht0 : 0 ≤ 1
ht1 : 1 ≤ 1
ht0' : 0 < 1
⊢ SameRay R (1 • (z -ᵥ x) +ᵥ x -ᵥ x) (z -ᵥ (1 • (z -ᵥ x) +ᵥ x))

case intro.intro.intro.inl.inl
R : Type u_1
V : Type u_2
V' : Type ?u.351137
P : Type u_3
P' : Type ?u.351143
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
ht0' : 0 < t
ht1' : t < 1
⊢ SameRay R (t • (z -ᵥ x) +ᵥ x -ᵥ x) (z -ᵥ (t • (z -ᵥ x) +ᵥ x))
case intro.intro.intro.inl.inl
R : Type u_1
V : Type u_2
V' : Type ?u.351137
P : Type u_3
P' : Type ?u.351143
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
ht0' : 0 < t
ht1' : t < 1
⊢ SameRay R (t • (z -ᵥ x) +ᵥ x -ᵥ x) (z -ᵥ (t • (z -ᵥ x) +ᵥ x))

case intro.intro.intro.inl.inr
R : Type u_1
V : Type u_2
V' : Type ?u.351137
P : Type u_3
P' : Type ?u.351143
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
ht0 : 0 ≤ 1
ht1 : 1 ≤ 1
ht0' : 0 < 1
⊢ SameRay R (1 • (z -ᵥ x) +ᵥ x -ᵥ x) (z -ᵥ (1 • (z -ᵥ x) +ᵥ x))
swap
case intro.intro.intro.inl.inl
R : Type u_1
V : Type u_2
V' : Type ?u.351137
P : Type u_3
P' : Type ?u.351143
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
ht0' : 0 < t
ht1' : t < 1
⊢ (1 - t) • (t • (z -ᵥ x) +ᵥ x -ᵥ x) = t • (z -ᵥ (t • (z -ᵥ x) +ᵥ x))
case intro.intro.intro.inl.inl
R : Type u_1
V : Type u_2
V' : Type ?u.351137
P : Type u_3
P' : Type ?u.351143
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
ht0' : 0 < t
ht1' : t < 1
⊢ SameRay R (t • (z -ᵥ x) +ᵥ x -ᵥ x) (z -ᵥ (t • (z -ᵥ x) +ᵥ x))
refine' Or.inr (Or.inr ⟨1 - t, t, sub_pos.2 ht1', ht0', _⟩)
case intro.intro.intro.inl.inl
R : Type u_1
V : Type u_2
V' : Type ?u.351137
P : Type u_3
P' : Type ?u.351143
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
ht0' : 0 < t
ht1' : t < 1
⊢ ((1 - t) * t) • (z -ᵥ x) = (t - t * t) • (z -ᵥ x)
case intro.intro.intro.inl.inl
R : Type u_1
V : Type u_2
V' : Type ?u.351137
P : Type u_3
P' : Type ?u.351143
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
ht0' : 0 < t
ht1' : t < 1
⊢ (1 - t) • (t • (z -ᵥ x) +ᵥ x -ᵥ x) = t • (z -ᵥ (t • (z -ᵥ x) +ᵥ x))
simp [vsub_vadd_eq_vsub_sub, smul_sub, smul_smul, ← sub_smul]
no goals
case intro.intro.intro.inl.inl
R : Type u_1
V : Type u_2
V' : Type ?u.351137
P : Type u_3
P' : Type ?u.351143
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
ht0' : 0 < t
ht1' : t < 1
⊢ ((1 - t) * t) • (z -ᵥ x) = (t - t * t) • (z -ᵥ x)
ring_nf
no goals
case intro.intro.intro.inr
R : Type u_1
V : Type u_2
V' : Type ?u.351137
P : Type u_3
P' : Type ?u.351143
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
ht0 : 0 ≤ 0
ht1 : 0 ≤ 1
⊢ SameRay R (0 • (z -ᵥ x) +ᵥ x -ᵥ x) (z -ᵥ (0 • (z -ᵥ x) +ᵥ x))
simp
no goals
case intro.intro.intro.inl.inr
R : Type u_1
V : Type u_2
V' : Type ?u.351137
P : Type u_3
P' : Type ?u.351143
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
ht0 : 0 ≤ 1
ht1 : 1 ≤ 1
ht0' : 0 < 1
⊢ SameRay R (1 • (z -ᵥ x) +ᵥ x -ᵥ x) (z -ᵥ (1 • (z -ᵥ x) +ᵥ x))
simp