case intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.353300
P : Type u_3
P' : Type ?u.353306
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 : SOppSide s x y
p : P
hp : p ∈ s
hw : Wbtw R x p y
⊢ ∃ p, p ∈ s ∧ Sbtw R x p y
R : Type u_1
V : Type u_2
V' : Type ?u.353300
P : Type u_3
P' : Type ?u.353306
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 : SOppSide s x y
⊢ ∃ p, p ∈ s ∧ Sbtw R x p y
obtain ⟨p, hp, hw⟩ := wOppSide_iff_exists_wbtw.1 h.wOppSide
case intro.intro.refine'_1
R : Type u_1
V : Type u_2
V' : Type ?u.353300
P : Type u_3
P' : Type ?u.353306
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 : SOppSide s x y
p : P
hp : p ∈ s
hw : Wbtw R x p y
⊢ p ≠ x

case intro.intro.refine'_2
R : Type u_1
V : Type u_2
V' : Type ?u.353300
P : Type u_3
P' : Type ?u.353306
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 : SOppSide s x y
p : P
hp : p ∈ s
hw : Wbtw R x p y
⊢ p ≠ y
case intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.353300
P : Type u_3
P' : Type ?u.353306
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 : SOppSide s x y
p : P
hp : p ∈ s
hw : Wbtw R x p y
⊢ ∃ p, p ∈ s ∧ Sbtw R x p y
refine' ⟨p, hp, hw, _, _⟩
case intro.intro.refine'_1
R : Type u_1
V : Type u_2
V' : Type ?u.353300
P : Type u_3
P' : Type ?u.353306
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
y p : P
hp : p ∈ s
h : SOppSide s p y
hw : Wbtw R p p y
⊢ False
case intro.intro.refine'_1
R : Type u_1
V : Type u_2
V' : Type ?u.353300
P : Type u_3
P' : Type ?u.353306
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 : SOppSide s x y
p : P
hp : p ∈ s
hw : Wbtw R x p y
⊢ p ≠ x
rintro rfl
no goals
case intro.intro.refine'_1
R : Type u_1
V : Type u_2
V' : Type ?u.353300
P : Type u_3
P' : Type ?u.353306
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
y p : P
hp : p ∈ s
h : SOppSide s p y
hw : Wbtw R p p y
⊢ False
exact h.2.1 hp
case intro.intro.refine'_2
R : Type u_1
V : Type u_2
V' : Type ?u.353300
P : Type u_3
P' : Type ?u.353306
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
hp : p ∈ s
h : SOppSide s x p
hw : Wbtw R x p p
⊢ False
case intro.intro.refine'_2
R : Type u_1
V : Type u_2
V' : Type ?u.353300
P : Type u_3
P' : Type ?u.353306
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 : SOppSide s x y
p : P
hp : p ∈ s
hw : Wbtw R x p y
⊢ p ≠ y
rintro rfl
no goals
case intro.intro.refine'_2
R : Type u_1
V : Type u_2
V' : Type ?u.353300
P : Type u_3
P' : Type ?u.353306
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
hp : p ∈ s
h : SOppSide s x p
hw : Wbtw R x p p
⊢ False
exact h.2.2 hp