case mp
R : Type u_1
V : Type u_2
V' : Type ?u.233854
P : Type u_3
P' : Type ?u.233860
inst✝⁶ : LinearOrderedField 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 p₁ : P
h : p₁ ∈ s
⊢ WSameSide s x y → x ∈ s ∨ ∃ p₂, p₂ ∈ s ∧ SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

case mpr
R : Type u_1
V : Type u_2
V' : Type ?u.233854
P : Type u_3
P' : Type ?u.233860
inst✝⁶ : LinearOrderedField 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 p₁ : P
h : p₁ ∈ s
⊢ (x ∈ s ∨ ∃ p₂, p₂ ∈ s ∧ SameRay R (x -ᵥ p₁) (y -ᵥ p₂)) → WSameSide s x y
R : Type u_1
V : Type u_2
V' : Type ?u.233854
P : Type u_3
P' : Type ?u.233860
inst✝⁶ : LinearOrderedField 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 p₁ : P
h : p₁ ∈ s
⊢ WSameSide s x y ↔ x ∈ s ∨ ∃ p₂, p₂ ∈ s ∧ SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
constructor
case mp.intro.intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.233854
P : Type u_3
P' : Type ?u.233860
inst✝⁶ : LinearOrderedField 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 p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : x -ᵥ p₁' = 0
⊢ x ∈ s ∨ ∃ p₂, p₂ ∈ s ∧ SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

case mp.intro.intro.intro.intro.inr.inl
R : Type u_1
V : Type u_2
V' : Type ?u.233854
P : Type u_3
P' : Type ?u.233860
inst✝⁶ : LinearOrderedField 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 p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : y -ᵥ p₂' = 0
⊢ x ∈ s ∨ ∃ p₂, p₂ ∈ s ∧ SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

case mp.intro.intro.intro.intro.inr.inr.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.233854
P : Type u_3
P' : Type ?u.233860
inst✝⁶ : LinearOrderedField 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 p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
hr : r₁ • (x -ᵥ p₁') = r₂ • (y -ᵥ p₂')
⊢ x ∈ s ∨ ∃ p₂, p₂ ∈ s ∧ SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
case mp
R : Type u_1
V : Type u_2
V' : Type ?u.233854
P : Type u_3
P' : Type ?u.233860
inst✝⁶ : LinearOrderedField 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 p₁ : P
h : p₁ ∈ s
⊢ WSameSide s x y → x ∈ s ∨ ∃ p₂, p₂ ∈ s ∧ SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
rintro ⟨p₁', hp₁', p₂', hp₂', h0 | h0 | ⟨r₁, r₂, hr₁, hr₂, hr⟩⟩
case mp.intro.intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.233854
P : Type u_3
P' : Type ?u.233860
inst✝⁶ : LinearOrderedField 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 p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : x = p₁'
⊢ x ∈ s ∨ ∃ p₂, p₂ ∈ s ∧ SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
case mp.intro.intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.233854
P : Type u_3
P' : Type ?u.233860
inst✝⁶ : LinearOrderedField 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 p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : x -ᵥ p₁' = 0
⊢ x ∈ s ∨ ∃ p₂, p₂ ∈ s ∧ SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
rw [vsub_eq_zero_iff_eq] at h0
case mp.intro.intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.233854
P : Type u_3
P' : Type ?u.233860
inst✝⁶ : LinearOrderedField 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 p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : x = p₁'
⊢ p₁' ∈ s ∨ ∃ p₂, p₂ ∈ s ∧ SameRay R (p₁' -ᵥ p₁) (y -ᵥ p₂)
case mp.intro.intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.233854
P : Type u_3
P' : Type ?u.233860
inst✝⁶ : LinearOrderedField 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 p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : x = p₁'
⊢ x ∈ s ∨ ∃ p₂, p₂ ∈ s ∧ SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
rw [h0]
no goals
case mp.intro.intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.233854
P : Type u_3
P' : Type ?u.233860
inst✝⁶ : LinearOrderedField 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 p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : x = p₁'
⊢ p₁' ∈ s ∨ ∃ p₂, p₂ ∈ s ∧ SameRay R (p₁' -ᵥ p₁) (y -ᵥ p₂)
exact Or.inl hp₁'
case mp.intro.intro.intro.intro.inr.inl
R : Type u_1
V : Type u_2
V' : Type ?u.233854
P : Type u_3
P' : Type ?u.233860
inst✝⁶ : LinearOrderedField 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 p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : y -ᵥ p₂' = 0
⊢ SameRay R (x -ᵥ p₁) (y -ᵥ p₂')
case mp.intro.intro.intro.intro.inr.inl
R : Type u_1
V : Type u_2
V' : Type ?u.233854
P : Type u_3
P' : Type ?u.233860
inst✝⁶ : LinearOrderedField 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 p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : y -ᵥ p₂' = 0
⊢ x ∈ s ∨ ∃ p₂, p₂ ∈ s ∧ SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
refine' Or.inr ⟨p₂', hp₂', _⟩
case mp.intro.intro.intro.intro.inr.inl
R : Type u_1
V : Type u_2
V' : Type ?u.233854
P : Type u_3
P' : Type ?u.233860
inst✝⁶ : LinearOrderedField 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 p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : y -ᵥ p₂' = 0
⊢ SameRay R (x -ᵥ p₁) 0
case mp.intro.intro.intro.intro.inr.inl
R : Type u_1
V : Type u_2
V' : Type ?u.233854
P : Type u_3
P' : Type ?u.233860
inst✝⁶ : LinearOrderedField 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 p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : y -ᵥ p₂' = 0
⊢ SameRay R (x -ᵥ p₁) (y -ᵥ p₂')
rw [h0]
no goals
case mp.intro.intro.intro.intro.inr.inl
R : Type u_1
V : Type u_2
V' : Type ?u.233854
P : Type u_3
P' : Type ?u.233860
inst✝⁶ : LinearOrderedField 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 p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : y -ᵥ p₂' = 0
⊢ SameRay R (x -ᵥ p₁) 0
exact SameRay.zero_right _
case mp.intro.intro.intro.intro.inr.inr.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.233854
P : Type u_3
P' : Type ?u.233860
inst✝⁶ : LinearOrderedField 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 p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
hr : r₁ • (x -ᵥ p₁') = r₂ • (y -ᵥ p₂')
⊢ r₁ • (x -ᵥ p₁) = r₂ • (y -ᵥ ((r₁ / r₂) • (p₁ -ᵥ p₁') +ᵥ p₂'))
case mp.intro.intro.intro.intro.inr.inr.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.233854
P : Type u_3
P' : Type ?u.233860
inst✝⁶ : LinearOrderedField 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 p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
hr : r₁ • (x -ᵥ p₁') = r₂ • (y -ᵥ p₂')
⊢ x ∈ s ∨ ∃ p₂, p₂ ∈ s ∧ SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
refine' Or.inr ⟨(r₁ / r₂) • (p₁ -ᵥ p₁') +ᵥ p₂', s.smul_vsub_vadd_mem _ h hp₁' hp₂',
  Or.inr (Or.inr ⟨r₁, r₂, hr₁, hr₂, _⟩)⟩
no goals
case mp.intro.intro.intro.intro.inr.inr.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.233854
P : Type u_3
P' : Type ?u.233860
inst✝⁶ : LinearOrderedField 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 p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
hr : r₁ • (x -ᵥ p₁') = r₂ • (y -ᵥ p₂')
⊢ r₁ • (x -ᵥ p₁) = r₂ • (y -ᵥ ((r₁ / r₂) • (p₁ -ᵥ p₁') +ᵥ p₂'))
rw [vsub_vadd_eq_vsub_sub, smul_sub, ← hr, smul_smul, mul_div_cancel' _ hr₂.ne.symm,
  ← smul_sub, vsub_sub_vsub_cancel_right]
case mpr.inl
R : Type u_1
V : Type u_2
V' : Type ?u.233854
P : Type u_3
P' : Type ?u.233860
inst✝⁶ : LinearOrderedField 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 p₁ : P
h : p₁ ∈ s
h' : x ∈ s
⊢ WSameSide s x y

case mpr.inr.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.233854
P : Type u_3
P' : Type ?u.233860
inst✝⁶ : LinearOrderedField 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 p₁ : P
h : p₁ ∈ s
h₁ : P
h₂ : h₁ ∈ s
h₃ : SameRay R (x -ᵥ p₁) (y -ᵥ h₁)
⊢ WSameSide s x y
case mpr
R : Type u_1
V : Type u_2
V' : Type ?u.233854
P : Type u_3
P' : Type ?u.233860
inst✝⁶ : LinearOrderedField 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 p₁ : P
h : p₁ ∈ s
⊢ (x ∈ s ∨ ∃ p₂, p₂ ∈ s ∧ SameRay R (x -ᵥ p₁) (y -ᵥ p₂)) → WSameSide s x y
rintro (h' | ⟨h₁, h₂, h₃⟩)
no goals
case mpr.inl
R : Type u_1
V : Type u_2
V' : Type ?u.233854
P : Type u_3
P' : Type ?u.233860
inst✝⁶ : LinearOrderedField 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 p₁ : P
h : p₁ ∈ s
h' : x ∈ s
⊢ WSameSide s x y
exact wSameSide_of_left_mem y h'
no goals
case mpr.inr.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.233854
P : Type u_3
P' : Type ?u.233860
inst✝⁶ : LinearOrderedField 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 p₁ : P
h : p₁ ∈ s
h₁ : P
h₂ : h₁ ∈ s
h₃ : SameRay R (x -ᵥ p₁) (y -ᵥ h₁)
⊢ WSameSide s x y
exact ⟨p₁, h, h₁, h₂, h₃⟩