R : Type u_1
V : Type u_2
V' : Type ?u.246833
P : Type u_3
P' : Type ?u.246839
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 ∧ (x ∈ s ∨ ∃ p₂, p₂ ∈ s ∧ SameRay R (x -ᵥ p₁) (y -ᵥ p₂)) ↔
      ¬y ∈ s ∧ ∃ p₂, p₂ ∈ s ∧ SameRay R (x -ᵥ p₁) (y -ᵥ p₂))
R : Type u_1
V : Type u_2
V' : Type ?u.246833
P : Type u_3
P' : Type ?u.246839
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
⊢ SSameSide s x y ↔ ¬x ∈ s ∧ ¬y ∈ s ∧ ∃ p₂, p₂ ∈ s ∧ SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
rw [SSameSide, and_comm, wSameSide_iff_exists_left h, and_assoc, and_congr_right_iff]
R : Type u_1
V : Type u_2
V' : Type ?u.246833
P : Type u_3
P' : Type ?u.246839
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
hx : ¬x ∈ s
⊢ ¬y ∈ s ∧ (x ∈ s ∨ ∃ p₂, p₂ ∈ s ∧ SameRay R (x -ᵥ p₁) (y -ᵥ p₂)) ↔
    ¬y ∈ s ∧ ∃ p₂, p₂ ∈ s ∧ SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
R : Type u_1
V : Type u_2
V' : Type ?u.246833
P : Type u_3
P' : Type ?u.246839
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 ∧ (x ∈ s ∨ ∃ p₂, p₂ ∈ s ∧ SameRay R (x -ᵥ p₁) (y -ᵥ p₂)) ↔
      ¬y ∈ s ∧ ∃ p₂, p₂ ∈ s ∧ SameRay R (x -ᵥ p₁) (y -ᵥ p₂))
intro hx
no goals
R : Type u_1
V : Type u_2
V' : Type ?u.246833
P : Type u_3
P' : Type ?u.246839
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
hx : ¬x ∈ s
⊢ ¬y ∈ s ∧ (x ∈ s ∨ ∃ p₂, p₂ ∈ s ∧ SameRay R (x -ᵥ p₁) (y -ᵥ p₂)) ↔
    ¬y ∈ s ∧ ∃ p₂, p₂ ∈ s ∧ SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
rw [or_iff_right hx]