R : Type u_1
V : Type u_2
V' : Type ?u.333089
P : Type u_3
P' : Type ?u.333095
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
h : WOppSide s x y
⊢ ∃ p, p ∈ s ∧ Wbtw R x p y
R : Type u_1
V : Type u_2
V' : Type ?u.333089
P : Type u_3
P' : Type ?u.333095
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
⊢ WOppSide s x y ↔ ∃ p, p ∈ s ∧ Wbtw R x p y
refine' ⟨fun h => _, fun ⟨p, hp, h⟩ => h.wOppSide₁₃ hp⟩
case intro.intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.333089
P : Type u_3
P' : Type ?u.333095
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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : x -ᵥ p₁ = 0
⊢ ∃ p, p ∈ s ∧ Wbtw R x p y

case intro.intro.intro.intro.inr.inl
R : Type u_1
V : Type u_2
V' : Type ?u.333089
P : Type u_3
P' : Type ?u.333095
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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : p₂ -ᵥ y = 0
⊢ ∃ p, p ∈ s ∧ Wbtw R x p y

case intro.intro.intro.intro.inr.inr.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.333089
P : Type u_3
P' : Type ?u.333095
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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p₁) = r₂ • (p₂ -ᵥ y)
⊢ ∃ p, p ∈ s ∧ Wbtw R x p y
R : Type u_1
V : Type u_2
V' : Type ?u.333089
P : Type u_3
P' : Type ?u.333095
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
h : WOppSide s x y
⊢ ∃ p, p ∈ s ∧ Wbtw R x p y
rcases h with ⟨p₁, hp₁, p₂, hp₂, h | h | ⟨r₁, r₂, hr₁, hr₂, h⟩⟩
case intro.intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.333089
P : Type u_3
P' : Type ?u.333095
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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : x = p₁
⊢ ∃ p, p ∈ s ∧ Wbtw R x p y
case intro.intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.333089
P : Type u_3
P' : Type ?u.333095
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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : x -ᵥ p₁ = 0
⊢ ∃ p, p ∈ s ∧ Wbtw R x p y
rw [vsub_eq_zero_iff_eq] at h
case intro.intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.333089
P : Type u_3
P' : Type ?u.333095
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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : x = p₁
⊢ ∃ p, p ∈ s ∧ Wbtw R p₁ p y
case intro.intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.333089
P : Type u_3
P' : Type ?u.333095
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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : x = p₁
⊢ ∃ p, p ∈ s ∧ Wbtw R x p y
rw [h]
no goals
case intro.intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.333089
P : Type u_3
P' : Type ?u.333095
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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : x = p₁
⊢ ∃ p, p ∈ s ∧ Wbtw R p₁ p y
exact ⟨p₁, hp₁, wbtw_self_left _ _ _⟩
case intro.intro.intro.intro.inr.inl
R : Type u_1
V : Type u_2
V' : Type ?u.333089
P : Type u_3
P' : Type ?u.333095
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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : p₂ = y
⊢ ∃ p, p ∈ s ∧ Wbtw R x p y
case intro.intro.intro.intro.inr.inl
R : Type u_1
V : Type u_2
V' : Type ?u.333089
P : Type u_3
P' : Type ?u.333095
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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : p₂ -ᵥ y = 0
⊢ ∃ p, p ∈ s ∧ Wbtw R x p y
rw [vsub_eq_zero_iff_eq] at h
case intro.intro.intro.intro.inr.inl
R : Type u_1
V : Type u_2
V' : Type ?u.333089
P : Type u_3
P' : Type ?u.333095
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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : p₂ = y
⊢ ∃ p, p ∈ s ∧ Wbtw R x p p₂
case intro.intro.intro.intro.inr.inl
R : Type u_1
V : Type u_2
V' : Type ?u.333089
P : Type u_3
P' : Type ?u.333095
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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : p₂ = y
⊢ ∃ p, p ∈ s ∧ Wbtw R x p y
rw [← h]
no goals
case intro.intro.intro.intro.inr.inl
R : Type u_1
V : Type u_2
V' : Type ?u.333089
P : Type u_3
P' : Type ?u.333095
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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : p₂ = y
⊢ ∃ p, p ∈ s ∧ Wbtw R x p p₂
exact ⟨p₂, hp₂, wbtw_self_right _ _ _⟩
case intro.intro.intro.intro.inr.inr.intro.intro.intro.intro.refine'_1
R : Type u_1
V : Type u_2
V' : Type ?u.333089
P : Type u_3
P' : Type ?u.333095
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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p₁) = r₂ • (p₂ -ᵥ y)
⊢ ↑(lineMap x y) (r₂ / (r₁ + r₂)) ∈ s

case intro.intro.intro.intro.inr.inr.intro.intro.intro.intro.refine'_2
R : Type u_1
V : Type u_2
V' : Type ?u.333089
P : Type u_3
P' : Type ?u.333095
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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p₁) = r₂ • (p₂ -ᵥ y)
⊢ Wbtw R x (↑(lineMap x y) (r₂ / (r₁ + r₂))) y
case intro.intro.intro.intro.inr.inr.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.333089
P : Type u_3
P' : Type ?u.333095
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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p₁) = r₂ • (p₂ -ᵥ y)
⊢ ∃ p, p ∈ s ∧ Wbtw R x p y
refine' ⟨lineMap x y (r₂ / (r₁ + r₂)), _, _⟩
case intro.intro.intro.intro.inr.inr.intro.intro.intro.intro.refine'_1
R : Type u_1
V : Type u_2
V' : Type ?u.333089
P : Type u_3
P' : Type ?u.333095
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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p₁) = r₂ • (p₂ -ᵥ y)
this : (r₂ / (r₁ + r₂)) • (y -ᵥ p₂ + (p₂ -ᵥ p₁) - (x -ᵥ p₁)) + (x -ᵥ p₁) = (r₂ / (r₁ + r₂)) • (p₂ -ᵥ p₁)
⊢ ↑(lineMap x y) (r₂ / (r₁ + r₂)) ∈ s
case intro.intro.intro.intro.inr.inr.intro.intro.intro.intro.refine'_1
R : Type u_1
V : Type u_2
V' : Type ?u.333089
P : Type u_3
P' : Type ?u.333095
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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p₁) = r₂ • (p₂ -ᵥ y)
⊢ ↑(lineMap x y) (r₂ / (r₁ + r₂)) ∈ s
have : (r₂ / (r₁ + r₂)) • (y -ᵥ p₂ + (p₂ -ᵥ p₁) - (x -ᵥ p₁)) + (x -ᵥ p₁) =
    (r₂ / (r₁ + r₂)) • (p₂ -ᵥ p₁) := by
  rw [add_comm (y -ᵥ p₂), smul_sub, smul_add, add_sub_assoc, add_assoc, add_right_eq_self,
    div_eq_inv_mul, ← neg_vsub_eq_vsub_rev, smul_neg, ← smul_smul, ← h, smul_smul, ← neg_smul,
    ← sub_smul, ← div_eq_inv_mul, ← div_eq_inv_mul, ← neg_div, ← sub_div, sub_eq_add_neg,
    ← neg_add, neg_div, div_self (Left.add_pos hr₁ hr₂).ne.symm, neg_one_smul, neg_add_self]
case intro.intro.intro.intro.inr.inr.intro.intro.intro.intro.refine'_1
R : Type u_1
V : Type u_2
V' : Type ?u.333089
P : Type u_3
P' : Type ?u.333095
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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p₁) = r₂ • (p₂ -ᵥ y)
this : (r₂ / (r₁ + r₂)) • (y -ᵥ p₂ + (p₂ -ᵥ p₁) - (x -ᵥ p₁)) + (x -ᵥ p₁) = (r₂ / (r₁ + r₂)) • (p₂ -ᵥ p₁)
⊢ (r₂ / (r₁ + r₂)) • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s
case intro.intro.intro.intro.inr.inr.intro.intro.intro.intro.refine'_1
R : Type u_1
V : Type u_2
V' : Type ?u.333089
P : Type u_3
P' : Type ?u.333095
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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p₁) = r₂ • (p₂ -ᵥ y)
this : (r₂ / (r₁ + r₂)) • (y -ᵥ p₂ + (p₂ -ᵥ p₁) - (x -ᵥ p₁)) + (x -ᵥ p₁) = (r₂ / (r₁ + r₂)) • (p₂ -ᵥ p₁)
⊢ ↑(lineMap x y) (r₂ / (r₁ + r₂)) ∈ s
rw [lineMap_apply, ← vsub_vadd x p₁, ← vsub_vadd y p₂, vsub_vadd_eq_vsub_sub, vadd_vsub_assoc,
  ← vadd_assoc, vadd_eq_add, this]
no goals
case intro.intro.intro.intro.inr.inr.intro.intro.intro.intro.refine'_1
R : Type u_1
V : Type u_2
V' : Type ?u.333089
P : Type u_3
P' : Type ?u.333095
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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p₁) = r₂ • (p₂ -ᵥ y)
this : (r₂ / (r₁ + r₂)) • (y -ᵥ p₂ + (p₂ -ᵥ p₁) - (x -ᵥ p₁)) + (x -ᵥ p₁) = (r₂ / (r₁ + r₂)) • (p₂ -ᵥ p₁)
⊢ (r₂ / (r₁ + r₂)) • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s
exact s.smul_vsub_vadd_mem (r₂ / (r₁ + r₂)) hp₂ hp₁ hp₁
no goals
R : Type u_1
V : Type u_2
V' : Type ?u.333089
P : Type u_3
P' : Type ?u.333095
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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p₁) = r₂ • (p₂ -ᵥ y)
⊢ (r₂ / (r₁ + r₂)) • (y -ᵥ p₂ + (p₂ -ᵥ p₁) - (x -ᵥ p₁)) + (x -ᵥ p₁) = (r₂ / (r₁ + r₂)) • (p₂ -ᵥ p₁)
rw [add_comm (y -ᵥ p₂), smul_sub, smul_add, add_sub_assoc, add_assoc, add_right_eq_self,
  div_eq_inv_mul, ← neg_vsub_eq_vsub_rev, smul_neg, ← smul_smul, ← h, smul_smul, ← neg_smul,
  ← sub_smul, ← div_eq_inv_mul, ← div_eq_inv_mul, ← neg_div, ← sub_div, sub_eq_add_neg,
  ← neg_add, neg_div, div_self (Left.add_pos hr₁ hr₂).ne.symm, neg_one_smul, neg_add_self]
no goals
case intro.intro.intro.intro.inr.inr.intro.intro.intro.intro.refine'_2
R : Type u_1
V : Type u_2
V' : Type ?u.333089
P : Type u_3
P' : Type ?u.333095
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
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p₁) = r₂ • (p₂ -ᵥ y)
⊢ Wbtw R x (↑(lineMap x y) (r₂ / (r₁ + r₂))) y
exact Set.mem_image_of_mem _
  ⟨div_nonneg hr₂.le (Left.add_pos hr₁ hr₂).le,
    div_le_one_of_le (le_add_of_nonneg_left hr₁.le) (Left.add_pos hr₁ hr₂).le⟩