case h
R : Type u_1
V : Type u_2
V' : Type ?u.400251
P : Type u_3
P' : Type ?u.400257
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 p : P
hx : ¬x ∈ s
hp : p ∈ s
y : P
⊢ y ∈ {y | WSameSide s x y} ↔ y ∈ Set.image2 (fun t q => t • (x -ᵥ p) +ᵥ q) (Set.Ici 0) ↑s
R : Type u_1
V : Type u_2
V' : Type ?u.400251
P : Type u_3
P' : Type ?u.400257
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 p : P
hx : ¬x ∈ s
hp : p ∈ s
⊢ {y | WSameSide s x y} = Set.image2 (fun t q => t • (x -ᵥ p) +ᵥ q) (Set.Ici 0) ↑s
ext y
case h
R : Type u_1
V : Type u_2
V' : Type ?u.400251
P : Type u_3
P' : Type ?u.400257
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 p : P
hx : ¬x ∈ s
hp : p ∈ s
y : P
⊢ WSameSide s x y ↔ ∃ a b, 0 ≤ a ∧ b ∈ ↑s ∧ a • (x -ᵥ p) +ᵥ b = y
case h
R : Type u_1
V : Type u_2
V' : Type ?u.400251
P : Type u_3
P' : Type ?u.400257
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 p : P
hx : ¬x ∈ s
hp : p ∈ s
y : P
⊢ y ∈ {y | WSameSide s x y} ↔ y ∈ Set.image2 (fun t q => t • (x -ᵥ p) +ᵥ q) (Set.Ici 0) ↑s
simp_rw [Set.mem_setOf, Set.mem_image2, Set.mem_Ici, mem_coe]
case h.mp
R : Type u_1
V : Type u_2
V' : Type ?u.400251
P : Type u_3
P' : Type ?u.400257
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 p : P
hx : ¬x ∈ s
hp : p ∈ s
y : P
⊢ WSameSide s x y → ∃ a b, 0 ≤ a ∧ b ∈ ↑s ∧ a • (x -ᵥ p) +ᵥ b = y

case h.mpr
R : Type u_1
V : Type u_2
V' : Type ?u.400251
P : Type u_3
P' : Type ?u.400257
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 p : P
hx : ¬x ∈ s
hp : p ∈ s
y : P
⊢ (∃ a b, 0 ≤ a ∧ b ∈ ↑s ∧ a • (x -ᵥ p) +ᵥ b = y) → WSameSide s x y
case h
R : Type u_1
V : Type u_2
V' : Type ?u.400251
P : Type u_3
P' : Type ?u.400257
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 p : P
hx : ¬x ∈ s
hp : p ∈ s
y : P
⊢ WSameSide s x y ↔ ∃ a b, 0 ≤ a ∧ b ∈ ↑s ∧ a • (x -ᵥ p) +ᵥ b = y
constructor
case h.mp
R : Type u_1
V : Type u_2
V' : Type ?u.400251
P : Type u_3
P' : Type ?u.400257
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 p : P
hx : ¬x ∈ s
hp : p ∈ s
y : P
⊢ (∃ p₂, p₂ ∈ s ∧ SameRay R (x -ᵥ p) (y -ᵥ p₂)) → ∃ a b, 0 ≤ a ∧ b ∈ ↑s ∧ a • (x -ᵥ p) +ᵥ b = y
case h.mp
R : Type u_1
V : Type u_2
V' : Type ?u.400251
P : Type u_3
P' : Type ?u.400257
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 p : P
hx : ¬x ∈ s
hp : p ∈ s
y : P
⊢ WSameSide s x y → ∃ a b, 0 ≤ a ∧ b ∈ ↑s ∧ a • (x -ᵥ p) +ᵥ b = y
rw [wSameSide_iff_exists_left hp, or_iff_right hx]
case h.mp.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.400251
P : Type u_3
P' : Type ?u.400257
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 p : P
hx : ¬x ∈ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : x -ᵥ p = 0
⊢ ∃ a b, 0 ≤ a ∧ b ∈ ↑s ∧ a • (x -ᵥ p) +ᵥ b = y

case h.mp.intro.intro.inr.inl
R : Type u_1
V : Type u_2
V' : Type ?u.400251
P : Type u_3
P' : Type ?u.400257
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 p : P
hx : ¬x ∈ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : y -ᵥ p₂ = 0
⊢ ∃ a b, 0 ≤ a ∧ b ∈ ↑s ∧ a • (x -ᵥ p) +ᵥ b = y

case h.mp.intro.intro.inr.inr.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.400251
P : Type u_3
P' : Type ?u.400257
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 p : P
hx : ¬x ∈ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p) = r₂ • (y -ᵥ p₂)
⊢ ∃ a b, 0 ≤ a ∧ b ∈ ↑s ∧ a • (x -ᵥ p) +ᵥ b = y
case h.mp
R : Type u_1
V : Type u_2
V' : Type ?u.400251
P : Type u_3
P' : Type ?u.400257
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 p : P
hx : ¬x ∈ s
hp : p ∈ s
y : P
⊢ (∃ p₂, p₂ ∈ s ∧ SameRay R (x -ᵥ p) (y -ᵥ p₂)) → ∃ a b, 0 ≤ a ∧ b ∈ ↑s ∧ a • (x -ᵥ p) +ᵥ b = y
rintro ⟨p₂, hp₂, h | h | ⟨r₁, r₂, hr₁, hr₂, h⟩⟩
case h.mp.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.400251
P : Type u_3
P' : Type ?u.400257
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 p : P
hx : ¬x ∈ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : x = p
⊢ ∃ a b, 0 ≤ a ∧ b ∈ ↑s ∧ a • (x -ᵥ p) +ᵥ b = y
case h.mp.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.400251
P : Type u_3
P' : Type ?u.400257
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 p : P
hx : ¬x ∈ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : x -ᵥ p = 0
⊢ ∃ a b, 0 ≤ a ∧ b ∈ ↑s ∧ a • (x -ᵥ p) +ᵥ b = y
rw [vsub_eq_zero_iff_eq] at h
no goals
case h.mp.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.400251
P : Type u_3
P' : Type ?u.400257
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 p : P
hx : ¬x ∈ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : x = p
⊢ ∃ a b, 0 ≤ a ∧ b ∈ ↑s ∧ a • (x -ᵥ p) +ᵥ b = y
exact False.elim (hx (h.symm ▸ hp))
case h.mp.intro.intro.inr.inl
R : Type u_1
V : Type u_2
V' : Type ?u.400251
P : Type u_3
P' : Type ?u.400257
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 p : P
hx : ¬x ∈ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : y = p₂
⊢ ∃ a b, 0 ≤ a ∧ b ∈ ↑s ∧ a • (x -ᵥ p) +ᵥ b = y
case h.mp.intro.intro.inr.inl
R : Type u_1
V : Type u_2
V' : Type ?u.400251
P : Type u_3
P' : Type ?u.400257
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 p : P
hx : ¬x ∈ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : y -ᵥ p₂ = 0
⊢ ∃ a b, 0 ≤ a ∧ b ∈ ↑s ∧ a • (x -ᵥ p) +ᵥ b = y
rw [vsub_eq_zero_iff_eq] at h
case h.mp.intro.intro.inr.inl
R : Type u_1
V : Type u_2
V' : Type ?u.400251
P : Type u_3
P' : Type ?u.400257
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 p : P
hx : ¬x ∈ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : y = p₂
⊢ 0 • (x -ᵥ p) +ᵥ p₂ = y
case h.mp.intro.intro.inr.inl
R : Type u_1
V : Type u_2
V' : Type ?u.400251
P : Type u_3
P' : Type ?u.400257
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 p : P
hx : ¬x ∈ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : y = p₂
⊢ ∃ a b, 0 ≤ a ∧ b ∈ ↑s ∧ a • (x -ᵥ p) +ᵥ b = y
refine' ⟨0, p₂, le_refl _, hp₂, _⟩
no goals
case h.mp.intro.intro.inr.inl
R : Type u_1
V : Type u_2
V' : Type ?u.400251
P : Type u_3
P' : Type ?u.400257
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 p : P
hx : ¬x ∈ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : y = p₂
⊢ 0 • (x -ᵥ p) +ᵥ p₂ = y
simp [h]
case h.mp.intro.intro.inr.inr.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.400251
P : Type u_3
P' : Type ?u.400257
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 p : P
hx : ¬x ∈ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p) = r₂ • (y -ᵥ p₂)
⊢ (r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
case h.mp.intro.intro.inr.inr.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.400251
P : Type u_3
P' : Type ?u.400257
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 p : P
hx : ¬x ∈ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p) = r₂ • (y -ᵥ p₂)
⊢ ∃ a b, 0 ≤ a ∧ b ∈ ↑s ∧ a • (x -ᵥ p) +ᵥ b = y
refine' ⟨r₁ / r₂, p₂, (div_pos hr₁ hr₂).le, hp₂, _⟩
no goals
case h.mp.intro.intro.inr.inr.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.400251
P : Type u_3
P' : Type ?u.400257
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 p : P
hx : ¬x ∈ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p) = r₂ • (y -ᵥ p₂)
⊢ (r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y
rw [div_eq_inv_mul, ← smul_smul, h, smul_smul, inv_mul_cancel hr₂.ne.symm, one_smul,
  vsub_vadd]
case h.mpr.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.400251
P : Type u_3
P' : Type ?u.400257
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 p : P
hx : ¬x ∈ s
hp : p ∈ s
t : R
p' : P
ht : 0 ≤ t
hp' : p' ∈ ↑s
⊢ WSameSide s x (t • (x -ᵥ p) +ᵥ p')
case h.mpr
R : Type u_1
V : Type u_2
V' : Type ?u.400251
P : Type u_3
P' : Type ?u.400257
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 p : P
hx : ¬x ∈ s
hp : p ∈ s
y : P
⊢ (∃ a b, 0 ≤ a ∧ b ∈ ↑s ∧ a • (x -ᵥ p) +ᵥ b = y) → WSameSide s x y
rintro ⟨t, p', ht, hp', rfl⟩
no goals
case h.mpr.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.400251
P : Type u_3
P' : Type ?u.400257
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 p : P
hx : ¬x ∈ s
hp : p ∈ s
t : R
p' : P
ht : 0 ≤ t
hp' : p' ∈ ↑s
⊢ WSameSide s x (t • (x -ᵥ p) +ᵥ p')
exact wSameSide_smul_vsub_vadd_right x hp hp' ht