R : Type u_1
V : Type u_2
V' : Type ?u.242614
P : Type u_3
P' : Type ?u.242620
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
h : p₂ ∈ s
⊢ (y ∈ s ∨ ∃ p₂_1, p₂_1 ∈ s ∧ SameRay R (y -ᵥ p₂) (x -ᵥ p₂_1)) ↔ y ∈ s ∨ ∃ p₁, p₁ ∈ s ∧ SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
R : Type u_1
V : Type u_2
V' : Type ?u.242614
P : Type u_3
P' : Type ?u.242620
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
h : p₂ ∈ s
⊢ WSameSide s x y ↔ y ∈ s ∨ ∃ p₁, p₁ ∈ s ∧ SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
rw [wSameSide_comm, wSameSide_iff_exists_left h]
no goals
R : Type u_1
V : Type u_2
V' : Type ?u.242614
P : Type u_3
P' : Type ?u.242620
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
h : p₂ ∈ s
⊢ (y ∈ s ∨ ∃ p₂_1, p₂_1 ∈ s ∧ SameRay R (y -ᵥ p₂) (x -ᵥ p₂_1)) ↔ y ∈ s ∨ ∃ p₁, p₁ ∈ s ∧ SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
simp_rw [SameRay.sameRay_comm]