case mp
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x y z : P
⊢ Wbtw R x y z ∧ Wbtw R y x z → x = y

case mpr
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x y z : P
⊢ x = y → Wbtw R x y z ∧ Wbtw R y x z
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x y z : P
⊢ Wbtw R x y z ∧ Wbtw R y x z ↔ x = y
constructor
case mp.intro
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x y z : P
hxyz : Wbtw R x y z
hyxz : Wbtw R y x z
⊢ x = y
case mp
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x y z : P
⊢ Wbtw R x y z ∧ Wbtw R y x z → x = y
rintro ⟨hxyz, hyxz⟩
case mp.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
hyxz : Wbtw R (↑(lineMap x z) ty) x z
⊢ x = ↑(lineMap x z) ty
case mp.intro
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x y z : P
hxyz : Wbtw R x y z
hyxz : Wbtw R y x z
⊢ x = y
rcases hxyz with ⟨ty, hty, rfl⟩
case mp.intro.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
hx : ↑(lineMap (↑(lineMap x z) ty) z) tx = x
⊢ x = ↑(lineMap x z) ty
case mp.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
hyxz : Wbtw R (↑(lineMap x z) ty) x z
⊢ x = ↑(lineMap x z) ty
rcases hyxz with ⟨tx, htx, hx⟩
case mp.intro.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
hx : tx • (z -ᵥ (ty • (z -ᵥ x) +ᵥ x)) + ty • (z -ᵥ x) +ᵥ x = x
⊢ x = ↑(lineMap x z) ty
case mp.intro.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
hx : ↑(lineMap (↑(lineMap x z) ty) z) tx = x
⊢ x = ↑(lineMap x z) ty
rw [lineMap_apply, lineMap_apply, ← add_vadd] at hx
case mp.intro.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
hx : tx - tx * ty + ty = 0 ∨ z -ᵥ x = 0
⊢ x = ↑(lineMap x z) ty
case mp.intro.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
hx : tx • (z -ᵥ (ty • (z -ᵥ x) +ᵥ x)) + ty • (z -ᵥ x) +ᵥ x = x
⊢ x = ↑(lineMap x z) ty
rw [← @vsub_eq_zero_iff_eq V, vadd_vsub, vsub_vadd_eq_vsub_sub, smul_sub, smul_smul, ← sub_smul,
  ← add_smul, smul_eq_zero] at hx
case mp.intro.intro.intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
h : tx - tx * ty + ty = 0
⊢ x = ↑(lineMap x z) ty

case mp.intro.intro.intro.intro.intro.inr
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
h : z -ᵥ x = 0
⊢ x = ↑(lineMap x z) ty
case mp.intro.intro.intro.intro.intro
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
hx : tx - tx * ty + ty = 0 ∨ z -ᵥ x = 0
⊢ x = ↑(lineMap x z) ty
rcases hx with (h | h)
case mp.intro.intro.intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
h : tx * 1 - tx * ty + ty = 0
⊢ x = ↑(lineMap x z) ty
case mp.intro.intro.intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
h : tx - tx * ty + ty = 0
⊢ x = ↑(lineMap x z) ty
nth_rw 1 [← mul_one tx] at h
case mp.intro.intro.intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
h : -(tx * (1 - ty)) = ty
⊢ x = ↑(lineMap x z) ty
case mp.intro.intro.intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
h : tx * 1 - tx * ty + ty = 0
⊢ x = ↑(lineMap x z) ty
rw [← mul_sub, add_eq_zero_iff_neg_eq] at h
case mp.intro.intro.intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
h : -(tx * (1 - ty)) = ty
h' : ty = 0
⊢ x = ↑(lineMap x z) ty
case mp.intro.intro.intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
h : -(tx * (1 - ty)) = ty
⊢ x = ↑(lineMap x z) ty
have h' : ty = 0 := by
  refine' le_antisymm _ hty.1
  rw [← h, Left.neg_nonpos_iff]
  exact mul_nonneg htx.1 (sub_nonneg.2 hty.2)
no goals
case mp.intro.intro.intro.intro.intro.inl
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
h : -(tx * (1 - ty)) = ty
h' : ty = 0
⊢ x = ↑(lineMap x z) ty
simp [h']
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
h : -(tx * (1 - ty)) = ty
⊢ ty ≤ 0
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
h : -(tx * (1 - ty)) = ty
⊢ ty = 0
refine' le_antisymm _ hty.1
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
h : -(tx * (1 - ty)) = ty
⊢ 0 ≤ tx * (1 - ty)
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
h : -(tx * (1 - ty)) = ty
⊢ ty ≤ 0
rw [← h, Left.neg_nonpos_iff]
no goals
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
h : -(tx * (1 - ty)) = ty
⊢ 0 ≤ tx * (1 - ty)
exact mul_nonneg htx.1 (sub_nonneg.2 hty.2)
case mp.intro.intro.intro.intro.intro.inr
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
h : z = x
⊢ x = ↑(lineMap x z) ty
case mp.intro.intro.intro.intro.intro.inr
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
h : z -ᵥ x = 0
⊢ x = ↑(lineMap x z) ty
rw [vsub_eq_zero_iff_eq] at h
no goals
case mp.intro.intro.intro.intro.intro.inr
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
h : z = x
⊢ x = ↑(lineMap x z) ty
rw [h, lineMap_same_apply]
case mpr
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x z : P
⊢ Wbtw R x x z ∧ Wbtw R x x z
case mpr
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x y z : P
⊢ x = y → Wbtw R x y z ∧ Wbtw R y x z
rintro rfl
no goals
case mpr
R : Type u_1
V : Type u_2
V' : Type ?u.181718
P : Type u_3
P' : Type ?u.181724
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
x z : P
⊢ Wbtw R x x z ∧ Wbtw R x x z
exact ⟨wbtw_self_left _ _ _, wbtw_self_left _ _ _⟩