case mp
R : Type u_1
V : Type u_2
V' : Type ?u.316087
P : Type u_3
P' : Type ?u.316093
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
⊢ WSameSide s x y ∧ WOppSide s x y → x ∈ s ∨ y ∈ s

case mpr
R : Type u_1
V : Type u_2
V' : Type ?u.316087
P : Type u_3
P' : Type ?u.316093
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
⊢ x ∈ s ∨ y ∈ s → WSameSide s x y ∧ WOppSide s x y
R : Type u_1
V : Type u_2
V' : Type ?u.316087
P : Type u_3
P' : Type ?u.316093
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
⊢ WSameSide s x y ∧ WOppSide s x y ↔ x ∈ s ∨ y ∈ s
constructor
case mp.intro
R : Type u_1
V : Type u_2
V' : Type ?u.316087
P : Type u_3
P' : Type ?u.316093
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
hs : WSameSide s x y
ho : WOppSide s x y
⊢ x ∈ s ∨ y ∈ s
case mp
R : Type u_1
V : Type u_2
V' : Type ?u.316087
P : Type u_3
P' : Type ?u.316093
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
⊢ WSameSide s x y ∧ WOppSide s x y → x ∈ s ∨ y ∈ s
rintro ⟨hs, ho⟩
case mp.intro
R : Type u_1
V : Type u_2
V' : Type ?u.316087
P : Type u_3
P' : Type ?u.316093
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
hs : WSameSide s x y
ho : WOppSide s y x
⊢ x ∈ s ∨ y ∈ s
case mp.intro
R : Type u_1
V : Type u_2
V' : Type ?u.316087
P : Type u_3
P' : Type ?u.316093
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
hs : WSameSide s x y
ho : WOppSide s x y
⊢ x ∈ s ∨ y ∈ s
rw [wOppSide_comm] at ho
case mp.intro
R : Type u_1
V : Type u_2
V' : Type ?u.316087
P : Type u_3
P' : Type ?u.316093
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
hs : WSameSide s x y
ho : WOppSide s y x
h : ¬(x ∈ s ∨ y ∈ s)
⊢ False
case mp.intro
R : Type u_1
V : Type u_2
V' : Type ?u.316087
P : Type u_3
P' : Type ?u.316093
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
hs : WSameSide s x y
ho : WOppSide s y x
⊢ x ∈ s ∨ y ∈ s
by_contra h
case mp.intro
R : Type u_1
V : Type u_2
V' : Type ?u.316087
P : Type u_3
P' : Type ?u.316093
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
hs : WSameSide s x y
ho : WOppSide s y x
h : ¬x ∈ s ∧ ¬y ∈ s
⊢ False
case mp.intro
R : Type u_1
V : Type u_2
V' : Type ?u.316087
P : Type u_3
P' : Type ?u.316093
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
hs : WSameSide s x y
ho : WOppSide s y x
h : ¬(x ∈ s ∨ y ∈ s)
⊢ False
rw [not_or] at h
no goals
case mp.intro
R : Type u_1
V : Type u_2
V' : Type ?u.316087
P : Type u_3
P' : Type ?u.316093
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
hs : WSameSide s x y
ho : WOppSide s y x
h : ¬x ∈ s ∧ ¬y ∈ s
⊢ False
exact h.1 (wOppSide_self_iff.1 (hs.trans_wOppSide ho h.2))
case mpr.inl
R : Type u_1
V : Type u_2
V' : Type ?u.316087
P : Type u_3
P' : Type ?u.316093
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 : x ∈ s
⊢ WSameSide s x y ∧ WOppSide s x y

case mpr.inr
R : Type u_1
V : Type u_2
V' : Type ?u.316087
P : Type u_3
P' : Type ?u.316093
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 : y ∈ s
⊢ WSameSide s x y ∧ WOppSide s x y
case mpr
R : Type u_1
V : Type u_2
V' : Type ?u.316087
P : Type u_3
P' : Type ?u.316093
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
⊢ x ∈ s ∨ y ∈ s → WSameSide s x y ∧ WOppSide s x y
rintro (h | h)
no goals
case mpr.inl
R : Type u_1
V : Type u_2
V' : Type ?u.316087
P : Type u_3
P' : Type ?u.316093
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 : x ∈ s
⊢ WSameSide s x y ∧ WOppSide s x y
exact ⟨wSameSide_of_left_mem y h, wOppSide_of_left_mem y h⟩
no goals
case mpr.inr
R : Type u_1
V : Type u_2
V' : Type ?u.316087
P : Type u_3
P' : Type ?u.316093
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 : y ∈ s
⊢ WSameSide s x y ∧ WOppSide s x y
exact ⟨wSameSide_of_right_mem x h, wOppSide_of_right_mem x h⟩