case mp
R : Type u_1
V : Type u_2
V' : Type ?u.226912
P : Type u_3
P' : Type ?u.226918
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

case mpr
R : Type u_1
V : Type u_2
V' : Type ?u.226912
P : Type u_3
P' : Type ?u.226918
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
⊢ x ∈ s → WOppSide s x x
R : Type u_1
V : Type u_2
V' : Type ?u.226912
P : Type u_3
P' : Type ?u.226918
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
constructor
case mp.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.226912
P : Type u_3
P' : Type ?u.226918
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₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ x)
⊢ x ∈ s
case mp
R : Type u_1
V : Type u_2
V' : Type ?u.226912
P : Type u_3
P' : Type ?u.226918
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
rintro ⟨p₁, hp₁, p₂, hp₂, h⟩
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.226912
P : Type u_3
P' : Type ?u.226918
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₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ x)
a : R
h₁ : x -ᵥ p₁ = a • (x -ᵥ p₁ + (p₂ -ᵥ x))
⊢ x ∈ s
case mp.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.226912
P : Type u_3
P' : Type ?u.226918
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₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ x)
⊢ x ∈ s
obtain ⟨a, -, -, -, -, h₁, -⟩ := h.exists_eq_smul_add
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.226912
P : Type u_3
P' : Type ?u.226918
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₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ x)
a : R
h₁ : x = a • (p₂ -ᵥ p₁) +ᵥ p₁
⊢ x ∈ s
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.226912
P : Type u_3
P' : Type ?u.226918
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₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ x)
a : R
h₁ : x -ᵥ p₁ = a • (x -ᵥ p₁ + (p₂ -ᵥ x))
⊢ x ∈ s
rw [add_comm, vsub_add_vsub_cancel, ← eq_vadd_iff_vsub_eq] at h₁
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.226912
P : Type u_3
P' : Type ?u.226918
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₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ x)
a : R
h₁ : x = a • (p₂ -ᵥ p₁) +ᵥ p₁
⊢ a • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.226912
P : Type u_3
P' : Type ?u.226918
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₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ x)
a : R
h₁ : x = a • (p₂ -ᵥ p₁) +ᵥ p₁
⊢ x ∈ s
rw [h₁]
no goals
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.226912
P : Type u_3
P' : Type ?u.226918
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₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ x)
a : R
h₁ : x = a • (p₂ -ᵥ p₁) +ᵥ p₁
⊢ a • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s
exact s.smul_vsub_vadd_mem a hp₂ hp₁ hp₁
no goals
case mpr
R : Type u_1
V : Type u_2
V' : Type ?u.226912
P : Type u_3
P' : Type ?u.226918
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
⊢ x ∈ s → WOppSide s x x
exact fun h => ⟨x, h, x, h, SameRay.rfl⟩