R : Type u_1
V : Type u_2
V' : Type ?u.274203
P : Type u_3
P' : Type ?u.274209
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
⊢ ¬x ∈ s →
    ¬y ∈ s → ((y ∈ s ∨ ∃ p₁, p₁ ∈ s ∧ SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) ↔ ∃ p₁, p₁ ∈ s ∧ SameRay R (x -ᵥ p₁) (p₂ -ᵥ y))
R : Type u_1
V : Type u_2
V' : Type ?u.274203
P : Type u_3
P' : Type ?u.274209
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
⊢ SOppSide s x y ↔ ¬x ∈ s ∧ ¬y ∈ s ∧ ∃ p₁, p₁ ∈ s ∧ SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
rw [SOppSide, and_comm, wOppSide_iff_exists_right h, and_assoc, and_congr_right_iff,
  and_congr_right_iff]
R : Type u_1
V : Type u_2
V' : Type ?u.274203
P : Type u_3
P' : Type ?u.274209
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
a✝ : ¬x ∈ s
hy : ¬y ∈ s
⊢ (y ∈ s ∨ ∃ p₁, p₁ ∈ s ∧ SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) ↔ ∃ p₁, p₁ ∈ s ∧ SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
R : Type u_1
V : Type u_2
V' : Type ?u.274203
P : Type u_3
P' : Type ?u.274209
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
⊢ ¬x ∈ s →
    ¬y ∈ s → ((y ∈ s ∨ ∃ p₁, p₁ ∈ s ∧ SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) ↔ ∃ p₁, p₁ ∈ s ∧ SameRay R (x -ᵥ p₁) (p₂ -ᵥ y))
rintro _ hy
no goals
R : Type u_1
V : Type u_2
V' : Type ?u.274203
P : Type u_3
P' : Type ?u.274209
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
a✝ : ¬x ∈ s
hy : ¬y ∈ s
⊢ (y ∈ s ∨ ∃ p₁, p₁ ∈ s ∧ SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) ↔ ∃ p₁, p₁ ∈ s ∧ SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
rw [or_iff_right hy]