case intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.208118
P : Type u_3
P' : Type ?u.208124
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : ↑(lineMap x z) t ∈ s
⊢ WOppSide s x z
R : Type u_1
V : Type u_2
V' : Type ?u.208118
P : Type u_3
P' : Type ?u.208124
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x y z : P
h : Wbtw R x y z
hy : y ∈ s
⊢ WOppSide s x z
rcases h with ⟨t, ⟨ht0, ht1⟩, rfl⟩
case intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.208118
P : Type u_3
P' : Type ?u.208124
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : ↑(lineMap x z) t ∈ s
⊢ SameRay R (x -ᵥ ↑(lineMap x z) t) (↑(lineMap x z) t -ᵥ z)
case intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.208118
P : Type u_3
P' : Type ?u.208124
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : ↑(lineMap x z) t ∈ s
⊢ WOppSide s x z
refine' ⟨_, hy, _, hy, _⟩
case intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.208118
P : Type u_3
P' : Type ?u.208124
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : ↑(lineMap x z) t ∈ s
ht1' : t < 1
⊢ SameRay R (x -ᵥ ↑(lineMap x z) t) (↑(lineMap x z) t -ᵥ z)

case intro.intro.intro.inr
R : Type u_1
V : Type u_2
V' : Type ?u.208118
P : Type u_3
P' : Type ?u.208124
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x z : P
ht0 : 0 ≤ 1
ht1 : 1 ≤ 1
hy : ↑(lineMap x z) 1 ∈ s
⊢ SameRay R (x -ᵥ ↑(lineMap x z) 1) (↑(lineMap x z) 1 -ᵥ z)
case intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.208118
P : Type u_3
P' : Type ?u.208124
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : ↑(lineMap x z) t ∈ s
⊢ SameRay R (x -ᵥ ↑(lineMap x z) t) (↑(lineMap x z) t -ᵥ z)
rcases ht1.lt_or_eq with (ht1' | rfl)
case intro.intro.intro.inr
R : Type u_1
V : Type u_2
V' : Type ?u.208118
P : Type u_3
P' : Type ?u.208124
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x z : P
ht0 : 0 ≤ 1
ht1 : 1 ≤ 1
hy : ↑(lineMap x z) 1 ∈ s
⊢ SameRay R (x -ᵥ ↑(lineMap x z) 1) (↑(lineMap x z) 1 -ᵥ z)

case intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.208118
P : Type u_3
P' : Type ?u.208124
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : ↑(lineMap x z) t ∈ s
ht1' : t < 1
⊢ SameRay R (x -ᵥ ↑(lineMap x z) t) (↑(lineMap x z) t -ᵥ z)
case intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.208118
P : Type u_3
P' : Type ?u.208124
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : ↑(lineMap x z) t ∈ s
ht1' : t < 1
⊢ SameRay R (x -ᵥ ↑(lineMap x z) t) (↑(lineMap x z) t -ᵥ z)

case intro.intro.intro.inr
R : Type u_1
V : Type u_2
V' : Type ?u.208118
P : Type u_3
P' : Type ?u.208124
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x z : P
ht0 : 0 ≤ 1
ht1 : 1 ≤ 1
hy : ↑(lineMap x z) 1 ∈ s
⊢ SameRay R (x -ᵥ ↑(lineMap x z) 1) (↑(lineMap x z) 1 -ᵥ z)
swap
case intro.intro.intro.inl.inl
R : Type u_1
V : Type u_2
V' : Type ?u.208118
P : Type u_3
P' : Type ?u.208124
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : ↑(lineMap x z) t ∈ s
ht1' : t < 1
ht0' : 0 < t
⊢ SameRay R (x -ᵥ ↑(lineMap x z) t) (↑(lineMap x z) t -ᵥ z)

case intro.intro.intro.inl.inr
R : Type u_1
V : Type u_2
V' : Type ?u.208118
P : Type u_3
P' : Type ?u.208124
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x z : P
ht0 : 0 ≤ 0
ht1 : 0 ≤ 1
hy : ↑(lineMap x z) 0 ∈ s
ht1' : 0 < 1
⊢ SameRay R (x -ᵥ ↑(lineMap x z) 0) (↑(lineMap x z) 0 -ᵥ z)
case intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.208118
P : Type u_3
P' : Type ?u.208124
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : ↑(lineMap x z) t ∈ s
ht1' : t < 1
⊢ SameRay R (x -ᵥ ↑(lineMap x z) t) (↑(lineMap x z) t -ᵥ z)
rcases ht0.lt_or_eq with (ht0' | rfl)
case intro.intro.intro.inl.inr
R : Type u_1
V : Type u_2
V' : Type ?u.208118
P : Type u_3
P' : Type ?u.208124
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x z : P
ht0 : 0 ≤ 0
ht1 : 0 ≤ 1
hy : ↑(lineMap x z) 0 ∈ s
ht1' : 0 < 1
⊢ SameRay R (x -ᵥ ↑(lineMap x z) 0) (↑(lineMap x z) 0 -ᵥ z)

case intro.intro.intro.inl.inl
R : Type u_1
V : Type u_2
V' : Type ?u.208118
P : Type u_3
P' : Type ?u.208124
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : ↑(lineMap x z) t ∈ s
ht1' : t < 1
ht0' : 0 < t
⊢ SameRay R (x -ᵥ ↑(lineMap x z) t) (↑(lineMap x z) t -ᵥ z)
case intro.intro.intro.inl.inl
R : Type u_1
V : Type u_2
V' : Type ?u.208118
P : Type u_3
P' : Type ?u.208124
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : ↑(lineMap x z) t ∈ s
ht1' : t < 1
ht0' : 0 < t
⊢ SameRay R (x -ᵥ ↑(lineMap x z) t) (↑(lineMap x z) t -ᵥ z)

case intro.intro.intro.inl.inr
R : Type u_1
V : Type u_2
V' : Type ?u.208118
P : Type u_3
P' : Type ?u.208124
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x z : P
ht0 : 0 ≤ 0
ht1 : 0 ≤ 1
hy : ↑(lineMap x z) 0 ∈ s
ht1' : 0 < 1
⊢ SameRay R (x -ᵥ ↑(lineMap x z) 0) (↑(lineMap x z) 0 -ᵥ z)
swap
case intro.intro.intro.inl.inl
R : Type u_1
V : Type u_2
V' : Type ?u.208118
P : Type u_3
P' : Type ?u.208124
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : ↑(lineMap x z) t ∈ s
ht1' : t < 1
ht0' : 0 < t
⊢ (1 - t) • (x -ᵥ ↑(lineMap x z) t) = t • (↑(lineMap x z) t -ᵥ z)
case intro.intro.intro.inl.inl
R : Type u_1
V : Type u_2
V' : Type ?u.208118
P : Type u_3
P' : Type ?u.208124
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : ↑(lineMap x z) t ∈ s
ht1' : t < 1
ht0' : 0 < t
⊢ SameRay R (x -ᵥ ↑(lineMap x z) t) (↑(lineMap x z) t -ᵥ z)
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.208118
P : Type u_3
P' : Type ?u.208124
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : ↑(lineMap x z) t ∈ s
ht1' : t < 1
ht0' : 0 < t
⊢ (-(1 - t) * t) • (z -ᵥ x) = (t * (t + -1)) • (z -ᵥ x)
case intro.intro.intro.inl.inl
R : Type u_1
V : Type u_2
V' : Type ?u.208118
P : Type u_3
P' : Type ?u.208124
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : ↑(lineMap x z) t ∈ s
ht1' : t < 1
ht0' : 0 < t
⊢ (1 - t) • (x -ᵥ ↑(lineMap x z) t) = t • (↑(lineMap x z) t -ᵥ z)
simp_rw [lineMap_apply, vadd_vsub_assoc, vsub_vadd_eq_vsub_sub, ← neg_vsub_eq_vsub_rev z x,
  vsub_self, zero_sub, ← neg_one_smul R (z -ᵥ x), ← add_smul, smul_neg, ← neg_smul, smul_smul]
no goals
case intro.intro.intro.inl.inl
R : Type u_1
V : Type u_2
V' : Type ?u.208118
P : Type u_3
P' : Type ?u.208124
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : ↑(lineMap x z) t ∈ s
ht1' : t < 1
ht0' : 0 < t
⊢ (-(1 - t) * t) • (z -ᵥ x) = (t * (t + -1)) • (z -ᵥ x)
ring_nf
case intro.intro.intro.inr
R : Type u_1
V : Type u_2
V' : Type ?u.208118
P : Type u_3
P' : Type ?u.208124
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x z : P
ht0 : 0 ≤ 1
ht1 : 1 ≤ 1
hy : ↑(lineMap x z) 1 ∈ s
⊢ SameRay R (x -ᵥ z) (z -ᵥ z)
case intro.intro.intro.inr
R : Type u_1
V : Type u_2
V' : Type ?u.208118
P : Type u_3
P' : Type ?u.208124
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x z : P
ht0 : 0 ≤ 1
ht1 : 1 ≤ 1
hy : ↑(lineMap x z) 1 ∈ s
⊢ SameRay R (x -ᵥ ↑(lineMap x z) 1) (↑(lineMap x z) 1 -ᵥ z)
rw [lineMap_apply_one]
no goals
case intro.intro.intro.inr
R : Type u_1
V : Type u_2
V' : Type ?u.208118
P : Type u_3
P' : Type ?u.208124
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x z : P
ht0 : 0 ≤ 1
ht1 : 1 ≤ 1
hy : ↑(lineMap x z) 1 ∈ s
⊢ SameRay R (x -ᵥ z) (z -ᵥ z)
simp
case intro.intro.intro.inl.inr
R : Type u_1
V : Type u_2
V' : Type ?u.208118
P : Type u_3
P' : Type ?u.208124
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x z : P
ht0 : 0 ≤ 0
ht1 : 0 ≤ 1
hy : ↑(lineMap x z) 0 ∈ s
ht1' : 0 < 1
⊢ SameRay R (x -ᵥ x) (x -ᵥ z)
case intro.intro.intro.inl.inr
R : Type u_1
V : Type u_2
V' : Type ?u.208118
P : Type u_3
P' : Type ?u.208124
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x z : P
ht0 : 0 ≤ 0
ht1 : 0 ≤ 1
hy : ↑(lineMap x z) 0 ∈ s
ht1' : 0 < 1
⊢ SameRay R (x -ᵥ ↑(lineMap x z) 0) (↑(lineMap x z) 0 -ᵥ z)
rw [lineMap_apply_zero]
no goals
case intro.intro.intro.inl.inr
R : Type u_1
V : Type u_2
V' : Type ?u.208118
P : Type u_3
P' : Type ?u.208124
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x z : P
ht0 : 0 ≤ 0
ht1 : 0 ≤ 1
hy : ↑(lineMap x z) 0 ∈ s
ht1' : 0 < 1
⊢ SameRay R (x -ᵥ x) (x -ᵥ z)
simp