-- Mathlib/Analysis/Convex/Between.lean
theorem wbtw_swap_left_iff [NoZeroSMulDivisors R V] {x y : P} (z : P) :
    Wbtw R x y z ∧ Wbtw R y x z ↔ x = y

Proof state:
case mp.intro.intro.intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
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

Tactic:
rcases hx with (h | h)

Result:
case mp.intro.intro.intro.intro.intro.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
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
P : Type u_4
inst✝⁴ : OrderedRing R
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

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
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

Tactic:
rw [← h, Left.neg_nonpos_iff]

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
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)

Proof state:
case mp.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
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

Tactic:
rcases hxyz with ⟨ty, hty, rfl⟩

Result:
case mp.intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
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

Proof state:
case mp.intro.intro.intro.intro.intro.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
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

Tactic:
rw [h, lineMap_same_apply]

Result:
no goals

Proof state:
case mpr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
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

Tactic:
exact ⟨wbtw_self_left _ _ _, wbtw_self_left _ _ _⟩

Result:
no goals

Proof state:
case mpr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
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

Tactic:
rintro rfl

Result:
case mpr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
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