R : Type u_1
V : Type u_2
V' : Type ?u.264410
P : Type u_3
P' : Type ?u.264416
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₂) (p₂_1 -ᵥ x)) ↔ y ∈ s ∨ ∃ p₁, p₁ ∈ s ∧ SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
R : Type u_1
V : Type u_2
V' : Type ?u.264410
P : Type u_3
P' : Type ?u.264416
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
⊢ WOppSide s x y ↔ y ∈ s ∨ ∃ p₁, p₁ ∈ s ∧ SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
rw [wOppSide_comm, wOppSide_iff_exists_left h]
case mp
R : Type u_1
V : Type u_2
V' : Type ?u.264410
P : Type u_3
P' : Type ?u.264416
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₂) (p₂_1 -ᵥ x)) → y ∈ s ∨ ∃ p₁, p₁ ∈ s ∧ SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

case mpr
R : Type u_1
V : Type u_2
V' : Type ?u.264410
P : Type u_3
P' : Type ?u.264416
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₁, p₁ ∈ s ∧ SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) → y ∈ s ∨ ∃ p₂_1, p₂_1 ∈ s ∧ SameRay R (y -ᵥ p₂) (p₂_1 -ᵥ x)
R : Type u_1
V : Type u_2
V' : Type ?u.264410
P : Type u_3
P' : Type ?u.264416
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₂) (p₂_1 -ᵥ x)) ↔ y ∈ s ∨ ∃ p₁, p₁ ∈ s ∧ SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
constructor
case mp.inl
R : Type u_1
V : Type u_2
V' : Type ?u.264410
P : Type u_3
P' : Type ?u.264416
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
hy : y ∈ s
⊢ y ∈ s ∨ ∃ p₁, p₁ ∈ s ∧ SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

case mp.inr.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.264410
P : Type u_3
P' : Type ?u.264416
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
p : P
hp : p ∈ s
hr : SameRay R (y -ᵥ p₂) (p -ᵥ x)
⊢ y ∈ s ∨ ∃ p₁, p₁ ∈ s ∧ SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
case mp
R : Type u_1
V : Type u_2
V' : Type ?u.264410
P : Type u_3
P' : Type ?u.264416
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₂) (p₂_1 -ᵥ x)) → y ∈ s ∨ ∃ p₁, p₁ ∈ s ∧ SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
rintro (hy | ⟨p, hp, hr⟩)
case mp.inr.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.264410
P : Type u_3
P' : Type ?u.264416
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
p : P
hp : p ∈ s
hr : SameRay R (y -ᵥ p₂) (p -ᵥ x)
⊢ SameRay R (x -ᵥ p) (p₂ -ᵥ y)
case mp.inr.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.264410
P : Type u_3
P' : Type ?u.264416
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
p : P
hp : p ∈ s
hr : SameRay R (y -ᵥ p₂) (p -ᵥ x)
⊢ y ∈ s ∨ ∃ p₁, p₁ ∈ s ∧ SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
refine' Or.inr ⟨p, hp, _⟩
no goals
case mp.inr.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.264410
P : Type u_3
P' : Type ?u.264416
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
p : P
hp : p ∈ s
hr : SameRay R (y -ᵥ p₂) (p -ᵥ x)
⊢ SameRay R (x -ᵥ p) (p₂ -ᵥ y)
rwa [SameRay.sameRay_comm, ← sameRay_neg_iff, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev]
no goals
case mp.inl
R : Type u_1
V : Type u_2
V' : Type ?u.264410
P : Type u_3
P' : Type ?u.264416
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
hy : y ∈ s
⊢ y ∈ s ∨ ∃ p₁, p₁ ∈ s ∧ SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
exact Or.inl hy
case mpr.inl
R : Type u_1
V : Type u_2
V' : Type ?u.264410
P : Type u_3
P' : Type ?u.264416
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
hy : y ∈ s
⊢ y ∈ s ∨ ∃ p₂_1, p₂_1 ∈ s ∧ SameRay R (y -ᵥ p₂) (p₂_1 -ᵥ x)

case mpr.inr.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.264410
P : Type u_3
P' : Type ?u.264416
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
p : P
hp : p ∈ s
hr : SameRay R (x -ᵥ p) (p₂ -ᵥ y)
⊢ y ∈ s ∨ ∃ p₂_1, p₂_1 ∈ s ∧ SameRay R (y -ᵥ p₂) (p₂_1 -ᵥ x)
case mpr
R : Type u_1
V : Type u_2
V' : Type ?u.264410
P : Type u_3
P' : Type ?u.264416
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₁, p₁ ∈ s ∧ SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) → y ∈ s ∨ ∃ p₂_1, p₂_1 ∈ s ∧ SameRay R (y -ᵥ p₂) (p₂_1 -ᵥ x)
rintro (hy | ⟨p, hp, hr⟩)
case mpr.inr.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.264410
P : Type u_3
P' : Type ?u.264416
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
p : P
hp : p ∈ s
hr : SameRay R (x -ᵥ p) (p₂ -ᵥ y)
⊢ SameRay R (y -ᵥ p₂) (p -ᵥ x)
case mpr.inr.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.264410
P : Type u_3
P' : Type ?u.264416
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
p : P
hp : p ∈ s
hr : SameRay R (x -ᵥ p) (p₂ -ᵥ y)
⊢ y ∈ s ∨ ∃ p₂_1, p₂_1 ∈ s ∧ SameRay R (y -ᵥ p₂) (p₂_1 -ᵥ x)
refine' Or.inr ⟨p, hp, _⟩
no goals
case mpr.inr.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.264410
P : Type u_3
P' : Type ?u.264416
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
p : P
hp : p ∈ s
hr : SameRay R (x -ᵥ p) (p₂ -ᵥ y)
⊢ SameRay R (y -ᵥ p₂) (p -ᵥ x)
rwa [SameRay.sameRay_comm, ← sameRay_neg_iff, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev]
no goals
case mpr.inl
R : Type u_1
V : Type u_2
V' : Type ?u.264410
P : Type u_3
P' : Type ?u.264416
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
hy : y ∈ s
⊢ y ∈ s ∨ ∃ p₂_1, p₂_1 ∈ s ∧ SameRay R (y -ᵥ p₂) (p₂_1 -ᵥ x)
exact Or.inl hy