R : Type u_1
V : Type u_2
V' : Type ?u.231207
P : Type u_3
P' : Type ?u.231213
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
⊢ ¬(WOppSide s x x ∧ ¬x ∈ s ∧ ¬x ∈ s)
R : Type u_1
V : Type u_2
V' : Type ?u.231207
P : Type u_3
P' : Type ?u.231213
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
⊢ ¬SOppSide s x x
rw [SOppSide]
no goals
R : Type u_1
V : Type u_2
V' : Type ?u.231207
P : Type u_3
P' : Type ?u.231213
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
⊢ ¬(WOppSide s x x ∧ ¬x ∈ s ∧ ¬x ∈ s)
simp